// @(#)$Id: IntSetPrivate2.lh,v 1.24 1999/03/04 03:32:30 leavens Exp $

#include "IntList.lh"

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

class IntSet {
private:
  IntList the_elems;
  int the_size;

  //@ depends value on the_elems, the_size;
  //@ represents value by
  //@    \A i: int (i \in value\any = i \in the_elems\any)
  //@    /\ size(value\any) = the_size\any;

  // Invariants documenting design decisions (rep invariants).
  //@ invariant \A i: int (i \in the_elems\any =>
  //@                           count(i, the_elems\any) = 1);
  //@ invariant the_size\any = len(the_elems\any);

public:
  // meaning of inherited specifications follows.

  //@ spec Set<int> value;
  //@ depends self on value;

  IntSet() throw();
  //@ behavior {
  //@   constructs self;                            // from IntSetInformal.lh
  //@   ensures informally "self' is {}";
  //@ also
  //@   constructs value;                            // from IntSet.lh
  //@   ensures value' = empty;
  //@   ensures redundantly  the_elems' = empty /\ the_size' = 0; // by invar.
  //@ }

  void insert(int e) throw();
  //@ behavior {
  //@   modifies self;                           // from IntSetInformal.lh
  //@   ensures informally "e is added to self";
  //@ also
  //@   modifies value;                          // from IntSet.lh
  //@   ensures value' = value^ \U {e};
  //@   ensures redundantly e \in the_elems';    // by the invariant
  //@ }

  bool is_in(int e) const throw();
  //@ behavior {
  //@                                             // from IntSetInformal.lh
  //@   ensures informally "result is true just when e is a member of self";
  //@ also
  //@   ensures result = (e \in (value\any));      // from IntSet.lh
  //@   ensures redundantly  result = (e \in (the_elems\any)); // by invar.
  //@ }

  int pick() throw();
  //@ behavior {
  //@   requires informally "self is not {}"; // from IntSetInformal.lh
  //@   modifies self;
  //@   ensures informally "result is some member of self"
  //@                      "and result is also deleted from self";
  //@ also
  //@   requires ~isEmpty(value^);             // from IntSet.lh
  //@   requires redundantly ~the_size = 0;    // by the invariant
  //@   modifies value;
  //@   ensures result \in value^ /\ not(result \in value');
  //@   ensures redundantly  not(result \in the_elems'); // by the invariant
  //@ also
  //@   requires ~isEmpty(value^);             // from IntSet2.lh
  //@   requires redundantly ~the_size = 0;    // by the invariant
  //@   modifies value;
  //@   ensures result \in value^ /\ value' = delete(result, value^);
  //@ }

  int size() throw();
  //@ behavior {
  //@   ensures result = size(value\any);          // from IntSet2.lh
  //@   ensures redundantly result = the_size\any; // by the invariant
  //@ }
};

[Index]

HTML generated using lcpp2html.