// @(#)$Id: BoundedIntStack.lh,v 1.28 1999/03/04 23:16:44 leavens Exp $

#include "StackError.lh"

//@ uses Stack(int for E, int for Int, IntStack for C);
//@ spec class IntStack;

class BoundedIntStack {
public:
  //@ spec IntStack stk;
  //@ spec int max_size;

  //@ invariant max_size\any >= 0 /\ size(stk\any) <= max_size\any;
  //@ constraint max_size^ = max_size';

  BoundedIntStack(int limit = 50) throw();
  //@ behavior {
  //@   requires limit >= 0;
  //@   modifies max_size, stk;
  //@   ensures max_size' = limit /\ stk' = empty;
  //@ }
  
  virtual ~BoundedIntStack() throw();
  //@ behavior {
  //@   ensures true;
  //@ }

  virtual BoundedIntStack& push(int e) throw(StackError*);
  //@ behavior {
  //@   requires size(stk^) < max_size^;
  //@   modifies stk;
  //@   ensures returns /\ result = self
  //@           /\ stk' = push(stk^,e);
  //@   example max_size^ >= 2
  //@           /\ stk^ = push(empty, 8) /\ e = 3
  //@           /\ stk' = push(push(empty, 8), 3) /\ result = self
  //@           /\ returns;
  //@ also
  //@   requires size(stk^) >= max_size^;
  //@   ensures throws(StackError*);
  //@   example max_size^ = 2
  //@           /\ stk^ = push(push(empty, 8), 3) /\ e = 7
  //@           /\ stk' = push(push(empty, 8), 3)
  //@           /\ throws(StackError*);
  //@ }

  virtual BoundedIntStack& pop() throw(StackError*);
  //@ behavior {
  //@   requires ~isEmpty(stk^);
  //@   modifies stk;
  //@   ensures returns /\ result = self
  //@           /\ stk' = pop(stk^);
  //@   example stk^ = push(push(empty, 8), 3)
  //@           /\ returns /\ result = self
  //@           /\ stk' = push(empty,8);
  //@ also
  //@   requires isEmpty(stk^);
  //@   ensures throws(StackError*);
  //@ }

  virtual int top() const throw(StackError*);
  //@ behavior {
  //@   requires ~isEmpty(stk\any);
  //@   ensures returns /\ result = top(stk\any);
  //@   example stk\any = push(push(empty, 8), 3) /\ result = 3;
  //@ also
  //@   requires isEmpty(stk\any);
  //@   ensures throws(StackError*);
  //@ }

  virtual bool isEmpty() const throw();
  //@ behavior {
  //@   ensures result = (isEmpty(stk\any));
  //@   ensures redundantly result = (size(stk\any) = 0);
  //@ }

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

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

[Index]

HTML generated using lcpp2html.