note description: "[ Lists implemented as ring buffers. The size of list might be smaller than the size of underlying array. Random access is constant time. Inserting or removing elements at front or back is amortized constant time. Inserting or removing elements in the middle is linear time. ]" author: "Nadia Polikarpova" revised_by: "Alexander Kogtenkov" model: sequence manual_inv: true false_guards: true class V_ARRAYED_LIST [G] inherit V_LIST [G] redefine default_create, is_equal_ end feature {NONE} -- Initialization default_create -- Create an empty list with default `capacity' and `growth_rate'. note status: creator do create array.make (0, default_capacity - 1) ensure then sequence_effect: sequence.is_empty observers_empty: observers.is_empty end feature -- Initialization copy_ (other: like Current) -- Initialize by copying all the items of `other'. require observers_open: ∀ o: observers ¦ o.is_open do if other /= Current then other.unwrap create array.copy_ (other.array) other.wrap first_index := other.first_index count_ := other.count_ sequence := other.sequence end ensure sequence_effect: sequence ~ old other.sequence modify_model ("sequence", Current) modify_field ("closed", other) end feature -- Access item alias "[]" (i: INTEGER): G assign put -- Value associated with `i'. do check inv end Result := array [array_index (i)] end feature -- Iteration at (i: INTEGER): V_ARRAYED_LIST_ITERATOR [G] -- New iterator pointing at position `i'. note status: impure do create Result.make (Current, i) check Result.inv end check inv_only ("lower_definition") end end feature -- Comparison is_equal_ (other: like Current): BOOLEAN -- Is list made of the same values in the same order as `other'? -- (Use reference comparison.) local i: INTEGER do if other = Current then Result := True elseif count = other.count then from Result := True i := 1 invariant 1 <= i and i <= sequence.count + 1 inv other.inv if Result then ∀ k: 1 |..| (i - 1) ¦ sequence [k] = other.sequence [k] else sequence [i - 1] /= other.sequence [i - 1] end until i > count_ or not Result loop Result := item (i) = other.item (i) i := i + 1 variant sequence.count - i end end end feature -- Replacement put (v: G; i: INTEGER) -- Associate `v' with index `i'. do array.put (v, array_index (i)) sequence := sequence.replaced_at (i, v) end feature -- Extension extend_front (v: G) -- Insert `v' at the front. note explicit: wrapping do reserve (count_ + 1) unwrap if count_ = 0 then array [0] := v first_index := 0 else first_index := mod_capacity (first_index - 1) array [first_index] := v end count_ := count_ + 1 sequence := sequence.prepended (v) wrap end extend_back (v: G) -- Insert `v' at the back. note explicit: wrapping do reserve (count_ + 1) unwrap count_ := count_ + 1 array [array_index (count_)] := v sequence := sequence & v wrap end extend_at (v: G; i: INTEGER) -- Insert `v' at position `i'. note explicit: wrapping do check inv_only ("count_definition") end if i = 1 then extend_front (v) check sequence = sequence.old_.extended_at (i, v) end elseif i = count_ + 1 then extend_back (v) check sequence = sequence.old_.extended_at (i, v) end else reserve (count_ + 1) unwrap count_ := count_ + 1 circular_copy (i, i + 1, count_ - i) array [array_index (i)] := v sequence := sequence.extended_at (i, v) wrap end end prepend (input: V_ITERATOR [G]) -- Prepend sequence of values, over which `input' iterates. note explicit: wrapping do insert_at (input, 1) end insert_at (input: V_ITERATOR [G]; i: INTEGER) -- Insert sequence of values, over which `input' iterates, starting at position `i'. note explicit: wrapping local ic, j, new_capacity: INTEGER do check input.inv_only ("subjects_definition", "index_constraint", "target_bag_constraint") end ic := input.target.count - input.index + 1 reserve (count_ + ic) unwrap if i < count_ + 1 then circular_copy (i, i + ic, count_ - i + 1) end new_capacity := array.sequence.count sequence := sequence.front (i - 1) + input.sequence.tail (input.index) + sequence.tail (i) from j := 0 invariant 0 <= j and j <= ic input.index_ = input.index_.old_ + j array.is_wrapped input.is_wrapped array.sequence.count = new_capacity ∀ k: 1 |..| sequence.count ¦ k <= i - 1 + j or i + ic <= k implies sequence [k] = array.sequence [array_seq_index (k)] modify_model ("sequence", array) modify_model ("index_", input) until input.after loop array [array_index (i + j)] := input.item j := j + 1 input.forth variant ic - j end count_ := count_ + ic wrap end feature -- Removal remove_front -- Remove first element. do first_index := mod_capacity (first_index + 1) count_ := count_ - 1 sequence := sequence.but_first end remove_back -- Remove last element. do count_ := count_ - 1 sequence := sequence.but_last end remove_at (i: INTEGER) -- Remove element at position `i'. note explicit: wrapping do check inv_only ("count_definition") end if i = 1 then remove_front elseif i = count_ then remove_back else unwrap circular_copy (i + 1, i, count_ - i) count_ := count_ - 1 sequence := sequence.removed_at (i) wrap end end wipe_out -- Remove all elements. do count_ := 0 create sequence end feature {V_CONTAINER, V_ITERATOR} -- Implementation array: V_ARRAY [G] -- Element storage. first_index: INTEGER -- Index of the first list element in `array'. feature {NONE} -- Implementation frozen capacity: INTEGER -- Size of the underlying array. require array_closed: array.closed reads (universe) do Result := array.count ensure Result = array.sequence.count end default_capacity: INTEGER = 8 -- Default value for `capacity'. growth_rate: INTEGER = 2 -- Minimum number by which underlying array grows when resized. frozen mod_capacity (i: INTEGER): INTEGER -- `i' modulo `capacity' in range [`0', `capacity' - 1]. require array_closed: array.closed i_in_bounds: -1 <= i and i < 2 * array.sequence.count inv_only ("array_non_empty") reads (universe) do Result := (i + capacity) \\ capacity ensure in_bounds: 0 <= Result and Result < array.sequence.count i = -1 implies Result = array.sequence.count - 1 0 <= i and i < array.sequence.count implies Result = i array.sequence.count <= i implies Result = i - array.sequence.count end frozen array_index (i: INTEGER): INTEGER -- Position in `array' of `i'th list element. require array_closed: array.closed inv_only ("array_non_empty", "first_index_in_bounds") i_in_bounds: 1 <= i and i <= array.sequence.count reads (universe) do Result := mod_capacity (i - 1 + first_index) ensure Result = array_seq_index (i) - 1 end circular_copy (src, dest, n: INTEGER) -- Copy `n' elements from position `src' to position `dest'. require array_wrapped: array.is_wrapped n_non_neagtive: n >= 0 src_non_negative: 1 <= src and src <= array.sequence.count - n + 1 dest_in_bounds: 1 <= dest and dest <= array.sequence.count - n + 1 inv_only ("array_non_empty", "first_index_in_bounds", "array_no_observers", "array_starts_from_zero") local i: INTEGER do if src < dest then from i := n invariant i_in_bounds: 0 <= i and i <= n array_wrapped: array.is_wrapped inv_only ("array_non_empty", "first_index_in_bounds", "array_no_observers", "array_starts_from_zero") array.sequence.count = array.sequence.count.old_ ∀ k: (array_index_set (dest + i, dest + n - 1)) ¦ array.sequence [k] = array.sequence.old_ [array_seq_index (list_index (k) - dest + src)] ∀ k: 1 |..| array.sequence.count ¦ not array_index_set (dest + i, dest + n - 1) [k] implies array.sequence [k] = array.sequence.old_ [k] until i < 1 loop array [array_index (dest + i - 1)] := array [array_index (src + i - 1)] i := i - 1 end check ∀ k: (array_index_set (dest, dest + n - 1)) ¦ array.sequence [k] = array.sequence.old_ [array_seq_index (list_index (k) - dest + src)] end elseif src > dest then from i := 1 invariant i_in_bounds: 1 <= i and i <= n + 1 array_wrapped: array.is_wrapped inv_only ("array_non_empty", "first_index_in_bounds", "array_no_observers", "array_starts_from_zero") array.sequence.count = array.sequence.count.old_ ∀ k: (array_index_set (dest, dest + i - 2)) ¦ array.sequence [k] = array.sequence.old_ [array_seq_index (list_index (k) - dest + src)] ∀ k: 1 |..| array.sequence.count ¦ not array_index_set (dest, dest + i - 2) [k] implies array.sequence [k] = array.sequence.old_ [k] until i > n loop array [array_index (dest + i - 1)] := array [array_index (src + i - 1)] i := i + 1 end check ∀ k: (array_index_set (dest, dest + n - 1)) ¦ array.sequence [k] = array.sequence.old_ [array_seq_index (list_index (k) - dest + src)] end end ensure array_wrapped: array.is_wrapped inv_only ("array_non_empty", "first_index_in_bounds", "array_no_observers", "array_starts_from_zero") sequence_domain_effect: array.sequence.count = old array.sequence.count sequence_effect_new: ∀ k: (array_index_set (dest, dest + n - 1)) ¦ ∀ l: 1 |..| array.sequence.count ¦ l = array_seq_index (list_index (k) - dest + src) implies array.sequence [k] = (old array.sequence) [l] sequence_effect_old: ∀ k: 1 |..| array.sequence.count ¦ not array_index_set (dest, dest + n - 1) [k] implies array.sequence [k] = array.sequence.old_ [k] modify_model ("sequence", array) end reserve (n: INTEGER) -- Make sure `array' can accommodate `n' elements; -- Do not resize by less than `growth_rate'. note explicit: contracts require wrapped: is_wrapped observers_open: ∀ o: observers ¦ o.is_open local old_size, new_size: INTEGER do unwrap if capacity < n then old_size := capacity new_size := n.max (capacity * growth_rate) array.resize (0, new_size - 1) if first_index + count_ > old_size then array.copy_range_within (first_index, old_size - 1, new_size - old_size + first_index) array.clear (first_index, (old_size - 1).min (new_size - old_size + first_index - 1)) first_index := new_size - old_size + first_index end end wrap ensure at_least_n: array.sequence.count >= n at_least_old: array.sequence.count >= old array.sequence.count wrapped: is_wrapped modify_field (["first_index", "closed"], Current) end feature {NONE} -- Specification array_seq_index (i: INTEGER): INTEGER -- Index in `array.sequence' that corresponds to index `i' in `sequence'. note status: ghost, functional require array_exists: array /= Void i_in_bounds: 1 <= i and i <= array.sequence.count inv_only ("first_index_in_bounds") reads_field (["array", "first_index"], Current) reads_field ("sequence", array) do Result := if i + first_index <= array.sequence.count then i + first_index else i + first_index - array.sequence.count end ensure result_in_bounds: 1 <= Result and Result <= array.sequence.count end list_index (i: INTEGER): INTEGER -- Index in `sequence' that corresponds to index `i' in `array.sequence'. note status: ghost, functional require array_exists: array /= Void i_in_bounds: 1 <= i and i <= array.sequence.count inv_only ("first_index_in_bounds") reads_field (["array", "first_index"], Current) reads_field ("sequence", array) do Result := if i - first_index >= 1 then i - first_index else i - first_index + array.sequence.count end ensure result_in_bounds: 1 <= Result and Result <= array.sequence.count end array_index_set (lo, hi: INTEGER): MML_SET [INTEGER] -- Set of indexes in `array_sequence' that corresponds to index interval `i'..`j' in `sequence'. note status: ghost, functional require array_exists: array /= Void lo_large_enough: 1 <= lo + first_index hi_small_enough: hi + first_index <= 2 * array.sequence.count inv_only ("first_index_in_bounds") reads_field (["array", "first_index"], Current) reads_field ("sequence", array) do Result := create {MML_INTERVAL}.from_range (lo + first_index, (hi + first_index).min (array.sequence.count)) + create {MML_INTERVAL}.from_range ((lo + first_index - array.sequence.count).max (1), hi + first_index - array.sequence.count) ensure result_in_domain: Result <= array.sequence.domain end invariant array_exists: array /= Void owns_definition: owns ~ create {MML_SET [ANY]}.singleton (array) array_non_empty: array.sequence.count > 0 array_starts_from_zero: array.lower_ = 0 first_index_in_bounds: 0 <= first_index and first_index < array.sequence.count sequence_count_constraint: sequence.count <= array.sequence.count sequence_implementation: ∀ i: 1 |..| sequence.count ¦ sequence [i] = array.sequence [array_seq_index (i)] array_no_observers: array.observers.is_empty note explicit: observers date: "$Date$" revision: "$Revision$" 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