Pointer Array Implementation of Stack

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:

A1,A2

Arr

I1,I2

Nat

s I1 || A1 R s I2 || A2

I2 == I1 and A1 [ I1 ] == A2 [ I1 ] and (I1 || A1 R I1 || A2)

0 || A1 R 0 || A2

{ top,pop }

Coinduction now requires us to do the following:

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