deferred class interface DS_INDEXED_CURSOR[G] feature(s) from DS_CURSOR -- Access item: G -- Item at cursor position require not_off: not off container: DS_TRAVERSABLE[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_INDEXED_CURSOR -- Access index: INTEGER -- Index of current position 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? feature(s) from DS_INDEXED_CURSOR -- Cursor movement go_i_th (i: INTEGER) -- Move cursor to i-th position. require valid_index: valid_index(i) ensure moved: index = i 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 end of deferred DS_INDEXED_CURSOR[G]