helphome pageduck scriptspecificationfirst proof pagepage 1 1 2 xpage 2

Implementing Stack with Pointer and Array
This proof does not succeed, because a lemma is needed.


We want to prove
      pop (< 0 , nil >) = empty
and
       ( A  : Arr  N  I  : Nat  ) top push(N , < I , A >) = N
and
       ( A  : Arr  N  I  : Nat  ) pop (< (s I) , put(N , I , A) >) = < I , A > .
Conjunction elimination yields 3 subgoals:
  1. pop (< 0 , nil >) = empty
  2. ( A  : Arr  N  I  : Nat  ) top push(N , < I , A >) = N
  3. ( A  : Arr  N  I  : Nat  ) pop (< (s I) , put(N , I , A) >) = < I , A >
    • Quantifier elimination introduces the new constant(s) a : Arr  n, i : Nat  .
    • We try to show pop (< (s i) , put(n , i , a) >) = < i , a > by reduction and circular coinduction.
      But reduction gives the following normal forms:
          < i , put(n , i , a) >
          < i , a > .
      Therefore the subgoal may be false, or may require one or more new lemmas.

And thus the main goal is not proved.

Explanation

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.


BOBJ proof scoreLeft    Up    Down    Right   
 

       This page was generated by Kumo on Tue Feb 13 19:32:22 PST 2001.