CSci 420/520: Homework 4

Proving in PVS II

Due Wednesday, September 28th by 1pm.

Summary

This assignment will introduce you with the commands needed to prove more complicated theories.

Program Modeling and Proving

In programming, you develop a program that tells the computer how to perform some computation. The properties that describe what that computation does are implicit. In contrast, specifications define what the software is supposed to do, but not how it should be done.

PVS provides a large number of features for modeling software and then proving that the model has desirable properties. In the next homework we will focus on abstract data types. In this homework we will focus on function. The main idea is to use PVS to specify the functions of the software, their arguements, return types and so on, then verify that the functions have desirable properties. As we prove the correctness of the functions with respect to these conjectures, we gain confidence that they are correct.

As we prove lemmas and theorems, we can use them to prove more complicated theorems. Typically we start with axioms are are assumed to be true, and build up our theory in terms of lemmas and theorems. Before we move on to learning how to write good models and theorems, we first need to learn how to use functions and lemmas in proofs. For this assignment, do not try to prove the functions and lemmas. Assume that these are correct and prove the theorems and conjectures.

Instructions

Download proving2.pvs and save it in your work directory.

For Section 1, you are asked to prove theories using the given lemmas. For this assignment, try to look at which lemma to apply to the proof and when to introduce them. PVS does not stop you from introducing needless lemmas, but incorrect introduction of lemmas does slow down the proof commands. (Note: you can use the hide command to remove irrelevant portions of a sequent to increase the speed of PVS commands.)

Section 2 of the homework is closer to what you will need to model your software. The model is one of introducing phone numbers into a directory. Here, we specified some functions for our program and then we use theorems to verify that our functions perform as we expected.

There are multiple ways of proving these problems, using different lemmas or functions in different orders will yield different solutions. Feel free to try different methods, but you need only submit one solution. The .prf file will contain the proof steps when you save the file or upon successful completion of a proof. Please do not submit incorrect proofs together with correct ones.

Grading

150 points total

Make sure none of the proofs are "unfinished", and then email your proving2.prf file to meghan@cs.wm.edu.