7.1.3 A Class with Exceptions (Stack)

It is traditional to give a specification of some kind of stack as an example specification. It is almost too easy to specify unbounded stacks, by using the LSL Handbook trait Stack (page 170 of [Guttag-Horning93]). A specification of unbounded stacks is included in the Larch/C++ release. In this section, we specify bounded stacks of integers in the following. (See section 8 Template Specifications for how to specify stacks of arbitrary types.) The abstract values of bounded integer stacks include both a stack of integers and a bound. To model this we again use specification variables. The specification variable max_size holds the maximum size of a BoundedIntStack. The specification variable stk holds a value specified by the trait mentioned above. We use a specification-only class declaration to declare the type of this variable, IntStack.

The interface specification of the class BoundedIntStack follows. Note that the history constraint for the class specifies that, although the bound is specified when an object is created, it cannot be changed thereafter.

The interface specified for BoundedIntStack uses exceptions (see section 6.11 Exceptions) and case analysis (see section 6.10 Case Analysis). The case analysis is used, for the functions that throw exceptions, to give two sets of pre- and postconditions: one for the "normal" case, and one for the case when the exception is thrown. This specification also illustrates how to specify mixed mutators and observers; for example, push returns the default argument (the object self). Note that result = self means that they are the same object.

// @(#)$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);
  //@ }
};

The interface specification of BoundedIntStack above also makes rather liberal use of examples (see section 6.9.1 Examples in Function Specifications). While these tend to make the specification somewhat lengthy, they are invaluable in communicating with readers who do not take the trouble to look at the trait in detail.

The C++ interface specified for numElems says that it is a virtual function, which returns an int. It also is specified to be a const member function. Finally the specified interface tells C++ that no exceptions are thrown, by writing throw(). (If one omits this, then as in C++, the specification does not limit what exceptions can be thrown.)

The exceptions that are thrown are all from the included specification of the class StackError. This is specified as follows.

// @(#)$Id: StackError.lh,v 1.4 1997/01/12 22:21:28 leavens Exp $

//@ uses NoInformationException(StackError);
class StackError { };

See section 6.11 Exceptions for the included trait NoInformationException and more discussion on this kind of example.

Go to the first, previous, next, last section, table of contents.