Stack with Pointer-Array

Implementing Stack with Pointer and Array

We prove that the common way of implementing a stack with a pointer plus an array is correct, by treating it as a behavioral refinement problem. The specification and proof use the builtin specification for NAT, which includes definitions for the inequality relations used, as well as for the function eq, which conservatively returns true or false only when it can actually prove them, and otherwise returns the computed normal form, in contrast to the less safe builtin operation ==, which returns false when it cannot prove equality.

The proof score first defines stack, then defines the pointer-array implementation, and then gives the proof. The correct cobasis to use in proving that the implementation behaviorally refines the specification is that of STACK, which contains only top and pop. This cobasis is selected for the proof by the command set cobasis of STACK. We repeatedly run both "red" (for behavioral rewriting) and "cred" (for circular coinductive rewriting), in order to determine whether or not each result is really coinductive.

The initial attempt to prove the stack equations of the implementation fails for one equation, but the way it fails suggests a lemma, which indeed allows the proof to complete. This lemma is proved by induction, and the output shows that both its basis and its induction step require coinduction. Moreover, a circularity occurs in the base case proof, as signalled by occurrence of the keyword "deduced" in the output, which is followed by the names of the equation used circularly. Section 1 below gives the BOBJ source code, and Section 2 gives its output. Sections 3 and 4 go over the same ground for parameterized versions of the same specifications, but with all the unnecessary computations omitted. These examples are due to Joseph Goguen with significant help from Kai Lin.


1. BOBJ Source Code

*** file: /groups/tatami/bobj/examples/stack.bob ***> implementing stack with pointer and array *** the source specification bth STACK is sort Stack . pr NAT . op empty : -> Stack . op push : Nat Stack -> Stack . op top_ : Stack -> Nat . op pop_ : Stack -> Stack . var N : Nat . var S : Stack . eq top push(N,S) = N . eq pop push(N,S) = S . end show cobasis . bth ARRAY is sort Arr . pr NAT . op nil : -> Arr . op put : Nat Nat Arr -> Arr . op _[_] : Arr Nat -> Nat . vars I J : Nat . var A : Arr . var N : Nat . cq put(N, I, A) [J] = N if eq(I, J) . cq put(N, I, A) [J] = A [J] if not eq(I, J) . end show cobasis . *** the implementation bth STACKIMP is pr (NAT || ARRAY) * (sort Tuple to Stack) . op empty : -> Stack . op push : Nat Stack -> Stack . op top_ : Stack -> Nat . op pop_ : Stack -> Stack . vars I J : Nat . var A : Arr . var N : Nat . eq empty = <0, nil>. eq push(N, <I, A>) = <s I, put(N, I, A)> . eq top <0, A> = 0 . eq top <s I, A> = A [I] . eq pop <s I, A> = <I, A> . eq pop <0, A> = <0, A> . end show cobasis . *** check the stack equations: set cobasis of STACK set cred trace on . red top push(N, <I, A>) == N . red pop push(N, <I, A>) == <I, A> . cred pop push(N, <I, A>) == <I, A> . red pop push(N, <I, A>). *** this suggests the lemma that we need: *** lemma by induction on I: <I, put(N, J, A)> = <I, A> if I <= J open . *** base case red <0, put(N, J, A)> == <0, A> . cred <0, put(N, J, A)> == <0, A> . *** induction step ops i j : -> Nat . eq i < j = true . cq <i, put(N,J,A)> = <i,A> if i <= J . red <s i, put(N, j, A)> == <s i, A> . cred <s i, put(N, j, A)> == <s i, A> . close open STACKIMP . *** assert the lemma: vars I J : Nat . var A : Arr . var N : Nat . cq <I, put(N,J,A)> = <I, A> if I <= J . *** prove the equations: red top push(N, <I, A>) == N . red pop push(N, <I, A>) == <I, A> . cred pop push(N, <I, A>) == <I, A> . close

2. BOBJ Output

awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.208 built: Tue Nov 19 12:11:59 PST 2002 University of California, San Diego Tue Nov 19 13:39:58 PST 2002 BOBJ> in stack ========================================== ***> implementing stack with pointer and array ========================================== bth STACK ========================================== The cobasis for Stack is: op top _ : Stack -> Nat [prec 15] op pop _ : Stack -> Stack [prec 15] ========================================== bth ARRAY ========================================== The cobasis for Arr is: op _ [ _ ] : Arr Nat -> Nat [prec 41] op put : Nat Nat Arr -> Arr ========================================== bth STACKIMP ========================================== The cobasis for Stack is: op top _ : Stack -> Nat [prec 15] op pop _ : Stack -> Stack [prec 15] op push : Nat Stack -> Stack ========================================== set cobasis of STACK ========================================== reduce in STACKIMP : top push(N, < I , A >) == N result Bool: true rewrite time: 5ms parse time: 7ms ========================================== reduce in STACKIMP : pop push(N, < I , A >) == < I , A > result Bool: false rewrite time: 5ms parse time: 11ms ========================================== c-reduce in STACKIMP : pop push(N, < I , A >) == < I , A > using cobasis of STACKIMP: op top _ : Stack -> Nat [prec 15] op pop _ : Stack -> Stack [prec 15] --------------------------------------- reduced to: < I , put(N, I, A) > == < I , A > ----------------------------------------- add rule (C1) : < I , put(N, I, A) > = < I , A > ----------------------------------------- target is: < I , put(N, I, A) > == < I , A > expand by: op top _ : Stack -> Nat [prec 15] reduced to: top (< I , put(N, I, A) >) == top (< I , A >) ----------------------------------------- result: false c-rewrite time: 64ms parse time: 17ms ========================================== reduce in STACKIMP : pop push(N, < I , A >) result Stack: < I , put(N, I, A) > rewrite time: 4ms parse time: 4ms ========================================== open ========================================== reduce in STACKIMP : < 0 , put(N, J, A) > == < 0 , A > result Bool: false rewrite time: 1ms parse time: 14ms ========================================== c-reduce in STACKIMP : < 0 , put(N, J, A) > == < 0 , A > using cobasis of STACKIMP: op top _ : Stack -> Nat [prec 15] op pop _ : Stack -> Stack [prec 15] --------------------------------------- reduced to: < 0 , put(N, J, A) > == < 0 , A > ----------------------------------------- add rule (C1) : < 0 , put(N, J, A) > = < 0 , A > ----------------------------------------- target is: < 0 , put(N, J, A) > == < 0 , A > expand by: op top _ : Stack -> Nat [prec 15] reduced to: true nf: 0 ----------------------------------------- target is: < 0 , put(N, J, A) > == < 0 , A > expand by: op pop _ : Stack -> Stack [prec 15] deduced using (C1) : true nf: < 0 , A > ----------------------------------------- result: true c-rewrite time: 43ms parse time: 14ms ========================================== ops i j : -> Nat ========================================== eq i < j = true ========================================== cq < i , put(N, J, A) > = < i , A > if i <= J ========================================== reduce in STACKIMP : < (s i) , put(N, j, A) > == < (s i) , A > result Bool: false rewrite time: 4ms parse time: 19ms ========================================== c-reduce in STACKIMP : < (s i) , put(N, j, A) > == < (s i) , A > using cobasis of STACKIMP: op top _ : Stack -> Nat [prec 15] op pop _ : Stack -> Stack [prec 15] --------------------------------------- reduced to: < (s i) , put(N, j, A) > == < (s i) , A > ----------------------------------------- add rule (C1) : < (s i) , put(N, j, A) > = < (s i) , A > ----------------------------------------- target is: < (s i) , put(N, j, A) > == < (s i) , A > expand by: op top _ : Stack -> Nat [prec 15] reduced to: true nf: A [i] ----------------------------------------- target is: < (s i) , put(N, j, A) > == < (s i) , A > expand by: op pop _ : Stack -> Stack [prec 15] reduced to: true nf: < i , A > ----------------------------------------- result: true c-rewrite time: 63ms parse time: 18ms ========================================== close ========================================== open STACKIMP ========================================== vars I J : Nat ========================================== var A : Arr ========================================== var N : Nat ========================================== cq < I , put(N, J, A) > = < I , A > if I <= J ========================================== reduce in STACKIMP : top push(N, < I , A >) == N result Bool: true rewrite time: 5ms parse time: 5ms ========================================== reduce in STACKIMP : pop push(N, < I , A >) == < I , A > result Bool: true rewrite time: 9ms parse time: 10ms ========================================== c-reduce in STACKIMP : pop push(N, < I , A >) == < I , A > using cobasis of STACKIMP: op top _ : Stack -> Nat [prec 15] op pop _ : Stack -> Stack [prec 15] --------------------------------------- result: true c-rewrite time: 2ms parse time: 10ms ========================================== close BOBJ> q Bye. awk%

3. BOBJ Code for Parameterized Stack

