class interface DS_LINKED_LIST_CURSOR[G] creation make (a_list: like container) -- Create a new cursor for a_list. require a_list_not_void: a_list /= Void ensure container_set: container = a_list; before: before feature(s) from DS_LINEAR_CURSOR -- Access container: DS_LINKED_LIST[G] -- List traversed feature(s) from DS_LINEAR_CURSOR -- Status report is_first: BOOLEAN -- Is cursor on the first item? ensure not_empty: Result implies not container.is_empty; not_off: Result implies not off; definition: Result implies item = container.first after: BOOLEAN -- Is there no valid position to right of cursor? off: BOOLEAN -- Is there no item at cursor position? feature(s) from DS_LINEAR_CURSOR -- Cursor movement start -- Move cursor to first position. -- (Performance: O(1).) ensure empty_behavior: container.is_empty implies after; not_empty_behavior: not container.is_empty implies is_first forth -- Move cursor to next position. -- (Performance: O(1).) require not_after: not after search_forth (v: G) -- Move to first position at or after current -- position where item and v are equal. -- (Use equality_tester's criterion from container -- 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. -- (Performance: O(1).) ensure after: after feature(s) from DS_CURSOR -- Access item: G -- Item at cursor position -- (Performance: O(1).) require not_off: not off feature(s) from DS_CURSOR -- Status report same_position (other: like Current): BOOLEAN -- Is current cursor at same position as other? require other_not_void: other /= Void feature(s) from DS_CURSOR -- Cursor movement go_to (other: like Current) -- Move cursor to other's position. -- (Performance: O(1).) require other_not_void: other /= Void; valid_cursor: container.valid_cursor(other) ensure same_position: same_position(other) feature(s) from DS_CURSOR -- Duplication copy (other: like Current) -- Copy other to current cursor. require other_not_void: other /= Void ensure is_equal: is_equal(other) feature(s) from DS_CURSOR -- Comparison is_equal (other: like Current): BOOLEAN -- Are other and current cursor at the same position? 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_BILINEAR_CURSOR -- Status report is_last: BOOLEAN -- Is cursor on the last item? ensure not_empty: Result implies not container.is_empty; not_off: Result implies not off; definition: Result implies item = container.last before: BOOLEAN -- Is there no valid position to left of cursor? feature(s) from DS_BILINEAR_CURSOR -- Cursor movement finish -- Move cursor to last position. -- (Performance: O(1).) ensure empty_behavior: container.is_empty implies before; not_empty_behavior: not container.is_empty implies is_last back -- Move cursor to previous position. -- (Performance: O(index).) require not_before: not before search_back (v: G) -- Move to first position at or before current -- position where item and v are equal. -- (Use equality_tester's criterion from container -- if not void, use = criterion otherwise.) -- Move before if not found. -- (Performance: O(index).) require not_off: not off or before go_before -- Move cursor to before position. -- (Performance: O(1).) ensure before: before feature(s) from DS_DYNAMIC_CURSOR -- Element change replace (v: G) -- Replace item at cursor position by v. -- (Performance: O(1).) require not_off: not off ensure replaced: item = v swap (other: DS_DYNAMIC_CURSOR[G]) -- Exchange items at current and other's positions. -- Note: cursors may reference two different containers. require not_off: not off; other_not_void: other /= Void; other_not_off: not other.off ensure new_item: item = old other.item; new_other: other.item = old item feature(s) from DS_INDEXED_CURSOR -- Access index: INTEGER -- Index of current position -- (Performance: O(container.count).) ensure valid_index: valid_index(Result) feature(s) from DS_INDEXED_CURSOR -- Status report valid_index (i: INTEGER): BOOLEAN -- Is i a valid index value? ensure definition: Result = (0 <= i and i <= container.count + 1) feature(s) from DS_INDEXED_CURSOR -- Cursor movement go_i_th (i: INTEGER) -- Move cursor to i-th position. -- (Performance: O(i).) require valid_index: valid_index(i) ensure moved: index = i feature(s) from DS_LIST_CURSOR -- Element change put_left (v: G) -- Add v to left of cursor position. -- Do not move cursors. require extendible: container.extendible(1); not_before: not before ensure one_more: container.count = old container.count + 1 put_right (v: G) -- Add v to right of cursor position. -- Do not move cursors. require extendible: container.extendible(1); not_after: not after ensure one_more: container.count = old container.count + 1 force_left (v: G) -- Add v to left of cursor position. -- Do not move cursors. require not_before: not before ensure one_more: container.count = old container.count + 1 force_right (v: G) -- Add v to right of cursor position. -- Do not move cursors. require not_after: not after ensure one_more: container.count = old container.count + 1 extend_left (other: DS_LINEAR[G]) -- Add items of other to left of cursor position. -- Keep items of other in the same order. -- Do not move cursors. require other_not_void: other /= Void; extendible: container.extendible(other.count); not_before: not before ensure new_count: container.count = old container.count + other.count extend_right (other: DS_LINEAR[G]) -- Add items of other to right of cursor position. -- Keep items of other in the same order. -- Do not move cursors. require other_not_void: other /= Void; extendible: container.extendible(other.count); not_after: not after ensure new_count: container.count = old container.count + other.count append_left (other: DS_LINEAR[G]) -- Add items of other to left of cursor position. -- Keep items of other in the same order. -- Do not move cursors. require other_not_void: other /= Void; not_before: not before ensure new_count: container.count = old container.count + other.count append_right (other: DS_LINEAR[G]) -- Add items of other to right of cursor position. -- Keep items of other in the same order. -- Do not move cursors. require other_not_void: other /= Void; not_after: not after ensure new_count: container.count = old container.count + other.count feature(s) from DS_LIST_CURSOR -- Removal remove -- Remove item at cursor position. -- Move any cursors at this position forth. require not_off: not off ensure one_less: container.count = old container.count - 1 remove_left -- Remove item to left of cursor position. -- Move any cursors at this position forth. require not_empty: not container.is_empty; not_before: not before; not_first: not is_first ensure one_less: container.count = old container.count - 1 remove_right -- Remove item to right of cursor position. -- Move any cursors at this position forth. require not_empty: not container.is_empty; not_after: not after; not_last: not is_last ensure one_less: container.count = old container.count - 1 prune_left (n: INTEGER) -- Remove n items to left of cursor position. -- Move all cursors off. require valid_n: 0 <= n and n < index ensure new_count: container.count = old container.count - n prune_right (n: INTEGER) -- Remove n items to right of cursor position. -- Move all cursors off. require valid_n: 0 <= n and n <= container.count - index ensure new_count: container.count = old container.count - n invariant container_not_void: container /= Void; -- The following assertion are commented out because -- some Eiffel compilers check invariants even when the -- execution of the creation procedure is not completed. -- (In this case, this is container which is not fully -- created yet, breaking its invariant.) -- empty_constraint: container.is_empty implies off after_constraint: after implies off; not_both: not (after and before); before_constraint: before implies off; off_definition: off = current_cell = Void; end of DS_LINKED_LIST_CURSOR[G]