CSCI P415/515 Fri Jan 6 15:18:04 EST 2012 [SDJ]

Homework Assignment

Meet PVS

Familiarize yourself with the PVS Prover Guide, the PVS Language Reference and the PVS System Guide.
In particular, study the third chapter of the Prover Guide, which explains the PVS logic and its reasoing rules.


  1. The PVS source files A.pvs, B.pvs, and EQ.pvs, and have already been placed in subdirectory class/astudent/1 of your homework directory.
  2. Move to subdirectory 1 and (on a departmental Linux machine) invoke pvs5. Using PVS, prove all the theorems in each file. Further instructions, restricting what proof-commands to use, are included as comments in these source files.
  3. When you are done proving the theorems, while still in PVS, enter the command M-x prove-pvs-file to generate a buffer containing a status report. Save this buffer (using C-x C-w) under the name A.status (B.status, EQ.status respectively).
  4. PVS has now created new files, A.prf, and B.prf and EQ.prf recording the proofs you have done; and A.status, B.status and EQ.status recording the status of your work. The commands:
    1. svn add *.prf *.status – tells SVN to include these new files in the repository. You must always explicitly add new files or directories. Adding a directory also adds everything it contains.
    2. svn commit -m "any string" 1 – Causes SVN to upload everything in directory 1 (that you have previously added) to the repository.

Notes and Hints: