// @(#)$Id: SimpleSet2.lh,v 1.3 1998/09/24 16:36:45 leavens Exp $

#include "Equivalence.lh"

template <class Elem /*@ expects SimpleSetRequirement(Elem) ElemTrait @*/>
  //@ where Elem is Equivalence<Elem using *ElemTrait>;
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.