PVS Ground Evaluator

The PVS ground evaluator consists of a translator from an executable subset of PVS into Common Lisp, a proof rule, and an evaluation environment. The subset of PVS which is handled by the translation is large - the unexecutable fragments are uninterpreted functions, non-bounded quantification, free variables, and higher-order equalities. However, the evaluation of expressions is non-strict, so expressions may be evaluable even if they contain non-evaluable sub-expressions. You can see the code generated by the translation for your theory with the Emacs command M-x pvs-lisp-theory.

The proof rule (eval) allows for the evaluation of ground PVS expressions whilst in the prover. Currently this has no effect on the state of the proof, but simply displays the result of the evaluation and otherwise acts like a (skip).

The evaluation environment is invoked by the Emacs command M-x pvsio; you will be prompted for a theory, defaulting to the one containing the cursor. This is an interactive read-eval-print loop that reads PVS expressions from the user, translates them to Lisp, evaluates them, and returns the results as PVS term.

Soundness and TCCs

The translation and evaluation assume that you have proven all TCCs associated with the expression you are evaluating - including those on declarations upon which the expression depends. This allows for greater execution speed, as the evaluation does not have to perform runtime checks.

Evaluation in the presence of unproven TCCs is unsound, just as proofs in the presence of unproven TCCs. However, in the evaluator the consequences can be more disastrous - you may crash into the Lisp debugger (type (restore) to resume) or worse may run out of stack space and kill the Lisp process.

When in the evaluation environment, the evaluator will display any TCCs that were generated by typechecking the expression you supplied. You should inspect these carefully before answering yes to continue the evaluation. If you wish to confirm to yourself that the TCCs are indeed provable, add the expression to be evaluated as a constant to the theory: that is, instead of just typing "factorial(-1)" to the evaluation environment (which generates an unproveable TCC and causes an infinite loop if you proceed with the evaluation anyway), add the declaration "crash : nat = factorial(-1)" to the theory and evaluate "crash" only after the TCCs have been proved (which is impossible in the case of that example).

Evaluation Environment

The evaluation environment is started with the Emacs command M-x pvsio. You will be prompted for a theory name - the evaluation then takes place logically after the last declaration in that theory.

PVS expressions (enclosed in double quotes, e.g. "exists (i:subrange(1,10)) : p(i)") can now be typed to the <GndEval> prompt. These are parsed and typechecked just as any other PVS expression, so you will get the standard parsing / typechecking errors if you make a mistake. The evaluator will then print the result of the expression, or an error from the translator or evaluator (see below).

The translation and compilation of PVS is performed lazily, ie on demand, so the first use of a particular definition will cause the evaluator to proceed more slowly than subsequent evaluations (note - translation time is not included in any reported timings).

There are several commands that may be typed to the evaluator (without quotes) that control its operation:

q or quit quit the evaluator
h or help display list of commands and current settings
timing display timing information for each execution
notiming don't display timing information
destructive use destructive updates when possible
nondestructive don't use destructive evaluation
convert convert the result back into PVS syntax
noconvert don't convert the result back into PVS syntax
verbose enable some verbose compiler messages
quiet disable verbose compiler messages

Error Messages

Hit uninterpreted term FOO during evaluation: The evaluator tried to evaluate a term (foo) for which there is no definition. See "uninterpreted constants" in the PVS language guide.

Typechecking FOO produced the following TCCs: There were TCCs generated from the expression (foo) you typed in. Evaluation may be unsound in the presence of unproven TCCs, or result in Lisp errors (see above).

FOO could not be translated: REASON: The translation of construct FOO into Lisp failed for the given reason.


fac : THEORY

  factorial(i : nat) : RECURSIVE nat =
    IF i = 0 THEN
      i * factorial(i - 1)

END fac

<GndEval> "factorial(12)"
; cpu time (non-gc) 0 msec user, 0 msec system
; cpu time (gc)     0 msec user, 0 msec system
; cpu time (total)  0 msec user, 0 msec system
; real time  0 msec
; space allocation:
;  3 cons cells, 0 symbols, 0 other bytes, 0 static bytes

<GndEval> "factorial(120)"
; cpu time (non-gc) 0 msec user, 0 msec system
; cpu time (gc)     0 msec user, 0 msec system
; cpu time (total)  0 msec user, 0 msec system
; real time  0 msec
; space allocation:
;  3 cons cells, 0 symbols, 6,216 other bytes, 0 static bytes

More Information

See also the reports

Please send comments and feedback on the evaluator to pvs-bugs@csl.sri.com.