Homework #4 Solutions


***********************************************************
*                       Problem #1                        *
***********************************************************

1. Prove that I= {(x >= a) ^ (x >= 1) ^ (x <= max(1, a, b) ) }

Thus, we must prove three things to show that I is the loop invariant:
  a. I is true before the while loop
  b. I is true at the end of each iteration of the while loop
  c. I is true after the while loop completes

{True}
  x := a
{x = a} by assignment axiom
  if x<1 then
{ (x = a) ^ (x < 1) ^ (a < 1) } by def'n of "if" and transitive prop. of "<"
    x := 1
{ (x = 1) ^ (a < 1) } by assignment axiom
  endif

{ [ (x = a) ^ (x >= 1) ] OR [ (x = 1) ^ (a < 1) ] } by def'n of "if"     
{ (x >= 1) ^ (x >= a) ^ [(x = 1) OR (x = a)] } a little logic fun...
{ (x >= 1) ^ (x >= a) ^ (x <= max(1, a) } by def'n of max 
**** This is sufficient to prove part a. above ****

  while (x= 1) ^ (x >= a) ^ (x <= max(1, a) ^ (x < b) } by def'n of while
    x := x + 1
{ (x > 1) ^ (x > a) ^ (x <= b) }  application of assignement axiom
{ (x > 1) ^ (x > a) ^ (x <= max(1, a, b) ) } because (x <=b) -> (x <= max(anything, b))
*** This is sufficient to prove part b. above ***
  endwhile
*** either we went through the while or we didn't, so... ***
{ [(x >= 1) ^ (x >= a) ^ (x <= max(1, a) ^ (x >= b)] 
   OR
  [(x > 1) ^ (x > a) ^ (x <= max(1, a, b) ) ^ (x >= b)] } by def'n of while

{ [(x >= 1) ^ (x >= a) ^ (x <= max(1, a, b) )]
  OR
  [(x > 1) ^ (x > a) ^ (x <= max(1, a, b) ) ] } by def'n of max

{(x >= 1) ^ (x >= a) ^ (x <= max(1, a, b) ) }
*** this proves part c. above ***

***********************************************************
*                       Problem #2                        *
***********************************************************
Derive a proof rule for the "do" statement as defined in C:
  do S while (B)

The first important trick to this problem is that:
  "do S while (B)" is equivalent to "S; while (B) do S"

The rest is syntax.  More on the syntax soon...

***********************************************************
*                       Problem #3                        *
***********************************************************

NOTE: I am now using the word 'AND' for the obvious meaning and the symbol '^' for exponents. This may be a little confusing, but I could think of anything clever that would be more readable. Before we get started, I will tell you the loop invariant that is necessary to prove this problem:

   I = { (z > 0) AND [y >= (j-1) >= 0] AND [x = z^(j-1)] }

{z and y are positive integers }
  x := 1;
  j := 1;
{ (z > 0) AND (y > 0) AND (x = 1) AND (j = 1) }
*** Since [ y >= (1 - 1) >= 0] AND [1 = z ^ 0 ], then I is true ***
{ (z > 0) AND (y > 0) AND (x = 1) AND (j = 1) AND [x = z^(j-1)] }
  while (y >= j) do
{ (z > 0) AND (y > 0) AND [1 <= x = z^(j-1)] AND (y >= j >= 1) }
    j := j + 1;
{ (z > 0) AND (y > 0) AND [1 <= x = z^(j-2)] AND (y >= (j-1) >= 1) }
    x := x * z;
{ (z > 0) AND (y > 0) AND [1 <= x = z*z^(j-2)] AND (y >= (j-1) >= 1) }
*** Because z, x, y, and j are all non-negative, ***
*** we can make the following conclusion about multiplication and exponentiation ***
{ (z > 0) AND (y > 0) AND [1 <= x = z^(j-1)] AND (y >= (j-1) >= 1) }
*** This is sufficient to satisfy I ***
  end while loop;
*** by definition of while loops ***
{ [(z > 0) AND (y > 0) AND (x = 1) AND (j = 1) AND [x = z^(j-1)] AND (y < j)]
  OR
  [(z > 0) AND (y > 0) AND [1 <= x = z^(j-1)] AND (y >= (j-1) >= 1) AND (y < j)] }
*** [(y > 0) AND (y < j) AND (j = 1)] -> (y > 0) AND (y < 1) ***
*** Since y is an integer, the clause before the OR is unsatisfiable ***
{ FALSE OR [(z > 0) AND (y > 0) AND [1 <= x = z^(j-1)] AND (y >= (j-1) >= 1) AND (y < j)] }
*** FALSE OR X -> X ***
{ (z > 0) AND (y > 0) AND [1 <= x = z^(j-1)] AND (y >= (j-1) >= 1) AND (y < j) }
*** [ (y >= j-1) AND (y < j) ] == (j > y >= j -1) ***
*** Since y and j are integers, this means that (y = j-1) ***
*** By Substitution, we get:  x = z^(j-1)  ->  x = z^y ***
{ x = z^y }
*** Voila, our proof is done. ***