Remainder Proof

 { PRE: x >= 0 }                
   begin

     q := 0

     r := x
     { INV: 0 <= r  and  x = q * y + r }
     while r >= y do

       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 }