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, ) = .
eq top <0, A> = 0 .
eq top = A [I] .
eq pop = .
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, ) == N .
red pop push(N, ) == .
cred pop push(N, ) == .
red pop push(N, ).
*** this suggests the lemma that we need:
*** lemma by induction on I: = 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 = if i <= J .
red == .
cred == .
close
open STACKIMP .
*** assert the lemma:
vars I J : Nat . var A : Arr . var N : Nat .
cq = if I <= J .
*** prove the equations:
red top push(N, ) == N .
red pop push(N, ) == .
cred pop push(N, ) == .
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, ) = .
eq top <0, A> = 0 .
eq top = A [I] .
eq pop = .
eq pop <0, A> = <0, A> .
end
set cobasis of STACK
set cred trace on .
*** lemma by induction on I: = 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 = if i <= J .
cred == .
close
open STACKIMP .
*** assert the lemma:
vars I J : Nat . var A : Arr . var E : Elt .
cq = if I <= J .
*** prove the equations:
red top push(E, ) == E .
red pop push(E, ) == .
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