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 pvs-ground-evaluator. This is an interactive read-eval-print loop that reads expressions from the user and returns the result of their evaluation.
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).
The evaluation environment is started with the Emacs command M-x pvs-ground-evaluator. 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 |
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
BEGIN
factorial(i : nat) : RECURSIVE nat =
IF i = 0 THEN
1
ELSE
i * factorial(i - 1)
ENDIF
MEASURE i
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
==>
479001600
<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
==>
6689502913449127057588118054090372586752746333138029810295671352301633
5572449629893668741652719849813081576378932140905525344085894081218598
98481114389650005964960521256960000000000000000000000000000
See also the reports
Please send comments and feedback on the evaluator to pvs-bugs@csl.sri.com.