// @(#)$Id: Stack.h,v 1.6 1998/09/23 15:58:39 ruby Exp $

#ifndef Stack_h
#define Stack_h

template <class Elem /*@ expects contained_objects(Elem) @*/ >
class Stack
#include "Stack.bse"
{
public:
  //@ uses StackTrait(Elem for E, Stack<Elem> for C);

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

  virtual ~Stack() throw();  // destructor
  //@ behavior {
  //@   ensures true;
  //@ }
  
  virtual Stack<Elem>& push(Elem e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures liberally self' = push(self^,e) /\ result = self;
  //@ }

  virtual Stack<Elem>& pop() throw();
  //@ behavior {
  //@   requires ~isEmpty(self^);
  //@   modifies self;
  //@   ensures self' = pop(self^) /\ result = self;
  //@ }

  virtual Elem top() const throw();
  //@ behavior {
  //@   requires ~isEmpty(self\any);
  //@   ensures result = top(self\any);
  //@ }

  virtual bool isEmpty() const throw();
  //@ behavior {
  //@   ensures result = (isEmpty(self\any));
  //@ }

#include "Stack.pri"
};

#endif

[Index]

HTML generated using lcpp2html.