deferred class interface DS_SORTABLE[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_SORTABLE
   --  Status report

   sorted (a_sorter: DS_SORTER[G]): BOOLEAN
      --  Is container sorted according to a_sorter's criterion?

      require
         a_sorter_not_void: a_sorter /= Void

feature(s) from DS_SORTABLE
   --  Sort

   sort (a_sorter: DS_SORTER[G])
      --  Sort container using a_sorter's algorithm.

      require
         a_sorter_not_void: a_sorter /= Void
      ensure
         sorted: sorted(a_sorter)

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

end of deferred DS_SORTABLE[G]