Homework 3 - Axiomatic semantics and invariants

Here is some practice with the techniques of axiomatic semantics and invariants. Due in class October 23.

1. Determine the weakest precondition for the given statements and postconditions (each line is a separate problem). Show the intermediate step(s) for the compound statements.

   wp(x = x+1, {0<=x+y<z}) Answer: {0<=x+1+y<z}

   wp(x = x-1; y = y+x, {x>=0 && y<=z}) Answer: wp(x = x-1, {x>=0 && y+x<=z}) thus {x-1>=0 && y+x-1<=z};
   make sure to substitute for the assigned-to variable *every* time it appears in the postcondition.

   wp(y=x; x = 3*(x+1), {0<y<x}) Answer:    wp(y=x, {0<y<3*(x+1)}) thus {0<x<3*(x+1)}.
   Simplify to {0<x}

   wp(y=x+1; x = 3*(y+1), {0<x<y}) Answer: wp(y=x+1, {0<3*(y+1)<y}) thus {0<3*(x+1+1)<x+1}.
   Simplify to {0<3*x+6<x+1} which is false -- there are no such states.

2. In this program

   s = 0;
   n = 1;
   while x > 0 do
      s = s+n;
      n = n + 2;
      x = x - 1;
   end

show that {s=((n-1)/2)**2} is an invariant of the loop by showing that {x > 0 and s=((n-1)/2)**2} => wp(the loop body, {s=((n-1)/2)**2}) For this problem write out the argument using formal, mathematical notation. From the invariant and the loop test what can you conclude about the state at the completion of the loop (after the last iteration)?

Answer: Part 1: show that the given formula is an invariant by showing

{x > 0  and s=((n-1)/2)**2} => wp(s=s+n; n=n+2; x=x-1, {s=((n-1)/2)**2})
which by the sequence and assignment rules is 
{x > 0  and s=((n-1)/2)**2} => wp(s=s+n; n=n+2, {s=((n-1)/2)**2})
which by the sequence and assignment rules is 
{x > 0  and s=((n-1)/2)**2} => wp(s=s+n, {s=((n+1)/2)**2})
which by the assignment rules is 
{x > 0  and s=((n-1)/2)**2} => s+n=((n+1)/2)**2}
which by algebra is true.

Part 2: what can we conclude when the loop exits:

The invariant and not the loop test, thus
{s=((n-1)/2)**2} and x<=0}
Note here that we did not choose a strong enough invariant to relate the final value of s to the final 
value of x. Can you strengthen the invariant (by adding another conjunct) so that you can show that
when the loop finishes s contains the square of the initial value of x?

3. Write code to calculate the integer quotient of two positive integers n, the dividend, and k, the divisor. Use repeated subtraction; do NOT use the / operator. Assume n and k are both > 0. The answer is to be in variable q

One key to this kind of problem is determining how to express the post-condition that is to be achieved. Once you know the postcondition think about the loop test and the invariant and how you will write the code. What is the postcondition? What will you try to use as the loop invariant? What is the boolean test? You must show, as in problem 2, that your claimed invariant actually is an invariant for your loop.

Answer: the integer quotient of n divided by k (positive n and k) is a number q such that (*) n=q*k+r for some r where (**) 0<=r<k. Observe that if r is initialized to n and q is initialized to 0 then (*) holds and so does the left part of (**) but the right half of (**) does not. We can try making (*) and {0<=r} our invariant and making r>=k our loop test. The obvious code then is

r=n
q=0
while r>=k {
   q=q+1;
   r=r-k;
}

and the proof goes like
First, show that 

r>=k and n=q*k+r => wp(q=q+1; r=r-k, {n=q*k+r and 0<=r})
which by sequencing and assignment rules is
r>=k and n=q*k+r => wp(q=q+1; {n=q*k+r-k and 0<=r-k})
which by the assignment rule is
r>=k and n=q*k+r => {n=(q+1)*k+r-k and 0<=r-k}
which is true by simple algebra.
Thus we have chosen a good invariant.
Since the initialization ensures the invariant is true when the
loop starts (because n=0*k+n) we can conclude that when the
loop finishes n=q*k+r and 0<=r and r<k which is exactly
what the definition of the quotient requires.

It's interesting to me that when I first wrote down the code for this solution I wrote r=r-n for the second statement in the loop. I discovered the mistake when I reached the last line of the "this is an invariant" proof where it was obvious that the implication did not hold.