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