class interface P_HASH_SET[G->HASHABLE]

creation
   make
      --  Create set.


feature(s) from P_CONTAINER
   --  Status

   count: INTEGER
      --  Number of items in the container.


   is_empty: BOOLEAN
      --  Is the container empty?


   is_readable: BOOLEAN
      --  Is the container currently readable?


   is_writable: BOOLEAN
      --  Is the container currently writable?


   item: G
      --  Current item.
      --  Time: O(1)

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Create set.

      require
         writable: is_writable
      ensure
         done: is_empty

feature(s) from P_CONTAINER
   --  Output

   out: STRING
      --  String representation.

      ensure
         is_copy:  --  new string

feature(s) from P_CONTAINER
   --  Utility

   is_void (x: ANY): BOOLEAN
      --  Void assertion for generic parameters.


feature(s) from P_SEARCHABLE
   --  Search

   search (x: G)
      --  Search item in container (compare using is_equal).
      --  Time: O(1)

      require
         readable: is_readable
      ensure
         search_eq_has: found implies has(x);
         item_set: found implies item.is_equal(x)

   found: BOOLEAN
      --  Result of last search.
      --  Time: O(1), attribute


   found_count: INTEGER
      --  A set has only one copy of each item.

      require
         meaningful: found = true
      ensure
         set_count: Result = 1;
         meaningful: Result >= 1

feature(s) from P_SET
   --  Search

   has (it: G): BOOLEAN
      --  Is the item in the container (side-effect free search)
      --  Time: O(1)


feature(s) from P_SET
   --  Update 

   add (it: G)
      --  Add item to container.
      --  Time: O(1), amortised

      require
         writable: is_writable;
         not_void: not is_void(it);
         has_not: not has(it)
      ensure
         count: count = old count + 1;
         keep_reference: has(it)

   remove
      --  Remove current item.
      --  Time: 0(1), amortised

      require
         writable: is_writable;
         not_empty: not is_empty
      ensure
         count: count = old count - 1; --  not has(old item)
         done: 
         done:  --  not has(old item)

feature(s) from P_SET
   --  Conversion

   to_list: P_LIST[G]
      --  Convert the hash set to a (linked) list.
      --  Time: O(count)

      ensure
         done: Result /= Void and then Result.count = count; --  new list, but real items
         is_shallow_copy: 

feature(s) from P_HASH_SET
   --  Creation

   make
      --  Create set.


feature(s) from P_HASH_SET
   --  General

   copy (other: like Current)
      --  Copy set (same items).
      --  Time: 0(count)

      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

   is_equal (other: like Current): BOOLEAN
      --  Other container equal?
      --  Time: O(count)

      require
         other_not_void: other /= Void
      ensure
         done_count: Result implies count = other.count; --  Result implies (for_each item other.has(item))
         done: 
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

invariant
   empty: is_empty = count = 0;
   resize_up: count // hashsize <= Grow_entries + 1;
   resize_down: not is_empty and then hashsize > Default_hashsize implies count // hashsize >= Shrink_entries - 1;
   has_hashtable: hashtable /= Void;
   hashsize: hashsize = hashtable.count;
   current_item: not is_empty implies hashlist /= Void;
   empty: is_empty = hashlist = Void;

end of P_HASH_SET[G->HASHABLE]