Homework Assignment 5: Program Correctness 

WARNING.  This homework may take LONGER than the last several, so
please work on it ahead of time.

Assigned, Thursday October 5
     Due, Thursday October 12

To prove an iterative program is correct:

 (1) Clearly state the loop invariant P that you will use.
 (2) use induction to prove that P is an invariant
        prove it is true before the first loop iteration (the base case)
              prove that if the loop continues then it is true after the loop.
 (3) Use the loop invariant to prove the program partially correct for
     the given initial and final assertions.
 (4) Prove that the program terminates.

 (*) If you are having trouble with step 1, it may help to trace the loop for
     several different inputs.

 (**) If you are having trouble with step 2, maybe there is a
     different loop invariant P that you should be using?

*********Practice Exercises*************

Book Problems: 3.5 (or, section 4.5 in the sixth edition), #4, #13

3. Use a loop invariant to prove that the following program is correct
with respect to the initial assertion that x is a positive integer and
the final assertion that ans = x2.

procedure square(x)
  i = 1
  j = 1 
  while (i < x) do
    j = j + 2i + 1 
    i = i + 1 
  od
  return j

***********Problems to Submit*********

1. Prove the correctness of the following iterative program
 for finding the nth Fibonacci number with respect to the initial
 assertion n >= 0 and the final assertion that y is the nth Fibonacci
 number, f(n).  
 Recall f(0) = 0, f(1) = 1 and forall n > 1, f(n) =  f(n-1) + f(n-2)

procedure fibonacci(n)

if (n==0)
  y = 0 
else
  x = 0 
  y = 1 
  i = 1
  while i < n do
    i = i + 1
    z = x + y 
    x = y 
    y = z
  od
fi
return y

 


2.  Prove that the following algorithm to compute the maximum value in
an array A[1..n] is correct, with respect to the initial assertion
that A has n elements, and the final assertion that x is the maximum
of the element A[1], A[2], ... A[n].

function max(A)
   x = A[1]
   for i = 2..n do
     if A[i] > x
        x = A[i]
     fi
   od

 


(3) Use the idea of the "fast exponentiation" algorithm discussed in
class to make a "fast multiplication" algorithm that returns the
product of (x,y) and uses only "plus", "minus", and "divide by 2 (that
works only for even numbers)".  Your program should be faster than one
that repetively adds x to itself y times.  (or y to itself x times).