deferred class interface DS_RESIZABLE[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_RESIZABLE
   --  Measurement

   capacity: INTEGER
      --  Maximum number of items in container


feature(s) from DS_RESIZABLE
   --  Status report

   is_full: BOOLEAN
      --  Is container full?


feature(s) from DS_RESIZABLE
   --  Resizing

   resize (n: INTEGER)
      --  Resize container so that it can contain
      --  at least n items. Do not lose any item.

      require
         n_large_enough: n >= capacity
      ensure
         capacity_set: capacity = n

invariant
   positive_count: count >= 0;
   empty_definition: is_empty = count = 0;
   count_constraint: count <= capacity;
   full_definition: is_full = count = capacity;

end of deferred DS_RESIZABLE[G]