note
	description: "Iterators to read and write from/to a container in linear order."
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: target, sequence, index_
	manual_inv: true
	false_guards: true

deferred class
	V_IO_ITERATOR [G]

inherit
	V_ITERATOR [G]
		redefine
			sequence,
			index_
		end

	V_OUTPUT_STREAM [G]
		undefine
			is_model_equal
		end

feature -- Replacement

	put (v: G)
			-- Replace item at current position with `v'.
		require
			not_off: not off
			target_wrapped: target.is_wrapped
			target_observers_open: ∀ o: target.observers ¦ o /= Current implies o.is_open
		deferred
		ensure
			sequence_effect: sequence ~ old sequence.replaced_at (index_, v)
			target_wrapped: target.is_wrapped
			target_bag_effect: target.bag ~ old ((target.bag / sequence [index_]) & v)
			modify_model (["sequence", "box"], Current)
			modify_model ("bag", target)
		end

	output (v: G)
			-- Replace item at current position with `v' and go to the next position.
		note
			status: nonvariant
		do
			check inv_only ("subjects_definition", "subjects_contraint") end
			put (v)
			check inv end
			forth
		ensure then
			sequence_effect: sequence ~ old (sequence.replaced_at (index_, v))
			index_effect: index_ = old index_ + 1
		end

feature -- Specification

	sequence: MML_SEQUENCE [G]
			-- Sequence of elements in `target'.
		note
			status: ghost
			replaces: off_
		attribute
		end

	index_: INTEGER
			-- Current position.
		note
			status: ghost
			replaces: off_
		attribute
		end

invariant
	off_definition: off_ = not sequence.domain [index_]

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