note description: "[ Two-dimensional arrays. Indexing of rows and columns starts from 1. ]" author: "Nadia Polikarpova" revised_by: "Alexander Kogtenkov" model: sequence, column_count manual_inv: true false_guards: true class V_ARRAY2 [G] inherit V_MUTABLE_SEQUENCE [G] rename item as flat_item, put as flat_put, at as flat_at redefine upper, is_equal_, is_model_equal end create make, make_filled feature {NONE} -- Initialization make (n, m: INTEGER) -- Create array with `n' rows and `m' columns; set all values to default. note status: creator require valid_dimensions: (n = 0 and m = 0) or (n > 0 and m > 0) do row_count := n column_count := m create array.make (1, n * m) create sequence.constant (({G}).default, n * m) ensure sequence_domain_definition: sequence.count = n * m sequence_definition: sequence.is_constant (({G}).default) column_count_definition: column_count = m no_observers: observers.is_empty end make_filled (n, m: INTEGER; v: G) -- Create array with `n' rows and `m' columns; set all values to `v'. note status: creator require valid_dimensions: (n = 0 and m = 0) or (n > 0 and m > 0) do row_count := n column_count := m create array.make_filled (1, n * m, v) create sequence.constant (v, n * m) ensure sequence_domain_definition: sequence.count = n * m sequence_definition: sequence.is_constant (v) column_count_definition: column_count = m no_observers: 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 row_count := other.row_count column_count := other.column_count other.unwrap create array.copy_ (other.array) other.wrap sequence := other.sequence end ensure then sequence_effect: sequence ~ other.sequence column_count_effect: column_count = other.column_count observers_open: ∀ o: observers ¦ o.is_open modify_model (["sequence", "column_count"], Current) modify_field ("closed", other) end feature -- Access item alias "[]" (i, j: INTEGER): G assign put -- Item at row `i' and column `j'. require valid_row: has_row (i) valid_column: has_column (j) do check inv end Result := flat_item (flat_index (i, j)) ensure definition: Result = sequence [flat_index (i, j)] end flat_item (i: INTEGER): G assign flat_put -- Item at dlat index `i'. do check inv end Result := array [i] end feature -- Measurement row_count: INTEGER -- Number of rows. column_count: INTEGER -- Number of columns. count: INTEGER -- Number of elements. do check inv end Result := row_count * column_count end flat_index (i, j: INTEGER): INTEGER -- Flat index at row `i' and column `j'. note status: functional require 1 <= i and i <= row_count 1 <= j and j <= column_count do Result := (i - 1) * column_count + j end row_index (i: INTEGER): INTEGER -- Row that corresponds to flat index `i'. note status: functional require non_empty: column_count > 0 do Result := (i - 1) // column_count + 1 end column_index (i: INTEGER): INTEGER -- Column that corresponds to flat index `i'. note status: functional require non_empty: column_count > 0 do Result := (i - 1) \\ column_count + 1 end Lower: INTEGER = 1 -- Lower flat index. upper: INTEGER -- Upper flat_index. do check inv end Result := row_count * column_count end feature -- Search has_row (i: INTEGER): BOOLEAN -- Does array contain row `i'? note status: functional do Result := 1 <= i and i <= row_count end has_column (j: INTEGER): BOOLEAN -- Does array contain column `j'? note status: functional do Result := 1 <= j and j <= column_count end feature -- Iteration flat_at (i: INTEGER): V_ARRAY_ITERATOR [G] -- New iterator pointing at flat position `i'. note status: impure do check inv end create Result.make (Current, i) end feature -- Comparison is_equal_ (other: like Current): BOOLEAN -- Is array made of the same items as `other'? -- (Use reference comparison.) do if other = Current then Result := True else check inv; other.inv; array.inv; other.array.inv end Result := column_count = other.column_count and array.is_equal_ (other.array) end end feature -- Replacement put (v: G; i, j: INTEGER) -- Replace value at row `i' and column `j' with `v'. note explicit: wrapping require valid_row: has_row (i) valid_column: has_column (j) observers_open: ∀ o: observers ¦ o.is_open do check inv end flat_put (v, flat_index (i, j)) ensure sequence_effect: sequence ~ old sequence.replaced_at (flat_index (i, j), v) modify_model ("sequence", Current) end flat_put (v: G; i: INTEGER) -- Replace value at position `i' with `v'. do array.put (v, i) sequence := sequence.replaced_at (i, v) end feature {V_CONTAINER, V_ITERATOR} -- Implemantation array: V_ARRAY [G] -- Flat representation. feature -- Specification is_model_equal (other: like Current): BOOLEAN -- Is the abstract state of `Current' equal to that of `other'? note status: ghost, functional do Result := sequence ~ other.sequence and column_count = other.column_count end invariant array_exists: array /= Void owns_definition: owns ~ create {MML_SET [ANY]}.singleton (array) array_lower_definition: array.lower_ = 1 array_no_observers: array.observers.is_empty sequence_implementation: sequence = array.sequence lower_definition: lower_ = 1 column_count_empty: sequence.is_empty implies column_count = 0 column_count_nonempty: not sequence.is_empty implies column_count > 0 row_count_definition: row_count * column_count = sequence.count note 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