deferred class interface P_SORTABLE[G]

feature(s) from P_CONTAINER
   --  Status

   count: INTEGER
      --  Number of items in the container.

      ensure
         positive: Result >= 0

   is_empty: BOOLEAN
      --  Is the container empty?


   is_readable: BOOLEAN
      --  Is the container currently readable?


   is_writable: BOOLEAN
      --  Is the container currently writable?


   item: G
      --  Current item.

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Remove all objects from the container.

      require
         writable: is_writable
      ensure
         done: is_empty

feature(s) from P_CONTAINER
   --  Output

   out: STRING
      --  String representation.

      ensure
         is_copy:  --  new string

feature(s) from P_CONTAINER
   --  Utility

   is_void (x: ANY): BOOLEAN
      --  Void assertion for generic parameters.


feature(s) from P_SORTABLE
   --  Order relation

   has_order: BOOLEAN
      --  Does this container has an order relation defined?


   set_order (ord_rel: P_ORDER_RELATION[G])
      --  Set the order relation which will be used 
      --  when sorting. The relation stays the same when 
      --  the container is reset.

      require
         valid: ord_rel /= Void
      ensure
         keep_reference: has_order

feature(s) from P_SORTABLE
   --  Sorting

   sort
      --  Sort the container.

      require
         has_order: has_order;
         writable: is_writable
      ensure
         sorted: is_sorted

   is_sorted: BOOLEAN
      --  Is the container sorted?

      require
         has_order: has_order
      ensure
         empty_sorted: is_empty implies Result

invariant
   empty: is_empty = count = 0;

end of deferred P_SORTABLE[G]