Index
1	16 Sep	Logic
2	2 Oct	Arithmetic
3	22 Oct	Induction

PVS

Software

The PVS Specification and Verification home page [HTM] contains links to descriptions, documentation, and downloads for PVS. On the CS Linux network (burrow, etc.) the command pvs4 invokes PVS, whose main interface is an emacs window. Users of emacs will have little trouble understanding the command syntax, but for others it will take some getting used to. PVS is available on all platforms (Windows, MAC/OSX, Linux) but installing it requires other packages, most notably a Common Lisp implementation. Our UI, Dylan Bargatze, has done this successfully on his MAC, so you will want to consult with him before attempting to install a personal copy.

Documentation

[PDF]	PVS Quick Reference. Commands, shortcuts, etc. This information is also available through the PVS Help Menu.
[PDF]	PVS Prover Guide. Explains the PVS logic (Ch. 3, a good starting point) and theorem proving commands.
[PDF]	PVS Language Reference. Explains PVS syntax. The examples in discussion should be enough to get you started.
[PDF]	PVS Systerm Guide. Deals with file management and other system level functions. Again, the discussion examples and write-ups should suffice.

PVS Logic

• Create a directory for your PVS work. You can call it anything and place it anywhere. For concreteness, let's call it pvs/. I'll also assume you are on a CS Linux machine.

• Copy the PVS source files, A.pvs, and B.pvs, into your local directory as, for example, my-pvs/B.pvs.

• Move into my-pvs/ and invoke the command pvs4

• In PVS,
  • M-x ff opens a PVS source file (.pvs)
  • M-x pr initiates a proof of the theorem under the cursor. This opens an emacs buffer running the PVS proof editor).

• The instructions in A.pvs and B.pvs say what prover commands to use to complete the proofs:
  • For A.prf you need only the commands (SPLIT f) and (FLATTEN f). Your learning goal should be to know (not guess) which command to use at a given point in the proof.
  • For B.prf you need only the commands only the commands (SPLIT f), (FLATTEN f), (SKOLEM f name) and (INST f t) Again, you want to get to the point of knowing (not guessing) which command to use and when.

• To get help for a prover command, in the PVS menu invoke help-pvs-prover-command (C-c C-n c), also available in the PVS→Help menu.

• The prover's quantifier elimination commands are (It is important to include the quotation marks):

  • (INST i "t") instantiates the for-all (in the antecedent) or there-exists (in the conclusion) variable in statement i with the term t. For example,

    {-1} (FORALL x: P(x)) |------- {1} ... Rule? (inst -1 "f(a)") {-1} P(f(a)) |------- {1} ... Rule?

  • (SKOLEM i "v") introduces the skolem constant (dummy name) for the for-all or there-exists variable in statement i. Example:

    {-1} (EXISTS x: NOT P(x)) |------- {1} ... Rule? (skolem -1 "A") {-1} NOT P(A) |------- {1} ... Rule?

  Arithmetic in PVS

  1. Copy the PVS source file D.pvs into a local directory and use PVS to prove all the theorems in that file. You will need to use:

     • (EXPAND "name") to expand the definitions of even? and odd?

     • (REPLACE f1 f2) To replace the left-hand side of an equality in formula f₁ with the right-hand side in formula f₂. If you need to, you can replace right-to-left using (REPLACE f1 f2 RL)

     • To prove equality formulas try (SIMPLIFY f) first. If that doesn't work, try (ASSERT)

  2. Copy the PVS source file 2/decisions.pvs into a local directory and use PVS to prove all the theorems in that file.

     All but one of the valid equalities are provable using the (ASSERT) command. Read about ASSERT in the PVS Prover Guide [PDF].

     One of the equalities is not immediately provable by ASSERT, but becomes provable after entering the command (lemma "pos_times_lt").

  Numerical Induction in PVS

  Copy the PVS source file F.pvs into a local directory and use PVS to prove all the theorems in that file.

  The command (induct v f) invokes induction on variable v in formula f. The f is optional. There is also a third argument, which names which form of induction to use, in case there are more than one.