class interface SET[E->HASHABLE]
   --
   -- Definition of a mathematical set of hashable objects. All common
   -- operations on mathematical sets are available.
   --

creation
   make
      -- Create an empty set. Internal storage capacity of the set is
      -- initialized using the Default_size value. Then, tuning of needed
      -- storage size is done automatically according to usage. If you
      -- are really sure that your set is always really bigger than
      -- Default_size, you may use with_capacity to save some execution 
      -- time.

      ensure
         is_empty;
         capacity = default_size

   with_capacity (medium_size: INTEGER)
      -- Create an empty set using medium_size as an appropriate value
      -- to help initialization of capacity. Thus, this feature may be
      -- used in place of make to save some execution time if one is
      -- sure that storage size will rapidly become really bigger than
      -- Default_size (if not sure, simply use make). Anyway, the
      -- initial medium_size value is just an indication and never a
      -- limit for the possible capacity. Keep in mind that the
      -- capacity tuning is done automatically according to usage.

      require
         medium_size > 0
      ensure
         is_empty;
         capacity >= medium_size

   from_collection (model: COLLECTION[like item])

feature(s) from SET   default_size: INTEGER
      -- Minimum size for storage in number of items.


feature(s) from SET
   -- Counting:

   count: INTEGER
      -- Cardinality of the set (i.e. actual count of stored elements).


   capacity: INTEGER
      -- Of the buckets storage area.


   is_empty: BOOLEAN
      -- Is the set empty?

      ensure
         Result = (count = 0)

feature(s) from SET
   -- Adding and removing:

   add (e: like item)
      -- Add a new item to the set: the mathematical definition of
      -- adding in a set is followed.

      require
         e /= Void
      ensure
         added: has(e);
         not_in_then_added: not old has(e) implies count = old count + 1;
         in_then_not_added: old has(e) implies count = old count

   remove (e: like item)
      -- Remove item e from the set: the mathematical definition of
      -- removing from a set is followed.

      require
         e /= Void
      ensure
         removed: not has(e);
         not_in_not_removed: not old has(e) implies count = old count;
         in_then_removed: old has(e) implies count = old count - 1

   clear
      -- Empty the current set.

      ensure
         is_empty

feature(s) from SET
   -- Looking and searching:

   has (e: like item): BOOLEAN
      -- Is element e in the set?

      require
         e /= Void
      ensure
         Result implies not is_empty

   reference_at (e: like item): like item
      -- When Is element e in the set?

      require
         e /= Void;
         not e.is_expanded_type
      ensure
         has(e) implies Result /= Void

feature(s) from SET
   -- To provide iterating facilities:

   lower: INTEGER

   upper: INTEGER
      ensure
         Result = count

   valid_index (index: INTEGER): BOOLEAN
      ensure
         Result = index.in_range(lower,upper)

   item (index: INTEGER): E
      -- Return the item indexed by index.

      require
         valid_index(index)
      ensure
         has(Result)

   get_new_iterator: ITERATOR[E]

feature(s) from SET
   -- Mathematical operations:

   union (other: like Current)
      -- Make the union of the Current set with other.

      require
         other /= Void
      ensure
         count <= old count + other.count

   infix "+" (other: like Current): like Current
      -- Return the union of the Current set with other.

      require
         other /= Void
      ensure
         Result.count <= count + other.count;
         Current.is_subset_of(Result) and then other.is_subset_of(Result)

   intersection (other: like Current)
      -- Make the intersection of the Current set with other.

      require
         other /= Void
      ensure
         count <= other.count.min(old count)

   infix "^" (other: like Current): like Current
      -- Return the intersection of the Current set with other.

      require
         other /= Void
      ensure
         Result.count <= other.count.min(count);
         Result.is_subset_of(Current) and then Result.is_subset_of(other)

   minus (other: like Current)
      -- Make the set Current - other.

      require
         other /= Void
      ensure
         count <= old count

   infix "-" (other: like Current): like Current
      -- Return  the set Current - other.

      require
         other /= Void
      ensure
         Result.count <= count;
         Result.is_subset_of(Current)

feature(s) from SET
   -- Comparison:

   is_subset_of (other: like Current): BOOLEAN
      -- Is the Current set a subset of other?

      require
         other /= Void
      ensure
         Result implies count <= other.count

   is_disjoint_from (other: like Current): BOOLEAN
      -- Is the Current set disjoint from other ?

      require
         other /= Void
      ensure
         Result = (Current ^ other).is_empty

   is_equal (other: like Current): BOOLEAN
      -- Is the Current set equal to other?

      require
         other /= Void
      ensure
         double_inclusion: Result = (is_subset_of(other) and other.is_subset_of(Current));
         generating_type = other.generating_type implies Result = other.is_equal(Current)

feature(s) from SET   copy (other: like Current)
      -- Copy 'other' into the current set

      require
         same_dynamic_type(other)
      ensure
         is_equal(other)

   from_collection (model: COLLECTION[like item])

feature(s) from SET
   -- Agents based features:

   do_all (action: PROCEDURE[ANY,TUPLE[HASHABLE]])
      -- Apply action to every item of Current.


   for_all (test: PREDICATE[ANY,TUPLE[HASHABLE]]): BOOLEAN
      -- Do all items satisfy test?


   exists (test: PREDICATE[ANY,TUPLE[HASHABLE]]): BOOLEAN
      -- Does at least one item satisfy test?



invariant
   capacity > 0;
   capacity >= count;
   cache_user.in_range(-1,count);
   cache_user > 0 implies cache_node /= Void;
   cache_user > 0 implies cache_buckets.in_range(0,capacity - 1);

end of SET[E->HASHABLE]