deferred class interface DS_TRAVERSABLE[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_TRAVERSABLE -- Access item_for_iteration: G -- Item at internal cursor position require not_off: not off new_cursor: DS_CURSOR[G] -- New external cursor for traversal ensure cursor_not_void: Result /= Void; valid_cursor: valid_cursor(Result) feature(s) from DS_TRAVERSABLE -- Status report off: BOOLEAN -- Is there no item at internal cursor position? same_position (a_cursor: like new_cursor): BOOLEAN -- Is internal cursor at same position as a_cursor? require a_cursor_not_void: a_cursor /= Void valid_cursor (a_cursor: DS_CURSOR[G]): BOOLEAN -- Is a_cursor a valid cursor? require a_cursor_not_void: a_cursor /= Void feature(s) from DS_TRAVERSABLE -- Cursor movement go_to (a_cursor: like new_cursor) -- Move internal cursor to a_cursor's position. require cursor_not_void: a_cursor /= Void; valid_cursor: valid_cursor(a_cursor) ensure same_position: same_position(a_cursor) invariant positive_count: count >= 0; empty_definition: is_empty = count = 0; empty_constraint: is_empty implies off; internal_cursor_not_void: internal_cursor /= Void; valid_internal_cursor: valid_cursor(internal_cursor); end of deferred DS_TRAVERSABLE[G]