ANOTHER EXAMPLE

Prove the correctness of the following
program:

{input1 > 0 and input2 > 0}
read(z); read(y);
x := 1;
j := 1;
while y >= j loop
j := j+1;
x := x * z;
end loop;
write(x);
{output = input1 ** input2}