Urban Hafner

CTM: Exercise 3-6

Posted by Urban Hafner Wed, 14 Sep 2005 19:25:26 GMT

The problem

State invariants. Write down a state invariant for the IterReverse function.

My solution

Define the state invariant P as follows:

P((Rs,Ys)) = (reverse(Xs) = reverse(Ys)|Rs)

• The proof for P_(_S_{0~) follows from S}0~ = (nil,Xs).
• Assuming P_(_S_{i~) and S_}i~ is not the final state, prove _P(S__i+1). This follows from the semantics of the case statement and the function call. Write _S_{i~ = (Rs,Ys). We are not in the final state, so Ys is of nonzero length. From the semantics, Y|Rs adds one element to Rs and the case statement removes this element from Ys. Therefore P_(_S}i+1~) holds.

As you might have noticed I’ve used the proof for IterLength and just changed the bits concerning the state invariant. This is OK because the two functions are nearly the same.