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:

  1. the candidate relation R, for I,I1,I2 : Nat and A1,A2 : Arr, by:
  2. the selector subsignature , to contain top, and
  3. the generator subsignature , to contain push, pop .
The selections in 2, 3 are both the defaults. Coinduction now requires us to do the following:
  1. show R is a hidden -congruence;
  2. show R is preserved by all operations in ; and
  3. show that the following hold:

29 May 1997