deferred class interface DS_DISPENSER[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

feature(s) from DS_DISPENSER
   --  Status report

   extendible (n: INTEGER): BOOLEAN
      --  May dispenser be extended with n items?

      require
         positive_n: n >= 0

feature(s) from DS_DISPENSER
   --  Access

   item: G
      --  Item accessible from dispenser

      require
         not_empty: not is_empty

feature(s) from DS_DISPENSER
   --  Element change

   put (v: G)
      --  Add v to dispenser.

      require
         extendible: extendible(1)
      ensure
         one_more: count = old count + 1

   force (v: G)
      --  Add v to dispenser.

      ensure
         one_more: count = old count + 1

   extend (other: DS_LINEAR[G])
      --  Add items of other to dispenser.
      --  Add other.first first, etc.

      require
         other_not_void: other /= Void;
         extendible: extendible(other.count)
      ensure
         new_count: count = old count + other.count

   append (other: DS_LINEAR[G])
      --  Add items of other to dispenser.
      --  Add other.first first, etc.

      require
         other_not_void: other /= Void
      ensure
         new_count: count = old count + other.count

feature(s) from DS_DISPENSER
   --  Removal

   remove
      --  Remove item from dispenser.

      require
         not_empty: not is_empty
      ensure
         one_less: count = old count - 1

   prune (n: INTEGER)
      --  Remove n items from dispenser.

      require
         valid_n: 0 <= n and n <= count
      ensure
         new_count: count = old count - n

   keep (n: INTEGER)
      --  Keep n items in dispenser.

      require
         valid_n: 0 <= n and n <= count
      ensure
         new_count: count = n

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

end of deferred DS_DISPENSER[G]