Homework 3 - Axiomatic semantics and invariants

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

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

   x = x+1 {0<=x+y<z}

   x = x-1; y = y+x {x>=0 && y<=z}

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

   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. Be sure to show that the invariant holds the first time the loop test is reached as well as each subsequent time. For this problem write out the necessary assertions 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 a 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. We will go over this in class. 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 (I)? What is the boolean test (B)? You must show, using the statement sequence rule that your claimed invariant actually is an invariant for your loop.