EXAMPLE (continued)

First, we use backward substitution:

{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}