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]