Homework 2 - Axiomatic semantics and invariants

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

4. Change the program for integer square roots handed out in class so that if n has an exact square root the program terminates with {L**2=n} otherwise {L=-1}. You don't have to write out the assertions formally but explain why our program works using the ideas of axiomatic semantics. You do have to write the program using binary search as was done in the example -- no taking shortcuts using sqrt(), for example.