A standard benchmark among correctness proofs is to verify the array-with-pointer implementation of stack. Because it has been done in so many different formalisms, it provides an excellent standard for comparing formalisms; we believe our coinductive proof is about as simple as possible, and in any case, it 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. An important lemma shows
that the values above the pointer do not effect behavior.

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 STACK model after forgetting the operations in
*-* . The proof uses coinduction, an efficient
syntactic proof technique for behavioral properties that does *not*
refer to the models directly. This example is discussed at length in "A Hidden Agenda" by Joseph Goguen and Grant
Malcolm, including justification of the recursive definition for the candidate
relation.

To the first tatami (i.e., proof page) of the formal coinductive correctness proof.

To the hand made Tatami demos homepage.

To the Links Project homepage.

To the UCSD Meaning and Computation Lab home page.

30 May 1997