User Tools
pvs:tools:pvsio
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
pvs:tools:pvsio [2016/08/25 20:41] jonathan |
pvs:tools:pvsio [2016/09/08 18:17] (current) marina [Ground evaluation] |
||
|---|---|---|---|
| Line 54: | Line 54: | ||
| END ground | END ground | ||
| </code> | </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)'' | ||
| + | |||
pvs/tools/pvsio.1472157667.txt.gz · Last modified: 2016/08/25 20:41 by jonathan
Page Tools
