Differences

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

--- pvs:start [2016/08/24 02:46]
jonathan
+++ pvs:start [2018/10/08 18:41] (current)
jonathan
@@ Line 1: / Line 1: @@
+[[:pvs/tools/pvs|Get started]]
 ====== PVS ======
@@ Line 7: / Line 9: @@
   * [[http://pvs.csl.sri.com/documentation.shtml|SRI Documentation]]
   * [[http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/|NASA PVS site]]
-  * [[http://pvs.eecs.yorku.ca|This site: pvs.eecs.yorku.ca]]. [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:start|EECS Wiki]]
+  * [[http://pvs.eecs.yorku.ca|This site: pvs.eecs.yorku.ca]]. [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:start|EECS Wiki]]. [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:latex:start|LaTex]]
+  * {{ :pvs:pvs-survival.pdf |PVS Survival Tips}}
 ===== Current Components =====
@@ Line 15: / Line 18: @@
   * Nasalib come with a batch ''proveit'' facility, ''hypatheon'' (for browsing the NASA libraries), and [[http://shemesh.larc.nasa.gov/people/cam/PVSio/|PVSio]] (for ground evaluation).
+===== Detailed Documentation =====
+  *{{ :pvs:pvs-system-guide.pdf |PVS System Guide}}
+  * {{ :pvs:pvs-prover-guide.pdf |PVS Prover Guide}}
+  * {{ :pvs:pvs-language-reference.pdf |PVS Language Reference}}
+  * {{ :pvs:pvs-survival-tips.pdf |PVS Survival Tips}}
+  * {{ :pvs:pvs7-prelude.pdf |PVS7 Prelude PDF}}
+  * {{ :pvs:emacs_reference_card.pdf |Emacs Reference Card}}
+<HTML>
+<center>
+<table border="1" width="100%">
+<tbody>
+<tr>
+<td valign="top">
+<table border="1">
+<tbody>
+<tr>
+<th rowspan="2"><font size="+1">Cursor<br>
+Motion</font></th>
+<th colspan="4">Operation</th>
+</tr>
+<tr>
+<th colspan="2">Move</th>
+<th colspan="2">Delete</th>
+</tr>
+<tr>
+<th>Amount</th>
+<th>forward</th>
+<th>backward</th>
+<th>forward</th>
+<th>backward</th>
+</tr>
+<tr>
+<td>Characters</td>
+<td><tt>C-f</tt></td>
+<td><tt>C-b</tt></td>
+<td><tt>C-d</tt></td>
+<td><tt>DEL</tt></td>
+</tr>
+<tr>
+<td>Words</td>
+<td><tt>M-f</tt></td>
+<td><tt>M-b</tt></td>
+<td><tt>M-d</tt></td>
+<td><tt>M-DEL</tt></td>
+</tr>
+<tr>
+<td>Lines</td>
+<td><tt>C-n</tt></td>
+<td><tt>C-p</tt></td>
+<td><tt>C-k</tt> <i>(to EOL)</i></td>
+<td><tt>C-SPC C-a C-w</tt></td>
+</tr>
+<tr>
+<td>Sentences</td>
+<td><tt>M-e</tt></td>
+<td><tt>M-a</tt></td>
+<td><tt>M-k</tt></td>
+<td><tt>C-x&nbsp;DEL</tt></td>
+</tr>
+<tr>
+<td>Expressions</td>
+<td><tt>C-M-f</tt></td>
+<td><tt>C-M-b</tt></td>
+<td><tt>C-M-k</tt></td>
+<td><tt>C-M-DEL</tt></td>
+</tr>
+<tr>
+<td>Paragraphs</td>
+<td><tt>M-}</tt></td>
+<td><tt>M-{</tt></td>
+<td colspan="2"><i>(no standard bindings for delete cmds)</i></td>
+</tr>
+<tr>
+<td>End/start of line</td>
+<td><tt>C-e</tt></td>
+<td><tt>C-a</tt></td>
+<td colspan="2"><i>(repeat count goes to following lines)</i></td>
+</tr>
+<tr>
+<td>End/start of buffer</td>
+<td><tt>M-&gt;</tt></td>
+<td><tt>M-&lt;</tt></td>
+<td colspan="2"><i>(no repeat count)</i></td>
+</tr>
+</tbody>
+</table>
+</td>
+<td valign="top">
+<table>
+<tbody>
+<tr>
+<th colspan="2"> <font size="+2">Cutting and Pasting </font>
+</th>
+</tr>
+<tr>
+<td valign="top"><tt>C-SPC</tt></td>
+<td valign="top">Mark one end of region</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-w</tt></td>
+<td valign="top">Cut (after you Mark and move to other end)
+</td>
+</tr>
+<tr>
+<td valign="top"><tt>M-w</tt></td>
+<td valign="top">Copy (after you Mark and move to other
+end) </td>
+</tr>
+<tr>
+<td valign="top"><tt>C-y</tt></td>
+<td valign="top">Yank (paste) most recently killed (cut or
+copied); will also use text currently selected in another application. </td>
+</tr>
+<tr>
+<td valign="top"><tt>M-y</tt></td>
+<td valign="top">Next most recently killed (do <tt>C-y</tt>
+first, repeat <tt>M-y</tt> to cycle thru all)</td>
+</tr>
+<tr>
+<td colspan="2" valign="top"> <i>To make cut/copy/paste
+behave as it does in other apps, do <tt>M-x&nbsp;cua-mode</tt>, or put
+<pre> (cua-mode)</pre>
+in your <tt>.emacs</tt> to enable in every session.</i> </td>
+</tr>
+</tbody>
+</table>
+</td>
+</tr>
+<tr>
+<td valign="top">
+<table>
+<tbody>
+<tr>
+<th colspan="2"> <font size="+2">Scrolling and Windows</font>
+</th>
+</tr>
+<tr>
+<td valign="top"><tt>C-v</tt></td>
+<td valign="top">Scroll down (toward end of buffer)</td>
+</tr>
+<tr>
+<td valign="top"><tt>M-v</tt></td>
+<td valign="top">Scroll up (toward beginning of buffer)</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-M-v</tt></td>
+<td valign="top">Scroll other window down</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;1</tt></td>
+<td valign="top">One window on current buffer</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;2</tt></td>
+<td valign="top">Split window vertically</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;3</tt></td>
+<td valign="top">Split window horizontally</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;^</tt></td>
+<td valign="top">Grow window vertically; prefix is number
+of lines</td>
+</tr>
+<tr>
+<th colspan="2"> <font size="+2">Command-related Stuff</font>
+</th>
+</tr>
+<tr>
+<td valign="top"><tt>ESC ESC ESC</tt></td>
+<td valign="top">Get me out of where I am now</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-u&nbsp;#</tt></td>
+<td valign="top">Prefix numeric arg # (digits with optional
+<tt>"-"</tt> sign) to next cmd</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-g</tt></td>
+<td valign="top">Stop a command in progress, or quit out of
+a partially entered command</td>
+</tr>
+<tr>
+<th colspan="2"> <font size="+2">Getting help</font> </th>
+</tr>
+<tr>
+<td valign="top"><tt>C-h&nbsp;k</tt></td>
+<td valign="top">Show command documentation; prompts for
+keystrokes</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-h&nbsp;a</tt></td>
+<td valign="top">"Command apropos"; prompts for regexp and
+shows all matching commands</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-h&nbsp;c</tt></td>
+<td valign="top">Show command name on message line; prompts
+for keystrokes</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-h&nbsp;f</tt></td>
+<td valign="top">Describe function; prompts for command or
+function name, shows documentation in other window</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-h&nbsp;i</tt></td>
+<td valign="top">Info browser; gives access to online
+documentation for emacs and more</td>
+</tr>
+</tbody>
+</table>
+<table>
+<tbody>
+<tr>
+<th colspan="2"> <font size="+2">Miscellaneous</font> </th>
+</tr>
+<tr>
+<td valign="top"><tt>C-_</tt> <i>or</i> <tt>C-x&nbsp;u</tt></td>
+<td valign="top">Undo/redo (a series of these keeps
+undoing; after doing something else, <tt>C-_</tt> or <tt>C-x&nbsp;u</tt>
+will undo the undo's)</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-q</tt></td>
+<td valign="top">Quoted insert; inserts the next character
+typed, even if it is a control or meta character</td>
+</tr>
+<tr>
+<td valign="top"><tt>M-x shell-strip-ctrl-m RET</tt></td>
+<td valign="top">Flush ^M at end of line</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-z</tt></td>
+<td valign="top">Suspend/iconify emacs (type <tt>"%emacs"</tt>
+in invoking shell to get it back) </td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;C-c</tt></td>
+<td valign="top">Exit emacs (asks about unsaved buffers and
+running programs)</td>
+</tr>
+</tbody>
+</table>
+</td>
+<td valign="top">
+<table>
+<tbody>
+<tr>
+<th colspan="2"> <font size="+2">Files and Buffers</font> </th>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;C-f</tt></td>
+<td valign="top">Find file (or create if not there);
+prompts for file name</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;C-s</tt></td>
+<td valign="top">Save file</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;C-w</tt></td>
+<td valign="top">Write file; prompts for new name</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;s</tt></td>
+<td valign="top">Save modified buffers; asks about each</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;b</tt></td>
+<td valign="top">Select buffer; prompts for buffer name</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;C-b</tt></td>
+<td valign="top">List buffers; shows in other window</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x&nbsp;k</tt></td>
+<td valign="top">Kill buffer; prompts for buffer name</td>
+</tr>
+<tr>
+<th colspan="2"> <font size="+2">Searching/Replacing</font>
+</th>
+</tr>
+<tr>
+<td valign="top"><tt>C-s</tt></td>
+<td valign="top">Incremental search forward; searches as
+you type</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-r</tt></td>
+<td valign="top">Incremental search backward</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-M-s</tt></td>
+<td valign="top">Regexp search forward (there are
+differences in Emacs regexp syntax wrt Perl, etc.)</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-M-r</tt></td>
+<td valign="top">Regexp search backward</td>
+</tr>
+<tr>
+<td valign="top"><tt>M-x replace-string RET</tt></td>
+<td valign="top">String replace from here to end of buffer;
+prompts for string and replacement</td>
+</tr>
+<tr>
+<td valign="top"><tt>M-x query-replace RET</tt></td>
+<td valign="top">String replace from here to end of buffer,
+querying for each occurrence</td>
+</tr>
+<tr>
+<td valign="top"><tt>M-x grep RET</tt></td>
+<td valign="top">Prompts for a <tt>grep</tt> command,
+shows hits in a buffer</td>
+</tr>
+<tr>
+<td valign="top"><tt>C-x `</tt></td>
+<td valign="top">Visit next <tt>grep</tt> hit</td>
+</tr>
+</tbody>
+</table>
+</td>
+</tr>
+</tbody>
+</table>
+</center>
+</HTML>

Software Engineering Documentation

User Tools

Site Tools

Differences

Page Tools