The ground evaluator is an experimental feature of PVS that enables the animation of functional specifications. The ground evaluator extracts Common Lisp code from PVS functional specifications to evaluate ground expressions on top of the PVS underlying Common Lisp machine.
PVSio (slides) is a PVS package that extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. PVSio provides: An alternative (and simplified) Emacs interface to the ground evaluator; A user-friendly mechanism to define new semantic attachments; A stand alone (Emacs-free) interface to the ground evaluator; A set of proof rules that safely integrates the ground evaluator to the PVS theorem prover.
ground : THEORY BEGIN % Also defined in the NASA reals library sqrt_newton(a:nnreal,n:nat): RECURSIVE posreal = IF n=0 THEN a+1 ELSE let r=sqrt_newton(a,n-1) IN (1/2)*(r+a/r) ENDIF MEASURE n+1 %M-x pvsio % <PVSio> (sqrt_newton(2,1)); % 11/6 % <PVSio> (sqrt_newton(2,3)); % 72097/50952 %println(sqrt_newton(2,10)); %<PVSio> println(sqrt_newton2(2,10)); %1.4142135 %Has been shown to satisfy % sqrt(a) < sqrt_newton(a, n) % sqrt_newton(a, n+1) < sqrt_newton(a,n) % As n --> infinity, sqrt_newton(a,n) converges to sqrt(q) test: CONJECTURE 2 < sqrt_newton(2, 10) * sqrt_newton(2, 10) AND sqrt_newton(2, 10) * sqrt_newton(2, 10) < 2.0000000000000001 %|- test : PROOF %|- (eval-formula 1) %|- QED % PVSio safely enables the ground evaluator in the theorem % prover. END ground
M-x tcp
) M-x pvsio
puts you into the PVSio ground evaluator(eval-formula)