INV: 0 <= r and x = q * y + r

GENERATING THE INVARIANT

To get INV, in this simple case, we take the condition we need after the loop (here, POST) and "subtract out" the negative of the loop boolean (here, ~(r >= y) ).

Then, we must convince ourselves "by eyeball" that out candidate INV is indeed invariant.

Check its validity just prior to loop execution for the first time: here, q = 0, r = x, so INV reduces to 0 <= x and x = x, which is true.

Now check what one loop execution does to the INV... r get smaller by y, q goes up by 1, so the effect on INV is x = (q+1)*y + (r-y) = q*y + r

So things look good... lets formalize this thinking.