Assignment 3: Software Verification

Important Information

The Problem

Your assignment is to prove the following Hoare logic assertion in HOL:

{x = X & y = Y}
w := 0;
z := y;
while !(w = x) (
  w := w + 1;
  z := z + 1
)
{z = X + Y}

(w, x, y and z are program variables and X and Y are constants)

Step 1: Construct a Formal Semitics for the Language

You will need to construct a formal semantics for this programming language in HOL. The semantics will be similar to the semantics you developed for the the language without while loops in Exercise 12, but you will need to model commands as relations between states rather than functions from states.

Hint: It might make things easier if you define a series of auxiliary functions SKIP, GETS, IF, SEQ and WHILE to help capture the meanings of individual commands. You can then define the meaning function on commands in terms of these.

Hint: The hardest of these auxiliary functions to define will be WHILE. One way to approach this is to define a further auxiliary function UNDEF, such that for all states s and t, UNDEF s t is false. You can then define WHILE b c as the limit of the following series of approximations:

UNDEF
IF b (SEQ c UNDEF) SKIP
IF b (SEQ c (IF b (SEQ c UNDEF) SKIP)) SKIP
IF b (SEQ c (IF b (SEQ c (IF b (SEQ c UNDEF) SKIP)) SKIP)) SKIP
...

Step 2: Prove the Hoare Logic Properties

Prove the Hoare logic properties of each of the commands in your language. Most of the proofs will be similar to the proofs you performed in Exercise 13.

Hint: The hardest property to prove will be the one for while loops, which is as follows:

!P B C Q. ({P & B} C {P}) /\ ({P & !B} skip {Q}) ==> ({P} while B C {Q})

This proof must be completed by induction, and the steps leading up to the introduction of the induction are critical to its successful completion. The proof begins by rewriting with the definitions of your Hoare logic construct and the meanings of the various language constructs. You will then have a term in which the original while loop has been replaced by its meaning in terms of the limit of a series of approximations. The limit operation takes the form of an existential quantification, and this quantification should be moved out to the very front of the goal. You can move the quantification outwards using RIGHT_AND_EXISTS_CONV and LEFT_IMP_EXISTS_CONV, this last conversion will transform the existential quantification into a universal quantification. Using these conversions you should be able to move the quantification outwards to the point where the only things before it are other universal quantifications. You must also move the quantification past these, which can be achieved using a combination of GEN_TAC and SPEC_TAC. (You must finish up with the all same quantifications as before, just in a different order!) You can then proceed by induction on this variable.

Step 3: Prove the Loop

This proof is relatively straight forward. The most important advice to give you is to make sure that you chose the intermediate assertions introduced when you decompose the sequential compositions such that the assertion established just prior to the loop is its invariant.

Hint: If this is a bit hard at the first attempt, then perhaps you should warm up to it with an easier proof like the following:

{x = X & y = Y}
t := x;
x := y;
y := t
{x = Y & y = X}

What to Submit

You should prepare your solution as a well commented sml program in a file called a3.sml. Submit your solution by mailing it to me as an attachment.