We show that array-with-pointer implementation of stack is
correct.
We use coinduction to
prove that the equations in the STACK specification are behavioral consequences of
the PTR || ARR
specification:
For this, we must define the following:
- the
candidate relation
R, for I,I1,I2
: Nat and A1,A2 : Arr,
by:
- (s I1 || A1) R (s I2 || A2)
iff
- I1 = I2 and
A1[I1] = A2[I2] and
(I1 || A1) R (I2 || A2) .
- (0 || A1) R (I || A2)
iff
I = 0 .
- (I || A) R (I || A) .
- I1 R I2
iff
I1 = I2 .
- the
selector subsignature
, to contain top, and
- the
generator subsignature
, to contain push,
pop .
The selections in 2, 3 are both
the defaults.
Coinduction now requires us to do the following:
- show R is a
hidden -congruence;
- show R is preserved by all operations in ; and
- show that the following hold:
- (pop empty) R empty .
- (
N : Nat, I : Nat, A : Arr)
(top push(N, I || A)) R N .
- ( N : Nat, I : Nat, A : Arr)
(pop push(N, I || A)) R (I || A) .
29 May 1997