# 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