ANOTHER EXAMPLE (continued)

First, by backward substition we obtain,

{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;
{x = input1 ** input2}

L1 { x = z ** (j-1) } is invariant because
substituting backward through the loop
{ x * z = z ** j }
yields again L1