note description: "[ Indexable containers, where elements can be inserted and removed at any position. Indexing starts from 1. ]" author: "Nadia Polikarpova" revised_by: "Alexander Kogtenkov" model: sequence manual_inv: true false_guards: true deferred class V_LIST [G] inherit V_MUTABLE_SEQUENCE [G] redefine item, at, is_model_equal end feature -- Access item alias "[]" (i: INTEGER): G -- Value at index `i'. deferred ensure then definition_sequence: Result = sequence [i] end feature -- Measurement lower: INTEGER -- Lower bound of index interval. note status: nonvariant do check inv_only ("lower_definition") end Result := 1 end count: INTEGER -- Number of elements. note status: nonvariant do check inv_only ("count_definition", "bag_definition") end Result := count_ end feature -- Iteration at (i: INTEGER): V_LIST_ITERATOR [G] -- New iterator pointing at position `i'. note status: impure explicit: contracts deferred ensure then index_definition_in_bounds: 0 <= i and i <= sequence.count + 1 implies Result.index_ = i end feature -- Extension extend_front (v: G) -- Insert `v' at the front. require observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old sequence.prepended (v) modify_model ("sequence", Current) end extend_back (v: G) -- Insert `v' at the back. require observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old (sequence & v) modify_model ("sequence", Current) end extend_at (v: G; i: INTEGER) -- Insert `v' at position `i'. require valid_index: 1 <= i and i <= sequence.count + 1 observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old sequence.extended_at (i, v) modify_model ("sequence", Current) end append (input: V_ITERATOR [G]) -- Append sequence of values produced by `input'. note status: nonvariant require not_current: input /= Current different_target: input.target /= Current input_target_wrapped: input.target.is_wrapped not_before: not input.before observers_open: ∀ o: observers ¦ o.is_open do from invariant is_wrapped and input.is_wrapped input.inv input.index_.old_ <= input.index_ input.index_ <= input.sequence.count + 1 sequence ~ sequence.old_ + input.sequence.interval (input.index_.old_, input.index_ - 1) until input.after loop extend_back (input.item) input.forth variant input.sequence.count - input.index_ end ensure sequence_effect: sequence ~ old (sequence + input.sequence.tail (input.index_)) input_index_effect: input.index_ = input.sequence.count + 1 modify_model ("sequence", Current) modify_model ("index_", input) end prepend (input: V_ITERATOR [G]) -- Prepend sequence of values produced by `input'. require not_current: input /= Current different_target: input.target /= Current input_target_wrapped: input.target.is_wrapped not_before: not input.before observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old (input.sequence.tail (input.index_) + sequence) input_index_effect: input.index_ = input.sequence.count + 1 observers_preserved: observers ~ old observers modify_model (["sequence", "observers"], Current) modify_model ("index_", input) end insert_at (input: V_ITERATOR [G]; i: INTEGER) -- Insert starting at position `i' sequence of values produced by `input'. require valid_index: 1 <= i and i <= sequence.count + 1 not_current: input /= Current different_target: input.target /= Current input_target_wrapped: input.target.is_wrapped not_before: not input.before observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old (sequence.front (i - 1) + input.sequence.tail (input.index_) + sequence.tail (i)) input_index_effect: input.index_ = input.sequence.count + 1 observers_preserved: observers ~ old observers modify_model (["sequence", "observers"], Current) modify_model ("index_", input) end feature -- Removal remove_front -- Remove first element. require not_empty: not is_empty observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old sequence.but_first modify_model ("sequence", Current) end remove_back -- Remove last element. require not_empty: not is_empty observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old sequence.but_last modify_model ("sequence", Current) end remove_at (i: INTEGER) -- Remove element at position `i'. require has_index: 1 <= i and i <= sequence.count observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence ~ old sequence.removed_at (i) modify_model ("sequence", Current) end remove (v: G) -- Remove the first occurrence of `v'. note status: nonvariant require has: sequence.has (v) observers_open: ∀ o: observers ¦ o.is_open local i: V_LIST_ITERATOR [G] do i := new_cursor i.search_forth (v) i.remove check i.inv_only ("target_bag_constraint", "sequence_definition") end forget_iterator (i) ensure sequence_effect: ∃ j: 1 |..| sequence.count.old_ ¦ sequence.old_ [j] = v and not sequence.old_.front (j - 1).has (v) and sequence ~ sequence.old_.removed_at (j) observers_restored: observers ~ old observers modify_model (["sequence", "observers"], Current) end remove_all (v: G) -- Remove all occurrences of `v'. note status: nonvariant require observers_open: ∀ o: observers ¦ o.is_open local i: V_LIST_ITERATOR [G] n_, j_: INTEGER do from i := new_cursor i.search_forth (v) invariant is_wrapped and i.is_wrapped i.inv_only ("sequence_definition", "index_constraint", "target_bag_constraint") 1 <= i.index_ and i.index_ <= sequence.count + 1 not i.off implies i.item = v not sequence.front (i.index_ - 1).has (v) sequence.count + n_ = sequence.old_.count sequence.front (i.index_ - 1) = removed_all (sequence.old_.front (i.index_ + n_ - 1), v) ∀ j: i.index_ |..| sequence.count ¦ sequence [j] = sequence.old_ [j + n_] n_ >= 0 modify_model ("sequence", Current) modify_model (["index_", "sequence"], i) until i.after loop use_definition (removed_all (sequence.old_.front (i.index_ + n_), v)) check sequence.old_.front (i.index_ + n_).but_last = sequence.old_.front (i.index_ + n_ - 1) end i.remove check i.inv_only ("target_bag_constraint", "sequence_definition") end j_ := i.index_ i.search_forth (v) check sequence.old_.front (i.index_ + n_) = sequence.old_.front (j_ + n_) + sequence.old_.interval (j_ + n_ + 1, i.index_ + n_) end check sequence.interval (j_, i.index_ - 1) = sequence.old_.interval (j_ + n_ + 1, i.index_ + n_) end lemma_removed_all_concat (sequence.old_.front (j_ + n_), sequence.old_.interval (j_ + n_ + 1, i.index_ + n_), v) n_ := n_ + 1 variant i.sequence.count - i.index_ end bag.old_.lemma_remove_all (v) forget_iterator (i) ensure sequence_effect: sequence ~ removed_all (old sequence, v) observers_restored: observers ~ old observers modify_model (["sequence", "observers"], Current) end wipe_out -- Remove all elements. require observers_open: ∀ o: observers ¦ o.is_open deferred ensure sequence_effect: sequence.is_empty modify_model ("sequence", Current) end feature {V_LIST, V_LIST_ITERATOR} -- Implementation count_: INTEGER -- Number of elements. feature -- Specification is_model_equal (other: like Current): BOOLEAN -- Is the abstract state of `Current' equal to that of `other'? note status: ghost, functional, nonvariant do Result := sequence ~ other.sequence end removed_all (s: like sequence; x: G): like sequence -- Sequence `s' with all occurrences of `x' removed. note status: ghost, functional, nonvariant, static, opaque require reads ([]) do Result := if s.is_empty then s else if s.last = x then removed_all (s.but_last, x) else removed_all (s.but_last, x) & s.last end end ensure not Result.has (x) not s.has (x) implies Result = s end lemma_removed_all_concat (s1, s2: like sequence; x: G) -- `removed_all' distributes over sequence concatenation. note status: lemma, static do use_definition (removed_all (s2, x)) if not s2.is_empty then check (s1 + s2).but_last = s1 + s2.but_last end lemma_removed_all_concat (s1, s2.but_last, x) use_definition (removed_all (s1 + s2, x)) else check s1 + s2 = s1 end end ensure removed_all (s1 + s2, x) = removed_all (s1, x) + removed_all (s2, x) end invariant lower_definition: lower_ = 1 count_definition: count_ = sequence.count 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