Differences

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

--- pvs:commands [2016/07/19 21:57]
jonathan
+++ pvs:commands [2017/09/06 19:33] (current)
jonathan
@@ Line 1: / Line 1: @@
-~~NOTOC~~
 ====== PVS/Emacs Shortcuts ======
 [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:shortcuts:start#keyboard_shortcuts|SEL wiki]]
+====== Restarting PVS ======
+If you have a run-away prover command (e.g. GRIND), you can type
+''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp.
+At the <rcl> prompt, type (''restore'') to get back to the previous
+sequent.
+If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage
+collection, this command will not engage immediately.
+See Survival-Tips.pdf
 ====== Emacs shortcuts with PVS ======
@@ Line 25: / Line 35: @@
 M-x show-proofs-theory   -- Show all proofs of theory
+M-x x-show-current-proof -- show current proof under x11
 step-proof,       prs (C-c C-p s)  Start proof and set up for stepping
@@ Line 60: / Line 71: @@
 </code>
-====== Restarting PVS ======
+====== Keyboard Shortcuts ======
-If you have a run-away prover command (e.g. GRIND), you can type
-''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp.
-At the <rcl> prompt, type (''restore'') to get back to the previous
-sequent.
-If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage
-collection, this command will not engage immediately.
-See Survival-Tips.pdf
+<html>
+<head>
+<meta content="text/html; charset=ISO-8859-1"
+http-equiv="content-type">
+<title>PVS-commands</title>
+</head>
+<body>
+<p> <strong>Prover Commands</strong></p>
+<p><strong style="font-weight: normal;">If the prover has gotten lost,
+you can type <span style="font-weight: bold;">C-c C-c </span>in the
+*pvs* buffer. This will bring you to Lisp's top level and show:<br>
+<br>
+&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp; Error: Received singal number 2
+(Keyboard interrupt)<br>
+&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp; &nbsp; [condition type:
+INTERRUPT-SIGNAL]<br>
+&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp;&nbsp; <br>
+&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp; &nbsp;Restart actions (select
+using :continue):<br>
+&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp; &nbsp;0: continue computation<br>
+&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp; <br>
+Type <span style="font-weight: bold;">(restore) </span>to get back to
+the previous sequent.<br>
+</strong></p>
+<p><strong style="font-weight: normal;"><span style="font-weight: bold;">(hide
+f)</span> removes formula number f from the sequent. <br>
+The command <span style="font-weight: bold;">M-x show-hidden-formula</span>s
+opens a buffer named Hidden displaying all the hidden formulas. <br>
+The PVS prover command <span style="font-weight: bold;">(reveal f) </span>returns
+the formula numbered f in Hidden to the sequent.</strong><br>
+</p>
+<table border="1" cellpadding="10" width="600">
+<tbody>
+<tr>
+<th align="center">Commands</th>
+<th align="center">Aliases</th>
+<th align="center">Commands</th>
+<th align="center">Aliases</th>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-apply-extensionality</font></td>
+<td align="center"><font size="2">TAB E</font></td>
+<td><font size="2">pvs-prover-assert</font></td>
+<td align="center"><font size="2">TAB a</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-auto-rewrite</font></td>
+<td align="center"><font size="2">TAB A</font></td>
+<td><font size="2">pvs-prover-auto-rewrite-theory</font></td>
+<td align="center"><font size="2">TAB C-a</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-bddsimp</font></td>
+<td align="center"><font size="2">TAB B</font></td>
+<td><font size="2">pvs-prover-beta</font></td>
+<td align="center"><font size="2">TAB b</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-case</font></td>
+<td align="center"><font size="2">TAB c</font></td>
+<td><font size="2">pvs-prover-case-replace</font></td>
+<td align="center"><font size="2">TAB C</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-decompose-equality</font></td>
+<td align="center"><font size="2">TAB =</font></td>
+<td><font size="2">pvs-prover-delete</font></td>
+<td align="center"><font size="2">TAB d</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-do-rewrite</font></td>
+<td align="center"><font size="2">TAB D</font></td>
+<td><font size="2">pvs-prover-expand</font></td>
+<td align="center"><font size="2">TAB e</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-extensionality</font></td>
+<td align="center"><font size="2">TAB x</font></td>
+<td><font size="2">pvs-prover-flatten</font></td>
+<td align="center"><font size="2">TAB f</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-grind</font></td>
+<td align="center"><font size="2">TAB G</font></td>
+<td><font size="2">pvs-prover-ground</font></td>
+<td align="center"><font size="2">TAB g</font></td>
+</tr>
+<tr>
+<td><font size="2">help-pvs-prover-command</font></td>
+<td align="center"><font size="2">TAB H</font></td>
+<td><font size="2">pvs-prover-hide</font></td>
+<td align="center"><font size="2">TAB C-h</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-iff</font></td>
+<td align="center"><font size="2">TAB F</font></td>
+<td><font size="2">pvs-prover-induct</font></td>
+<td align="center"><font size="2">TAB I</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-induct-and-simplify</font></td>
+<td align="center"><font size="2">TAB C-s</font></td>
+<td><font size="2">pvs-prover-inst</font></td>
+<td align="center"><font size="2">TAB i</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-inst-question</font></td>
+<td align="center"><font size="2">TAB ?</font></td>
+<td><font size="2">pvs-prover-lemma</font></td>
+<td align="center"><font size="2">TAB L</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-lift-if</font></td>
+<td align="center"><font size="2">TAB l</font></td>
+<td><font size="2">pvs-prover-model-check</font></td>
+<td align="center"><font size="2">TAB M</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-musimp</font></td>
+<td align="center"><font size="2">TAB m</font></td>
+<td><font size="2">pvs-prover-name</font></td>
+<td align="center"><font size="2">TAB n</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-postpone</font></td>
+<td align="center"><font size="2">TAB P</font></td>
+<td><font size="2">pvs-prover-prop</font></td>
+<td align="center"><font size="2">TAB p</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-quit</font></td>
+<td align="center"><font size="2">TAB C-q</font></td>
+<td><font size="2">pvs-prover-replace</font></td>
+<td align="center"><font size="2">TAB r</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-replace-eta</font></td>
+<td align="center"><font size="2">TAB 8</font></td>
+<td><font size="2">pvs-prover-rewrite</font></td>
+<td align="center"><font size="2">TAB R</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-skolem-bang</font></td>
+<td align="center"><font size="2">TAB !</font></td>
+<td><font size="2">pvs-prover-skosimp</font></td>
+<td align="center"><font size="2">TAB S</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-skosimp-star</font></td>
+<td align="center"><font size="2">TAB *</font></td>
+<td><font size="2">pvs-prover-split</font></td>
+<td align="center"><font size="2">TAB s</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-tcc</font></td>
+<td align="center"><font size="2">TAB T</font></td>
+<td><font size="2">pvs-prover-then</font></td>
+<td align="center"><font size="2">TAB C-t</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-typepred</font></td>
+<td align="center"><font size="2">TAB t</font></td>
+<td><font size="2">pvs-prover-undo</font></td>
+<td align="center"><font size="2">TAB u</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-one-proof-step</font></td>
+<td align="center"><font size="2">TAB 1</font></td>
+<td><font size="2">pvs-prover-many-proof-steps</font></td>
+<td align="center"><font size="2">TAB @</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-undo-one-proof-step</font></td>
+<td align="center"><font size="2">TAB U</font></td>
+<td><font size="2">pvs-prover-undo-many-proof-steps</font></td>
+<td align="center"><font size="2">TAB C-u</font></td>
+</tr>
+<tr>
+<td><font size="2">pvs-prover-skip-one-proof-step</font></td>
+<td align="center"><font size="2">TAB #</font></td>
+</tr>
+</tbody>
+</table>
+<br>
+</body>
+</html>
 ====== Proof Rules ======

Software Engineering Documentation

User Tools

Site Tools

Differences

Page Tools