deferred class interface DS_LINEAR_CURSOR[G] feature(s) from DS_CURSOR -- Access item: G -- Item at cursor position require not_off: not off container: DS_LINEAR[G] -- Data structure traversed feature(s) from DS_CURSOR -- Status report off: BOOLEAN -- Is there no item at cursor position? 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. 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_LINEAR_CURSOR -- Status report is_first: BOOLEAN -- Is cursor on 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? feature(s) from DS_LINEAR_CURSOR -- Cursor movement start -- Move cursor to first position. ensure empty_behavior: container.is_empty implies after; not_empty_behavior: not container.is_empty implies is_first forth -- Move cursor to next position. 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. ensure after: after 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; end of deferred DS_LINEAR_CURSOR[G]