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,X )      now do this composition
  o
   ( ( R < Y --> ident ) 
   | ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y ) )