note description: "[ Iterators to read from a container in linear order. Indexing starts from 1. ]" author: "Nadia Polikarpova" revised_by: "Alexander Kogtenkov" model: target, sequence, index_ manual_inv: true false_guards: true deferred class V_ITERATOR [G] inherit V_INPUT_STREAM [G] rename search as search_forth redefine item, search_forth end ITERATION_CURSOR [G] rename after as off redefine item end feature -- Access target: V_CONTAINER [G] -- Container to iterate over. item: G -- Item at current position. deferred ensure then definition: Result = sequence [index_] end feature -- Measurement index: INTEGER -- Current position. require subjects_closed: subjects.any_item.closed deferred ensure definition: Result = index_ end valid_index (i: INTEGER): BOOLEAN -- Is `i' a valid position for a cursor? note status: functional, ghost, nonvariant require target_exists: target /= Void reads (Current, target) do Result := 0 <= i and i <= target.bag.count + 1 end feature -- Status report before: BOOLEAN -- Is current position before any position in `target'? deferred ensure definition: Result = (index_ = 0) end after: BOOLEAN -- Is current position after any position in `target'? require target.closed deferred ensure definition: Result = (index_ = sequence.count + 1) end off: BOOLEAN -- Is current position off scope? note status: nonvariant do check inv end Result := before or after ensure then new_definition: Result = not sequence.domain [index_] end is_first: BOOLEAN -- Is cursor at the first position? require target_closed: target.closed deferred ensure definition: Result = (not sequence.is_empty and index_ = 1) end is_last: BOOLEAN -- Is cursor at the last position? require target_closed: target.closed deferred ensure definition: Result = (not sequence.is_empty and index_ = sequence.count) end feature -- Cursor movement start -- Go to the first position. require target_closed: target.closed deferred ensure index_effect: index_ = 1 target_closed: target.closed modify_model ("index_", Current) end finish -- Go to the last position. require target_closed: target.closed deferred ensure index_effect: index_ = sequence.count target_closed: target.closed modify_model ("index_", Current) end forth -- Go one position forward. deferred ensure then index_effect: index_ = old index_ + 1 end back -- Go one position backward. require not_off: not off target_closed: target.closed deferred ensure index_effect: index_ = old index_ - 1 target_closed: target.closed modify_model ("index_", Current) end go_to (i: INTEGER) -- Go to position `i'. note status: nonvariant require has_index: valid_index (i) target_wrapped: target.is_wrapped local j: INTEGER do check inv end if i = 0 then go_before elseif i = target.count + 1 then go_after elseif i = target.count then finish else from start j := 1 invariant is_wrapped sequence.domain [i] j_in_bounds: 1 <= j and j <= i index_counter: index_ = j until j = i loop check inv end forth j := j + 1 end end ensure index_effect: index_ = i modify_model ("index_", Current) end go_before -- Go before any position of `target'. deferred ensure index_effect: index_ = 0 modify_model ("index_", Current) end go_after -- Go after any position of `target'. require target_closed: target.closed deferred ensure index_effect: index_ = sequence.count + 1 target_closed: target.closed modify_model ("index_", Current) end search_forth (v: G) -- Move to the first occurrence of `v' at or after current position. -- If `v' does not occur, move `after'. -- (Use reference equality.) note status: nonvariant do check inv_only ("subjects_definition") end if before then start end from invariant is_wrapped inv_only ("index_constraint", "box_definition") target.is_wrapped index_.old_ <= index_ and index_ <= sequence.count + 1 not before ∀ i: index_.old_.max (1) |..| (index_ - 1) ¦ sequence [i] /= v until after or else item = v loop forth variant sequence.count - index_ end ensure then index_effect_not_found: not sequence.tail (old index_).has (v) implies index_ = sequence.count + 1 index_effect_found: sequence.tail (old index_).has (v) implies index_ >= old index_ and sequence [index_] = v index_constraint: not sequence.interval (old index_, index_ - 1).has (v) end search_back (v: G) -- Move to the last occurrence of `v' at or before current position. -- If `v' does not occur, move `before'. -- (Use reference equality.) note status: nonvariant require target_wrapped: target.is_wrapped do if after then finish end from invariant is_wrapped inv_only ("index_constraint", "subjects_definition") target.is_wrapped 0 <= index_ index_ <= index_.old_ index_ <= sequence.count ∀ i: (index_ + 1) |..| index_.old_.min (sequence.count) ¦ sequence [i] /= v until before or else item = v loop back variant index_ end ensure index_effect_not_found: not sequence.front (old index_).has (v) implies index_ = 0 index_effect_found: sequence.front (old index_).has (v) implies (sequence [index_] = v and not sequence.interval (index_ + 1, old index_).has (v)) modify_model ("index_", Current) end feature -- Specification sequence: MML_SEQUENCE [G] -- Sequence of elements in `target'. note status: ghost attribute check is_executable: False then end end index_: INTEGER -- Current position. note status: ghost replaces: box attribute end invariant target_exists: target /= Void subjects_definition: subjects ~ create {MML_SET [ANY]}.singleton (target) target_bag_constraint: target.bag ~ sequence.to_bag index_constraint: 0 <= index_ and index_ <= sequence.count + 1 box_definition: box ~ if sequence.domain [index_] then create {MML_SET [G]}.singleton (sequence [index_]) else {MML_SET [G]}.empty_set end note copyright: "Copyright (c) 1984-2021, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end