// @(#)$Id: IntSet.lh,v 1.15 1999/03/02 17:56:26 leavens Exp $

#include "IntSetInformal.lh"

//@ spec template <class T> class Set;
//@ uses ChoiceSet(int for E, Set<int> for C), NoContainedObjects(Set<int>);

//@ refine IntSet
//@ by
class IntSet {
public:
  //@ spec Set<int> value;
  //@ depends self on value;
  //@ represents self by self\any = value\any;

  IntSet() throw();
  //@ behavior {
  //@   constructs value;
  //@   ensures value' = empty;
  //@ }

  void insert(int e) throw();
  //@ behavior {
  //@   modifies value;
  //@   ensures value' = value^ \U {e};
  //@ }

  bool is_in(int e) const throw();
  //@ behavior {
  //@   ensures result = (e \in (value\any));
  //@ }

  int pick() throw();
  //@ behavior {
  //@   requires ~isEmpty(value^);
  //@   modifies value;
  //@   ensures result \in value^ /\ not(result \in value');
  //@ }
};

[Index]

HTML generated using lcpp2html.