// @(#)$Id: IntSetPrivate.lh,v 1.16 1999/03/04 03:32:22 leavens Exp $

#include "IntSet2.lh"
#include "IntList.lh"

//@ refine IntSet
//@ by
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);

};

[Index]

HTML generated using lcpp2html.