deferred class interface DS_SEARCHABLE[G]

feature(s) from DS_CONTAINER
   --  Measurement

   count: INTEGER
      --  Number of items in container


feature(s) from DS_CONTAINER
   --  Status report

   is_empty: BOOLEAN
      --  Is container empty?


feature(s) from DS_CONTAINER
   --  Comparison

   is_equal (other: like Current): BOOLEAN
      --  Is current container equal to other?

      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

feature(s) from DS_CONTAINER
   --  Removal

   wipe_out
      --  Remove all items from container.

      ensure
         wiped_out: is_empty

feature(s) from DS_SEARCHABLE
   --  Status report

   has (v: G): BOOLEAN
      --  Does container include v?
      --  (Use equality_tester's comparison criterion
      --  if not void, use = criterion otherwise.)

      ensure
         not_empty: Result implies not is_empty

   same_items (v, u: G): BOOLEAN
      --  Are v and u considered equal?
      --  (Use equality_tester's comparison criterion
      --  if not void, use = criterion otherwise.)


   same_equality_tester (other: DS_SEARCHABLE[G]): BOOLEAN
      --  Does container use the same comparison
      --  criterion as other?

      require
         other_not_void: other /= Void

feature(s) from DS_SEARCHABLE
   --  Measurement

   occurrences (v: G): INTEGER
      --  Number of times v appears in container
      --  (Use equality_tester's comparison criterion
      --  if not void, use = criterion otherwise.)

      ensure
         positive: Result >= 0;
         has: has(v) implies Result >= 1

feature(s) from DS_SEARCHABLE
   --  Access

   equality_tester: DS_EQUALITY_TESTER[G]
      --  Equality tester;
      --  A void equality tester means that =
      --  will be used as comparison criterion.


feature(s) from DS_SEARCHABLE
   --  Setting

   set_equality_tester (a_tester: like equality_tester)
      --  Set equality_tester to a_tester.
      --  A void equality tester means that =
      --  will be used as comparison criterion.

      ensure
         equality_tester_set: equality_tester = a_tester

invariant
   positive_count: count >= 0;
   empty_definition: is_empty = count = 0;

end of deferred DS_SEARCHABLE[G]