Source Code (for reference)

Program P

   Q := 0
   R := X
   while R>=Y do
      Q := Q + 1
      R := R - Y
   end

Specification r

r(X,Y,Q,R) = { ( X, Y, X/Y, X mod Y ) | X >= 0 and Y > 0 }