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*.

- 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 body>