If you make a new discovery or have an insight about using PVS, please send me a message about it. I will maintain a list of useful facts for everone's reference. The initial list below is extracted from Ricky W. Butler's "PVS Survival Hints". Check this page from time to time to see if new wisdom has been added.
You should read Section 3.32 of the PVS system guide available from the exercise directory of the home page.
If you think the prover has gotten lost, or that you've asked it to do too much, you can type C-c C-c while in the *pvs* buffer. This will bring you to Lisp's top level where you will see:
Error: Received signal number 2 (Keyboard interrupt) [condition type: INTERRUPT-SIGNAL] Restart actions (select using :continue): 0: continue computation [1c]At the <rcl> prompt type (restore) to get back to the previous sequent.
If you type M-x reset-pvs while your cursor is in the *pvs* buffer it interrupts the prover, as above. If you are positioned in another buffer, current and pending PVS commands are aborted.
Corresponding to each .pvs file is a .prf file that holds all the proofs you have done. If you want to see the stored proof, place your purpose on its theorem statement and type M-x edit-proof. This will open a buffer containing the Lisp representation of the proof. It looks something like this:
If you're a real risk taker, you can change the proof and save the result by typing C-C C-i in the Proof buffer.("" (SKOSIMP*) (EXPAND "whatever") (LIFT-IF) (EXPAND "nonesuch") (PROPAX))
You can setp through a proof one command at a time by issuing either the command M-x step-proof or the command M-x x-step-proof. The latter also displays a proof tree.
The PVS window is split into two parts, a buffer named Proof containing the proof script, and the *pvs* buffer showing the proof in progress.
The command TAB 1 executes one proof step. The command ESC n TAB 1 executes n proof steps.
Repositioning the cursor in the Proofwindow affects which step will be executed next. Therefore, use C-x o to switch between bufferes rather than using mouse clicks.
The PVS prover command (hide f) removes formula number f from the sequent. This helps reduce clutter. The command M-x show-hidden-formulas opens a buffer named Hidden displaying all the hidden formulas. The PVS prover command (reveal f) returns the formula numbered f in Hidden to the sequent.