Quotient Program: Proof Plan
The spec r is
r(X,Y,Q,R) = { ( X, Y, X/Y, X mod Y ) | X >= 0 and Y > 0 }
The program P is
Q := 0
R := X
while R>=Y do
Q := Q + 1
R := R - Y
end
We will decompose this as
[Q:=0] o [R:=X] o [WHILE]
Steps:
- find [WHILE]
- guess function f such that f = [WHILE]
- use Mills' theorem to verify your guess:
- show ( ~b --> f ) = ( ~b --> identity )
- show dom(f) = dom([WHILE]) (a termination argument)
- show f = [IF] o f where IF is composed of loop components
- determine the restriction on [WHILE] made by the initial assignments
to get [P]
[P](X,Y,Q,R) = [WHILE]([Q:=0;R:=X](X,Y,Q,R))
= [WHILE](X,Y,0,X)
- show that the program implements the spec, i.e., r subset [P]