Proof Example 1: Remainder Program

Consider this program: it computes a remainder

   { 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 }