// @(#)$Id: BoundedStack.h,v 1.8 1998/09/23 15:58:20 ruby Exp $

#ifndef BoundedStack_h
#define BoundedStack_h

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

  static const int max_size = 50;

  //@ invariant size(self\any) <= max_size\any;

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

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

  virtual BoundedStack<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));
  //@ }

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

  virtual int numElems() const throw();
  //@ behavior {
  //@   ensures result = size(self\any);
  //@ }

#include "BoundedStack.pri"
};

#endif

[Index]

HTML generated using lcpp2html.