helphome pageduck scriptspecificationfirst proof page

Implementing Stack with Pointer and Array


A standard benchmark for correctness proofs is verifying the pointer-array implementation of stack. Because it has been done in so many different formalisms, it provides an excellent standard for comparing formalisms, and we believe that our coinductive proof is about as simple as possible; in any case, it certainly provides a good illustration of our hidden algebra proof technology.

A hidden refinement proof requires proving that the equations in the hidden specification of stack are behaviorally satisfied by the implementation specification, in which the pointer is represented as a cell containing a natural number. A stack of depth n has n in this cell, and its n elements appear in places 0,...,n-1 of the array. Note that there may also be elements above the pointer, i.e., in a place greater than n-1. The Java applet below (by Akira Mori, based on an original by Grant Malcolm) shows the behavior of both the original stack abstraction and of its array with pointer implementation.

Let be the stack signature and E its equations, let be the implementation signature and E' its equations. Since the stack operations are defined in the implementation, we have . Technically, we will show that E' E, which means that every model of the implementation gives rise to a model of the stack spec, after forgetting the operations in - . The proof requires a lemma, which shows that the values above the pointer have no effect on the behavior of the implementation.

The proof uses circular coinductive rewriting, an efficient syntactic proof technique for behavioral properties that does not refer to the models directly. This example is discussed in some detail in "Circular Coinductive Rewriting" by Joseph Goguen, Kai Lin and Grigore Rosu, and an older, less automated proof is discussed in "A Hidden Agenda" by Joseph Goguen and Grant Malcolm; the coinduction tutorial page discusses the method used in the older proof.


To the Kumo demos homepage.
To the Tatami Project homepage.
To the UCSD Meaning and Computation Group homepage.

       This page was generated by Kumo on Tue Feb 13 19:32:22 PST 2001.