We show that array-with-pointer implementation of stack is correct.
We want to prove
pop empty = empty and
( A : Arr, N I : Nat) top push(N , I || A) = N and
( A : Arr, N I : Nat) pop push(N , I || A) = I || A
We use coinduction to prove that it is a behavioral property of the input specification. For this, we must define the following:
the observation relation
R
for
A1,A2
:
Arr
I1,I2
:
Nat
, by
s I1 || A1 R s I2 || A2
iff
I2 == I1 and A1 [ I1 ] == A2 [ I1 ] and (I1 || A1 R I1 || A2)
.
0 || A1 R 0 || A2
.
the cobasis :
{ top,pop }
.
Coinduction now requires us to do the following:
Show
R
is -congruence.Show
((pop empty) R empty and (( A : Arr, N I : Nat) top push(N , I || A) = N)) and (( A : Arr, N I : Nat) (pop push(N , I || A)) R I || A)
.
This page was generated by Kumo on Wed Oct 13 18:03:25 PDT 1999.