CSci 420/520: Homework 3

Proving in PVS I

Due Wednesday, September 21st by 1pm.

Summary

This assignment will get you started with PVS in Emacs, introducing you to the editor and some of its basic features.

You can find the PVS documentation at http://pvs.csl.sri.com/documentation.shtml, and on the course webpage.

Make sure you have PVS running as described in the tools setup document.

Opening a Theory

PVS stores specifications in .pvs files, which it locates in its working context. The context defaults to the directory in which pvs was executed.

In Emacs, M- refers to the "meta" key, which is usually Esc, but sometimes Alt. So M-x may mean press "Esc" then "x".

1. If your context isn't the work directory your created earlier, type M-x change-context to change it. (Note that Emacs has tab completion.)
2. Download proving1.pvs and save it in your work directory.
3. Open the file proving1.pvs.

Typechecking and Proving in PVS

Type M-x tc to perform type-checking of the whole document. This is to check for syntactic mistakes in the PVS program, and verify any type check constraints. If PVS cannot automatically verify that all types are being used correctly, it will generate type correctness conditions (TCCs) that you will need to prove.

1. Type check the document. Initially no TCCs will be generated.
2. In Section 1, uncomment the two error lemmas, and type check the document again. Fix the problems so that it type checks correctly.
3. Prove all of the lemmas in Section 2 using only the flatten, split, and assert commands described in class.

A PVS theory is analogous to a program. To verify that a theory is correct, you have to prove the corresponding conjectures, lemmas that are based on the functions in your theory are correct. To prove a particular statement, move the curser to the statement you want to prove and then type M-x pr to start the proof. Now you will see the PVS prompt, Rule?, in the lower window. Issue PVS commands here. PVS will automatically terminate when the proof is done.

Grading

100 points total.

PVS will create a proving1.prf file to store your proofs. Make sure none of the proofs are "unfinished", and then email this file along with your proving1.pvs file to meghan@cs.wm.edu. (We will need the .pvs file to check your modified error lemmas.)