Differences

This shows you the differences between two versions of the page.

--- pvs:tools:pvsio [2016/08/25 19:55]
jonathan created
+++ pvs:tools:pvsio [2016/09/08 18:17] (current)
marina [Ground evaluation]
@@ Line 4: / Line 4: @@
 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 is a PVS package that extends the ground evaluator with a predefined library
+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
+< 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)''

Software Engineering Documentation

User Tools

Site Tools

Differences

Page Tools