Evaluating Expressions

"Constructive" expressions -- i.e., using only constructively defined types and ops -- can be evaluated directly from the Specware Shell. Evaluating an expression requires a "context" to be set, which is a spec containing the definitions of the relevant types and ops. For example, in the context of

spec def f x = 2*x+1 def u = 6172 endspec

the expression f u has value 12345.

The evaluation context can be set by the shell command

ctext [spec-term]

As usual, if the argument is absent, it indicates the last term processed, which must elaborate to a spec.

Once a context has been set, a Metaslang expression can be evaluated by:

eval [expression]

which results in the value of the expression being shown, insofar as possible: some types of values, in particular functions, have no "printable" representation. Apart from that, values are shown using Metaslang syntax; for example, eval [100, 2*100] shows [100, 200]. The evaluation is done by a built-in Metaslang interpreter.

The command eval may be abbreviated to e.

Instead of using the built-in Metaslang interpreter, it is also possible to evaluate Metaslang expressions from the Specware Shell command line as translated into Lisp. Unless no user-defined types and ops are used (as in the expression 2+2), this requires that Lisp code has already been generated for the context spec (see the Section called Generating Lisp Code) and that the Lisp file has been loaded (see the Section called Auxiliary Commands for Lisp). The command is:

eval-lisp [expression]

which also results in the value of the expression being shown, but now using Lisp syntax; for example, eval-lisp [100, 2*100] shows (100 200). For expressions whose evaluation is very computation-intensive, this method of evaluation can be substantially faster than using the interpreter.