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