Remainder Proof

 { PRE: x >= 0 }
   begin

     q := 0

     r := x

     while r >= y do

       r := r - y

       q := q + 1

     end

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