Differences

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

--- pvs:tools:proveit [2016/08/25 21:12]
jonathan [Proveit Batch Utility]
+++ pvs:tools:proveit [2016/09/01 18:58] (current)
marina
@@ Line 3: / Line 3: @@
 ''proveit'' is a command line utility for running the theorem prover in batch mode.
-  $ proveit --importchain --clean ''use_bag.pvs''
+  $ proveit --importchain --clean use_bag.pvs
+This example can be used to test ''proveit'' and the installation of NASA PVS library.
 ===== Example =====
+  * Download the file below as ''use_bag.pvs'' (uses the NASA Library for Bag)
+  * All the conjectures can be proved with ''(grind)''
+  * execute the above ''proveit'' command in the terminal
+  * This will generate use_bag.summary
-<code text us_bag>
+<code>
+*** use_bag (17:18:33 8/25/2016)
+*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
+*** Trusted Oracles
+***   MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit
+***
+ Proof summary for theory use_bag
+    test1.................................proved - complete   [shostak](0.04 s)
+    test2.................................proved - complete   [shostak](0.03 s)
+    test3.................................proved - complete   [shostak](0.01 s)
+    test4.................................proved - complete   [shostak](0.01 s)
+    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.09 s)
+Grand Totals: 4 proofs, 4 attempted, 4 succeeded (0.09 s)
+</code>
+<code text use_bag>
 use_bag : THEORY
 BEGIN

Software Engineering Documentation