Proof: Quotient Program

Specification:

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

   ( X,Y,Q,R := X,Y,0,R ) o      function for assignment statement
   [R := X] o                    is a concurrent assignment 
   [while R>=Y do
       Q := Q + 1
       R := R - Y
    end]