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

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

• Enter the above files in PVS as ground.pvs and type check it (M-x tcp)
• M-x pvsio puts you into the PVSio ground evaluator
• At the prompt enter (sqrt_newton(2,3)); which already gives a good approximation to sqrt(2)
• Enter: println(sqrt_newton(2,10));
• Prove the Conjecture using (eval-formula)