User Tools
pvs:prover
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
pvs:prover [2016/08/23 17:06] jonathan [Basic] |
pvs:prover [2017/09/14 16:08] (current) jonathan [Basic] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Interaction with Prover ====== | ====== Interaction with Prover ====== | ||
| + | |||
| ===== Basic ===== | ===== Basic ===== | ||
| Line 5: | Line 6: | ||
| * From the command line: ''pvs'' | * From the command line: ''pvs'' | ||
| * Change context: C-c C-c | * Change context: C-c C-c | ||
| - | * Create new PVS file: | + | * Create new PVS file: M-x nf |
| - | * Type Check: | + | * Type Check: M-x tcp |
| + | * Show type correctness conjectures: M-x tccs | ||
| + | * pretty print expanded: C-c C-p e | ||
| * Prove a Conjecture: | * Prove a Conjecture: | ||
| - | * Prove the whole file: | + | * Prove the whole file: C-c C-p f |
| + | * View prelude file: M-x vpf | ||
| + | * View proof status: ''M-x spf'' | ||
| + | * Display the proof in progress: ''M-x show-current-proof '' | ||
| + | ProofLite scripts can be created from proofs in two ways: | ||
| + | (1) Place the cursor on the formula for which you want to create | ||
| + | a ProofLite script and issue the Emacs command: M-x insert-prooflite-script (C-c 2p). T | ||
| + | he ProofLite script is automatically inserted after the formula. | ||
| + | (2) Issue the command: M-x display-prooflite-script (C-c dp) | ||
| + | and enter the name of a formula. The ProofLite script of that | ||
| + | formula is displayed in the bu ffer "ProofLite". | ||
| + | ===== Commands ===== | ||
| + | * Introduce all types in formula: ''(all-typepreds)'' | ||
| + | * ''(typepred a b c)'' | ||
pvs/prover.1471971960.txt.gz · Last modified: 2016/08/23 17:06 by jonathan
Page Tools
