deferred class interface P_SET[G]

feature(s) from P_CONTAINER
   --  Status

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

      ensure
         positive: Result >= 0

   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.

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Remove all objects from the container.

      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 (it: G)
      --  Search using is_equal for comparisons.

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

   found: BOOLEAN
      --  Result of the last search operation.


   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
      --  Does the container has a - unique - copy of the object? 


feature(s) from P_SET
   --  Update 

   add (it: G)
      --  Add an item to the container.

      require
         writable: is_writable;
         not_void: not is_void(it);
         has_not: not has(it)
      ensure
         keep_reference: has(it)

   remove
      --  Remove the current item.

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

feature(s) from P_SET
   --  Conversion

   to_list: P_LIST[G]
      --  Convert the set to a list.

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

invariant
   empty: is_empty = count = 0;

end of deferred P_SET[G]