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

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

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