In this example we consider a small program to divide one natural number by another, by means of repeated subtraction.
We posit a program correctness goal to the normal HOL subgoal package as
- g `^(||` { 0 < y /\ 'x = x /\ 'y = y }
r := x;
q := 0;
assert 'x = q * 'y + r /\ 0 < y /\ 'y = y
while ~(r < y) do
r := r - y;
q := ++q
od
{ 'x = q * 'y + r /\ r < 'y } /empty
`||)`;
We then invoke the verified Sunrise verification condition generator as an HOL tactic:
- et(VCGCP_TAC);
This produces the following output as a trace of the VCG's work:
By the ASSIGN rule, we have
{'x = (q + 1) * 'y + r /\ (0 < y /\ 'y = y)}
q := ++q
{'x = q * 'y + r /\ (0 < y /\ 'y = y)} /r
By the ASSIGN rule, we have
{'x = (q + 1) * 'y + (r - y) /\ (0 < y /\ 'y = y)}
r := r - y
{'x = (q + 1) * 'y + r /\ (0 < y /\ 'y = y)} /r
By the SEQ rule, we have
{'x = (q + 1) * 'y + (r - y) /\ (0 < y /\ 'y = y)}
r := r - y; q := ++q
{'x = q * 'y + r /\ (0 < y /\ 'y = y)} /r
By the WHILE rule, we have
{'x = q * 'y + r /\ (0 < y /\ 'y = y)}
assert 'x = q * 'y + r /\ (0 < y /\ 'y = y)
while ~(r < y) do r := r - y; q := ++q od
{'x = q * 'y + r /\ r < 'y} /r
with verification conditions
[('x = q * 'y + r /\ (0 < y /\ 'y = y)) /\ ~(r < y) ==>
'x = (q + 1) * 'y + (r - y) /\ (0 < y /\ 'y = y),
('x = q * 'y + r /\ (0 < y /\ 'y = y)) /\ ~(~(r < y)) ==>
'x = q * 'y + r /\ r < 'y]
By the ASSIGN rule, we have
{'x = 0 * 'y + r /\ (0 < y /\ 'y = y)}
q := 0
{'x = q * 'y + r /\ (0 < y /\ 'y = y)} /r
By the SEQ rule, we have
{'x = 0 * 'y + r /\ (0 < y /\ 'y = y)}
q := 0;
assert 'x = q * 'y + r /\ (0 < y /\ 'y = y)
while ~(r < y) do r := r - y; q := ++q od
{'x = q * 'y + r /\ r < 'y} /r
with verification conditions
[('x = q * 'y + r /\ (0 < y /\ 'y = y)) /\ ~(r < y) ==>
'x = (q + 1) * 'y + (r - y) /\ (0 < y /\ 'y = y),
('x = q * 'y + r /\ (0 < y /\ 'y = y)) /\ ~(~(r < y)) ==>
'x = q * 'y + r /\ r < 'y]
By the ASSIGN rule, we have
{'x = 0 * 'y + x /\ (0 < y /\ 'y = y)}
r := x
{'x = 0 * 'y + r /\ (0 < y /\ 'y = y)} /r
By the SEQ rule, we have
{'x = 0 * 'y + x /\ (0 < y /\ 'y = y)}
r := x;
q := 0;
assert 'x = q * 'y + r /\ (0 < y /\ 'y = y)
while ~(r < y) do r := r - y; q := ++q od
{'x = q * 'y + r /\ r < 'y} /r
with verification conditions
[('x = q * 'y + r /\ (0 < y /\ 'y = y)) /\ ~(r < y) ==>
'x = (q + 1) * 'y + (r - y) /\ (0 < y /\ 'y = y),
('x = q * 'y + r /\ (0 < y /\ 'y = y)) /\ ~(~(r < y)) ==>
'x = q * 'y + r /\ r < 'y]
By precondition strengthening, we have
{0 < y /\ ('x = x /\ 'y = y)}
r := x;
q := 0;
assert 'x = q * 'y + r /\ (0 < y /\ 'y = y)
while ~(r < y) do r := r - y; q := ++q od
{'x = q * 'y + r /\ r < 'y} /r
with additional verification condition
0 < y /\ ('x = x /\ 'y = y) ==> 'x = 0 * 'y + x /\ (0 < y /\ 'y = y)
At the end of executing the tactic, we have three normal HOL subgoals presented, expressed in the standard HOL logic. Each goal corresponds to one of the verification conditions generated.
CPU: usr: 1.760 s sys: 0.000 s gc: 0.320 s theorems: 15155
> val it =
!'x q 'y r y.
(('x = q * 'y + r) /\ 0 < y /\ ('y = y)) /\ r < y ==>
('x = q * 'y + r) /\ r < 'y
!'x q 'y r y.
(('x = q * 'y + r) /\ 0 < y /\ ('y = y)) /\ ~(r < y) ==>
('x = (q + 1) * 'y + (r - y)) /\ 0 < y /\ ('y = y)
!y 'x x 'y.
0 < y /\ ('x = x) /\ ('y = y) ==>
('x = 0 * 'y + x) /\ 0 < y /\ ('y = y)
: goalstack
These can now be solved by standard HOL techniques. Afterwards, the HOL subgoal package returns the original program correctness goal, now established as an accredited HOL theorem:
> val it =
Initial goal proved.
|- {0 < y /\ ('x = x /\ 'y = y)}
r := x;
q := 0;
assert 'x = q * 'y + r /\ (0 < y /\ 'y = y)
while ~(r < y) do r := r - y; q := ++q od
{'x = q * 'y + r /\ r < 'y} /empty : goalstack
End of example.
For the sake of brevity, many details are not explained here. More information can be found in the User's Guide (PDF).