note description: "Streams where values can be output one by one." author: "Nadia Polikarpova" revised_by: "Alexander Kogtenkov" model: off_ manual_inv: true false_guards: true deferred class V_OUTPUT_STREAM [G] feature -- Status report off: BOOLEAN -- Is current position off scope? deferred ensure defintion: Result = off_ end feature -- Replacement output (v: G) -- Put `v' into the stream and move to the next position. require not_off: not off subjects_wrapped: ∀ s: subjects ¦ s.is_wrapped and ∀ o: s.observers ¦ o /= Current implies o.is_open deferred ensure subjects_wrapped: ∀ s: subjects ¦ s.is_wrapped and ∀ o: s.observers ¦ o /= Current implies o.is_open modify_model ("off_", Current) modify (subjects) end pipe (input: V_INPUT_STREAM [G]) -- Copy values from `input' until either `Current' or `input' is `off'. note status: nonvariant require input_wrapped: input.is_wrapped input_not_current: input /= Current subjects_wrapped: ∀ s: subjects ¦ s.is_wrapped and ∀ o: s.observers ¦ o /= Current implies o.is_open input_subjects_wrapped: ∀ s: input.subjects ¦ s.is_wrapped do from invariant is_wrapped and input.is_wrapped inv and input.inv subjects ~ subjects.old_ subjects_wrapped: ∀ s: subjects ¦ s.is_wrapped and ∀ o: s.observers ¦ o /= Current implies o.is_open decreases ([]) until off or input.off loop output (input.item) input.forth end ensure off_effect: off_ or input.box.is_empty modify (Current, subjects) modify_model ("box", input) end pipe_n (input: V_INPUT_STREAM [G]; n: INTEGER) -- Copy `n' elements from `input'; stop if either `Current' or `input' is `off'. note status: nonvariant require input_exists: input.is_wrapped input_not_current: input /= Current n_non_negative: n >= 0 subjects_wrapped: ∀ s: subjects ¦ s.is_wrapped and ∀ o: s.observers ¦ o /= Current implies o.is_open input_subjects_wrapped: ∀ s: input.subjects ¦ s.is_wrapped local i: INTEGER do from i := 1 invariant is_wrapped and input.is_wrapped inv and input.inv subjects ~ subjects.old_ subjects_wrapped: ∀ s: subjects ¦ s.is_wrapped and ∀ o: s.observers ¦ o /= Current implies o.is_open until i > n or off or input.off loop output (input.item) input.forth i := i + 1 variant n - i end ensure modify_model ("box", input) modify (Current, subjects) end feature -- Specification off_: BOOLEAN note status: ghost attribute end invariant subjects_contraint: not subjects [Current] no_observers: observers ~ create {MML_SET [ANY]} 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