|PVS 2.3 Experimental Features - ground evaluation|
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.
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).
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|
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 ==> 6689502913449127057588118054090372586752746333138029810295671352301633557244962989366874165271984981308157637893214090552534408589408121859898481114389650005964960521256960000000000000000000000000000
|Last modified: Wed Jun 23 02:16:57 PDT 1999||[ PVS Home Page]|