// @(#)$Id: SimpleStackInstances.lh,v 1.6 1998/09/23 16:01:29 ruby Exp $
#include "SimpleStack.lh"

extern  Stack<Stack<int /*@ using int @*/>
              /*@ using SimpleStackTrait(int, Stack<int>) @*/>
          myStackofStacks;

//@ uses SimpleStackTrait(int for E, Stack<int> for C);
//@ uses SimpleStackTrait(Stack<int> for E, Stack< Stack<int> > for C);

extern void pop_the_top_stack() throw();
//@ behavior {
//@   requires assigned(myStackofStacks, pre) /\ ~isEmpty(myStackofStacks^)
//@            /\ ~isEmpty(top(myStackofStacks^));
//@   modifies myStackofStacks;
//@   ensures myStackofStacks' = push(pop(top(myStackofStacks^)),
//@                                   pop(myStackofStacks^));
//@ };

[Index]

HTML generated using lcpp2html.