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:

where( I, I1, I2: Nat, A : Arr)

I1 <= I2implies(I1 || put(I, I2, A)) R (I1 || 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.

- Click here for the first tatami (i.e., proof page) of the proof of this lemma.
- Click here for the Tatami demos home page.
- Click here for the Links Project home page.
- Click here for the UCSD Meaning and Computation Lab home page.

13 May 1997