{ PRE: x >= 0 } begin { P4: 0 <= x and x = 0 * y + x } q := 0 { P3: 0 <= x and x = q * y + x } 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 { P5: 0 <= r and x = q * y + r and ~(r >= y) } end { POST: 0 <= r < y and x = q * y + r }