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

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

end of deferred DS_CONTAINER[G]