// @(#)$Id: SimpleStack.lh,v 1.18 1998/09/23 16:01:14 ruby Exp $

template <class T /*@ expects contained_objects(T) @*/ >
class Stack {
public:
  //@ uses SimpleStackTrait(T for E, Stack<T> for C);

  Stack() throw();
  //@ behavior {
  //@   constructs self;
  //@   ensures liberally self' = empty;
  //@ }

  void push(T e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures liberally self' = push(e, self^);
  //@ }

  T pop() throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures self' = pop(self^);
  //@ }

  T top() const throw();
  //@ behavior {
  //@   requires ~isEmpty(self^);
  //@   ensures result = top(self^);
  //@ }
};

[Index]

HTML generated using lcpp2html.