Homework 3 - Axiomatic semantics and invariants

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

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. Some problems involving repeated actions are naturally solved using invariants. Here is a classic: suppose you remove two diagonally opposite corners of a chessboard. Note that those two squares are the same color. Now place rectanges on the board with each rectangle covering exactly two horizontally or vertically adjacent squares. Can you completely cover the mutilated chessboard using these rectangles? To answer the question find and state an invariant property of the board as it is gradually covered with rectangles. (Just state the invariant as an English sentence -- you don't have to formalize it in mathematics.) When no more rectangles can be placed (i.e. the loop exits) what can you conclude about the coverage of the board.

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

4. 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.