User Tools
pvs:tools:proveit
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
pvs:tools:proveit [2016/08/25 18:52] jonathan created |
pvs:tools:proveit [2016/09/01 18:58] (current) marina |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Proveit Batch Utility ====== | ====== Proveit Batch Utility ====== | ||
| - | $ proveit --importchain --clean interval_arith/top.pvs | + | ''proveit'' is a command line utility for running the theorem prover in batch mode. |
| + | $ 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> | ||
| + | *** 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 | ||
| + | IMPORTING structures@bags | ||
| + | % NASA library | ||
| + | |||
| + | % All the conjectures prove with grind | ||
| + | test1: CONJECTURE | ||
| + | member(5,insert(5,emptybag)) = 1 | ||
| + | |||
| + | %|- test1 : PROOF | ||
| + | %|- (grind) | ||
| + | %|- QED | ||
| + | |||
| + | test2: CONJECTURE | ||
| + | count(1, emptybag) = 0 | ||
| + | AND count(1, insert(1, emptybag)) = 1 | ||
| + | AND count(1, insert(1, insert(1, emptybag))) = 2 | ||
| + | |||
| + | %|- test2 : PROOF | ||
| + | %|- (grind) | ||
| + | %|- QED | ||
| + | |||
| + | PRODUCT: TYPE = posnat | ||
| + | prd, prd1, prd2: VAR PRODUCT | ||
| + | | ||
| + | SET_PRODUCT: TYPE = setof[PRODUCT] | ||
| + | sp, sp1, sp2: VAR SET_PRODUCT | ||
| + | |||
| + | % add product p to set of products sp | ||
| + | add_type(p:PRODUCT,sp): SET_PRODUCT = | ||
| + | union(singleton(p), sp) | ||
| + | |||
| + | %IMPORTING structures@bags[PRODUCT] | ||
| + | STOCK: TYPE = bag[PRODUCT] | ||
| + | st, st1, st2: VAR STOCK | ||
| + | |||
| + | add_product(st1, st): STOCK = % add st1 to stock st if dom(st1) | ||
| + | plus(st1, st) | ||
| + | |||
| + | p1,p2,p3: PRODUCT | ||
| + | |||
| + | test3: CONJECTURE | ||
| + | st = emptybag WITH [p1 := 1, p2 := 2] implies count(p2, st) = 2 | ||
| + | |||
| + | %|- test3 : PROOF | ||
| + | %|- (grind) | ||
| + | %|- QED | ||
| + | |||
| + | cart1: bag[PRODUCT] = emptybag WITH [p1 := 1, p2 := 2] | ||
| + | |||
| + | %insert(x,b): bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF) | ||
| + | test4: CONJECTURE | ||
| + | p3 /= p2 AND p2 /= p1 AND p1 /= p3 => count(p3, cart1) = 0 | ||
| + | |||
| + | %|- test4 : PROOF | ||
| + | %|- (grind) | ||
| + | %|- QED | ||
| + | | ||
| + | END use_bag | ||
| + | </code> | ||
pvs/tools/proveit.1472151130.txt.gz · Last modified: 2016/08/25 18:52 by jonathan
Page Tools
