Mills Example: Quotient Program

Consider this program specification:

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

Consider this program P:

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

Show that program P is correct w.r.t the spec r