====== PVSio Ground Evaluation ======

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. 

[[http://shemesh.larc.nasa.gov/people/cam/PVSio/PVSio-2.d.pdf|PVSio]] ({{ :pvs:tools:pvsio-slides.pdf |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 evaluation =====

<code text 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
</code>

  * 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)''