// @(#)$Id: SimpleSet.lh,v 1.20 1998/08/29 21:48:54 leavens Exp $

template <class Elem /*@ expects SimpleSetRequirement(Elem) @*/>
  //@ where Elem is {
  //@   bool operator ==(Elem x, Elem y);
  //@   behavior {
  //@       ensures returns /\ result = (x = y);
  //@   }
  //@ };
class Set {
public:
  //@ uses SimpleSetTrait(Elem for E, Set<Elem> for C);

  Set() throw();
  //@ behavior {
  //@   constructs self;
  //@   ensures liberally self' = empty;
  //@ }

  void insert(Elem e) throw();
  //@ behavior {
  //@   modifies self;
  //@   ensures liberally self' = self^ \U {e};
  //@ }

  bool is_in(Elem e) const throw();
  //@ behavior {
  //@   ensures result = (e \in self);
  //@ }
};

[Index]

HTML generated using lcpp2html.