2. (Invariants) [25 points]
Prove the partial correctness of the program below with respect to the input and output assertions shown (all variables are integer).
Input assertion: x == a && y == b && y >= 0
z = 0;
while( y > 0 )
{
z = z + x;
y = y - 1;
}
Output assertion: z == a * b