Key Lemma for Stack Implementation
Proving non-trivial behavioral properties of the array-with-pointer implementation of stack is often facilitated by knowing that values in the array that lie above the pointer do not matter behaviorally. This key lemma can be formulated as follows:
( I, I1, I2: Nat, A : Arr)
                I1 <= I2   implies   (I1 || put(I, I2, A)) R (I1 || A) .
where put(I,I2,A) puts the value I at location I2 in the array A, and where I1 || A indicates the implementation state with pointer I1 and array A.

The applet below illustrates this lemma. The top array and pointer represent a fixed current state, and below that is a copy that we can manipulate. For this, first choose a pointer value by clicking on a position between the two arrays. Next, change the value of a cell above the pointer in the lower array by clicking that cell; a random number will be chosen for its new value. Now, you can try the "pop" and "push" operations to see that the two arrays are indeed "behaviorally" the same.



13 May 1997