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 + 
    z = x + y 
    x = y 
    y = z
  od
fi
return y
 0"
  loop invariant: x = f(i-1), y = f(i)

  before the loop iteration when i = 1:
    x = 0 = f(1-1)= f(0);
    y = 1 = f(1)

  Assume loop iteration true after interation i
   Prove it is true after interation i+1
       Assume: x=f(i-1), y = f(i)  
       loop execution does the following:
        i' = i+1;
        y' = x+y
        x' = y
       so 
        x' = f(i) = f(i' - 1);
        y' = f(i) + f(i-1) = f(i+1) = f(i')
       so the loop maintains the invariant.
   after loop stops, value of i is n
   and by loop invariant y = f(i)
  so when program ends, y = f(n)

The program terminates because the loop executes exactly n times, and n is a positive integer.


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

 
Loop invariant: x is the max of A[1..i]

The for loop is equivalent to the statements:

i = 1
while i < n
  i = i+1
  if A[i] > x
      x = A[i]
  fi
od

1. So before the loop starts, i = 1, and x = A[1] so x is the max (and
only element) of A[1..1].

2. Prove L {loop code} L
Assume x = max(A[1..n])

after loop i' = i+1, and there are two cases for x.

case 1, x > A[i'],
  x does not change, but x is already the max of A[1..i']

case 2, x < A[i'], 

  x does change, the new value x' is set to A[i'].

  This is the max of A[1..i'] because A[i'] is greater than x (because
  where are in this case), and x is the max of A[1..i].

3. At the end of the loop, i = n, so x is the max of A[1..n].

4. The loop stops because i is incremented once each time through the
loop and stops when it gets to n.






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).  Your program should be faster than one that
repetively adds x to itself y times.  (or y to itself x times).
(a) write down your program
(b) Prove that your algorithm is correct.
 

multiply(x,y)

a = x;
b = y;
answer = 0;
while b > 0 do
  if b is even
    a = a + a;
    b = b/2;
  else
    answer = answer + a;
    b = b-1;
  fi
od

(1b) Prove that your algorithm is correct.

First, lets break the code up into chunks.

S1 = "a = x;
      b = y;
      answer = 0"

loop = everthing between "while" and "od".

loopOne = "a = a + a;
           b = b/2;"

loopTwo = "answer = answer + a;
           b = b-1;"


ok... So, the preconditions should be:

P <==> "x, y are positive integers."

then our loop invariant:

L <==> answer + a*b = x*y

So, lets prove our step by step thing, starting with the precondition:

P {S1} L:

  Well, S1 assigns answer = 0, a = x, and b = y.  So
 
  answer + a * b =   0 + x * y = x * y.  weehaa!

Next, lets prove that L {loop} L
 
  we need to do this with two cases (because there is an if statement
  in the loop).


  Assume L is true before the loop, ( so "answer + a * b = x * y" ).


  Case One: b is even.
    After the loop, a' = a+a, and b' = b/2.
      So, answer + a' * b' =
          answer + (a+a) * b/2 = 
          answer + 2*a * b/2 = 
          answer + a * b = ... and from above, we assume this is x * y.

  Case Two:
    After the loop, answer' = answer + a, and b' = b-1.
      So, answer' + a * b' =
          (answer + a) + a * (b-1) = 
          (answer) + a + a * (b-1) = 
          (answer) + a (1 + (b-1)) = 
          (answer) + a (    b    ) = 
          answer + a * b = ... and from above, we assume this is x * y.

so in either case, L { loop } L.

Finally, we need to prove that (L and not (b > 0)) --> answer = x*y.
  So, when the loop ends, it ends because b is no longer greater than
  zero.  In this case b = 0.  So, becase L is true, 

  answer + a * b = x * y,    but, since the loop is over, b = 0, so:
  answer + a * 0 = x * y,
  answer         = x * y,  

  which is what we should, long ago, have claimed as our final
  assertion.

Lastly, we need to argue that the loop always ends.  In either case
(when b is even or odd), the value of b decreases by at least 1.
Therefore, eventually the loop stops.