2. (Invariants) [25 points]

  Input assertion: x == a && y == b && y >= 0

z = 0;
while( y > 0 )
{
  z = z + x;
  y = y - 1;
}

  Output assertion: z == a * b

We first prove that the two statements

(1) y >= 0
(2) z = (b-y)*a

are loop invariants.

To show this is true in the base case, substitute
the values of y==b and z==0 into the second statement
above. The first is a direct
restatement of an input assertion.

Now, suppose the two loop invariants hold true at some
point in the program's execution AND that control
returns to the loop test. Distinguish the more recently assigned
variables from the previous iteration's with a prime, so that
the new loop invariant would be

  y' >= 0     and    z'=(b-y')*a
  
We want to show that the above two statements hold, given
the inductive hypothesis:

  y >= 0      and    z = (b-y)*a
  
and the fact that the loop test was failed and
the body of the loop was executed, i.e.,

  y > 0   and   z' = z + x   and  y' = y-1
  
Proof:

  First we show statement 1. The assertion y>0
  implies that y-1>=0 because all values are integral.
  Since y' = y-1, it follows that y' >= 0.
  
  Second we show statement 2. Replacing z in the
  assertion z' = z + x with its value in z = (b-y)*a
  yields
  
     z' = (b-y)*a + x 
     
  But x=a, so that
  
    z' = (b-y)*a + a = (b-y+1)*a = (b-(y-1))*a = (b-y')*a,
    
  which is what we wanted to show.
  
Finally, consider the value of  z when the loop ends.
In that case the loop test must be false, so that
!(y > 0), which implies y<=0. Because of the loop invariant
y >= 0, we know that y = 0. Because of the loop invariant
z = (b-y)*a, along with y=0, we have z = b*a, which is
what we wanted to show.