Remainder Proof

 { PRE: x >= 0 }            
   begin

     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

   end
 { POST: 0 <= r < y  and  x = q * y + r }