deferred class interface DS_BILINEAR[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_BILINEAR_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) feature(s) from DS_SEARCHABLE -- Status report has (v: G): BOOLEAN -- Does container include v? -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) ensure not_empty: Result implies not is_empty same_items (v, u: G): BOOLEAN -- Are v and u considered equal? -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) same_equality_tester (other: DS_SEARCHABLE[G]): BOOLEAN -- Does container use the same comparison -- criterion as other? require other_not_void: other /= Void feature(s) from DS_SEARCHABLE -- Measurement occurrences (v: G): INTEGER -- Number of times v appears in container -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) ensure positive: Result >= 0; has: has(v) implies Result >= 1 feature(s) from DS_SEARCHABLE -- Access equality_tester: DS_EQUALITY_TESTER[G] -- Equality tester; -- A void equality tester means that = -- will be used as comparison criterion. feature(s) from DS_SEARCHABLE -- Setting set_equality_tester (a_tester: like equality_tester) -- Set equality_tester to a_tester. -- A void equality tester means that = -- will be used as comparison criterion. ensure equality_tester_set: equality_tester = a_tester feature(s) from DS_LINEAR -- Access first: G -- First item in container require not_empty: not is_empty ensure has_first: has(Result) feature(s) from DS_LINEAR -- Status report is_first: BOOLEAN -- Is internal cursor on first item? ensure not_empty: Result implies not is_empty; not_off: Result implies not off; definition: Result implies item_for_iteration = first after: BOOLEAN -- Is there no valid position to right of internal cursor? feature(s) from DS_LINEAR -- Cursor movement start -- Move internal cursor to first position. ensure empty_behavior: is_empty implies after; not_empty_behavior: not is_empty implies is_first forth -- Move internal cursor to next position. require not_after: not after search_forth (v: G) -- Move internal cursor to first position at or after current -- position where item_for_iteration and v are equal. -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) -- Move after if not found. require not_off: not off or after go_after -- Move cursor to after position. ensure after: after feature(s) from DS_BILINEAR -- Access last: G -- Last item in container require not_empty: not is_empty ensure has_last: has(Result) feature(s) from DS_BILINEAR -- Status report is_last: BOOLEAN -- Is internal cursor on last item? ensure not_empty: Result implies not is_empty; not_off: Result implies not off; definition: Result implies item_for_iteration = last before: BOOLEAN -- Is there no valid position to left of internal cursor? feature(s) from DS_BILINEAR -- Cursor movement finish -- Move internal cursor to last position. ensure empty_behavior: is_empty implies before; not_empty_behavior: not is_empty implies is_last back -- Move internal cursor to previous position. require not_before: not before search_back (v: G) -- Move internal cursor to first position at or before current -- position where item_for_iteration and v are equal. -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) -- Move before if not found. require not_off: not off or before go_before -- Move cursor to before position. ensure before: before 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); after_constraint: after implies off; not_both: not (after and before); before_constraint: before implies off; end of deferred DS_BILINEAR[G]