// @(#)$Id: BoundedStack.pri,v 1.3 1997/07/25 17:04:15 leavens Exp $
// protected and private members for class BoundedStack

private:
  Elem elems[max_size];
  int current_top;
  //@ depends self on elems, current_top;
  //@ invariant (-1) <= current_top\any /\ current_top\any <= max_size;
  //@ uses BoundedStackPrivateTrait;
  //@ invariant self\any = toStack(elems\any, current_top\any);