|page 1||1 2 x|
We want to prove
pop (< 0 , nil >) = emptyConjunction elimination yields 3 subgoals:
And thus the main goal is not proved.
The first rule applied here is conjunction elimination, resulting in three subgoals. The first succeeds by circular coinduction and the second by reduction, but the third fails under both methods. Hence we do not know whether this subgoal is true or not, but rather that these methods failed to yield a proof.
However, Kumo has provided us with some additional information, namely that we need to prove that
< i, put(n,i.a)> = < i, a > .This is a special case of a a more general lemma, which says that placing new information above the pointer does not effect behavior, and as shown in the second proof page, this lemma does the trick for our third subgoal.
Note that the first and third STACK equations are not satisfied in the strict equational sense by the pointer-array theory; here we already know that the first is behaviorally satisfied, and the next proof page will show that the third is also behaviorally satisfied. The webpages for the flag proof includes a general discussion and exemplification of the importance of behavioral properties in software verification.
A different proof of this behavioral refinement was given in A Hidden Agenda, using
an explicit coinduction with some subtle complications, including a recursive
definition of the candidate relation.