Note that the interface theory for the parameterized specifications requires that a constant be supplied in actual parameters. This constant is used to give a value for the top of the empty stack in the implementation; it is needed in the base case of the proof of the lemma. Note also that choosing the name "0" for the constant means that it will be mapped to 0 in NAT if these modules are instantiated with NAT. For consistency, one might want to also say that the top of the empty stack has value 0 in the source specification STACK, but this is not necessary. *** file: /groups/tatami/bobj/examples/stack1.bob ***> implementing stack with pointer and array th TRIV* is sort Elt . op 0 : -> Elt . end *** the source specification bth STACK[X :: TRIV*] is sort Stack . op empty : -> Stack . op push : Elt Stack -> Stack . op top_ : Stack -> Elt . op pop_ : Stack -> Stack . var E : Elt . var S : Stack . eq top push(E,S) = E . eq pop push(E,S) = S . end bth ARRAY[X :: TRIV*] is sort Arr . pr NAT . op nil : -> Arr . op put : Elt Nat Arr -> Arr . op _[_] : Arr Nat -> Elt . vars I J : Nat . var A : Arr . var E : Elt . cq put(E, I, A) [J] = E if eq(I, J) . cq put(E, I, A) [J] = A [J] if not eq(I, J) . end *** the implementation bth STACKIMP[X :: TRIV*] is pr (NAT || ARRAY[X]) * (sort Tuple to Stack). op empty : -> Stack . op push : Elt Stack -> Stack . op top_ : Stack -> Elt . op pop_ : Stack -> Stack . vars I J : Nat . var A : Arr . var E : Elt . eq empty = <0, nil>. eq push(E, <I, A>) = <s I, put(E, I, A)> . eq top <0, A> = 0 . eq top <s I, A> = A [I] . eq pop <s I, A> = <I, A> . eq pop <0, A> = <0, A> . end set cobasis of STACK set cred trace on . *** lemma by induction on I: <I, put(N, J, A)> = <I, A> if I <= J open . *** base case cred <0, put(E, J, A)> == <0, A> . *** induction step ops i j : -> Nat . eq i < j = true . cq <i, put(E,J,A)> = <i,A> if i <= J . cred <s i, put(E, j, A)> == <s i, A> . close open STACKIMP . *** assert the lemma: vars I J : Nat . var A : Arr . var E : Elt . cq <I, put(E,J,A)> = <I, A> if I <= J . *** prove the equations: red top push(E, <I, A>) == E . red pop push(E, <I, A>) == <I, A> . close

4. BOBJ Output

awk% bobj \|||||||||||||||||/ --- Welcome to BOBJ --- /|||||||||||||||||\ BOBJ version 0.9.208 built: Tue Nov 19 12:11:59 PST 2002 University of California, San Diego Tue Nov 19 13:40:43 PST 2002 BOBJ> in stack1 ========================================== ***> implementing stack with pointer and array ========================================== th TRIV* ========================================== bth STACK ========================================== bth ARRAY ========================================== bth STACKIMP ========================================== set cobasis of STACK ========================================== open ========================================== c-reduce in STACKIMP : < 0 , put(E, J, A) > == < 0 , A > using cobasis of STACKIMP: op top _ : Stack -> Elt [prec 15] op pop _ : Stack -> Stack [prec 15] --------------------------------------- reduced to: < 0 , put(E, J, A) > == < 0 , A > ----------------------------------------- add rule (C1) : < 0 , put(E, J, A) > = < 0 , A > ----------------------------------------- target is: < 0 , put(E, J, A) > == < 0 , A > expand by: op top _ : Stack -> Elt [prec 15] reduced to: true nf: 0 ----------------------------------------- target is: < 0 , put(E, J, A) > == < 0 , A > expand by: op pop _ : Stack -> Stack [prec 15] deduced using (C1) : true nf: < 0 , A > ----------------------------------------- result: true c-rewrite time: 83ms parse time: 15ms ========================================== ops i j : -> Nat ========================================== eq i < j = true ========================================== cq < i , put(E, J, A) > = < i , A > if i <= J ========================================== c-reduce in STACKIMP : < (s i) , put(E, j, A) > == < (s i) , A > using cobasis of STACKIMP: op top _ : Stack -> Elt [prec 15] op pop _ : Stack -> Stack [prec 15] --------------------------------------- reduced to: < (s i) , put(E, j, A) > == < (s i) , A > ----------------------------------------- add rule (C1) : < (s i) , put(E, j, A) > = < (s i) , A > ----------------------------------------- target is: < (s i) , put(E, j, A) > == < (s i) , A > expand by: op top _ : Stack -> Elt [prec 15] reduced to: true nf: A [i] ----------------------------------------- target is: < (s i) , put(E, j, A) > == < (s i) , A > expand by: op pop _ : Stack -> Stack [prec 15] reduced to: true nf: < i , A > ----------------------------------------- result: true c-rewrite time: 69ms parse time: 32ms ========================================== close ========================================== open STACKIMP ========================================== vars I J : Nat ========================================== var A : Arr ========================================== var E : Elt ========================================== cq < I , put(E, J, A) > = < I , A > if I <= J ========================================== reduce in STACKIMP : top push(E, < I , A >) == E result Bool: true rewrite time: 14ms parse time: 6ms ========================================== reduce in STACKIMP : pop push(E, < I , A >) == < I , A > result Bool: true rewrite time: 9ms parse time: 15ms ========================================== close BOBJ> q Bye. awk%
To BOBJ examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Wed Nov 20 16:23:44 PST 2002