{ PRE: x >= 0 }
begin
q := 0
r := x
{ INV: 0 <= r and x = q * y + r }
while r >= y do
{ P2: 0 <= (r-y) and x = (q+1) * y + (r-y) }
r := r - y
{ P1: 0 <= r and x = (q+1) * y + r }
q := q + 1
{ INV: 0 <= r and x = q * y + r }
end
end
{ POST: 0 <= r < y and x = q * y + r }
