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]