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})

   wp(x = x-1; y = y+x, {x>=0 && y<=z})

   wp(y=x; x = 3*(x+1), {0<y<x})

   wp(y=x+1; x = 3*(y+1), {0<x<y})

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)?

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.