Source Code (for reference)
Program P
Q := 0 R := X
while
R>=Y
do
Q := Q + 1 R := R - Y
end
Specification r
r(X,Y,Q,R) = { ( X, Y, X/Y, X mod Y ) | X >= 0 and Y > 0 }