// @(#)$Id: IntSetInformal.lh,v 1.13 1997/08/05 23:06:08 leavens Exp $

class IntSet {
public:
  IntSet() throw();
  //@ behavior {
  //@   constructs self;
  //@   ensures informally "self' is {}";
  //@ }

  void insert(int e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures informally "e is added to self";
  //@ }

  bool is_in(int e) const throw();
  //@ behavior {
  //@   ensures informally "result is true just when e is a member of self";
  //@ }

  int pick() throw();
  //@ behavior {
  //@   requires informally "self is not {}";
  //@   modifies self;
  //@   ensures informally "result is some member of self"
  //@                      "and result is also deleted from self";
  //@ }
};

[Index]

HTML generated using lcpp2html.