EXAMPLE (continued)

{input1 > 0 and input2 > 0}
read(x); read(y);
div := 0;
while x >= y loop
div := div + 1;
x := x - y;
end loop;
{input1 = div * input2 + x and
0 =< x < input2}

We need a LOOP INVARIANT. An obvious choice is:

L1: {input1 = div * y + x}

Backward substition shows L1 is an invariant, because going back through the loop yileds L1 again.

{input = (div+1) * y + (x-y)}