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.