indexing
	description: "Multi-dimensional array"
	status: "See notice at end of class"
	representation: array
	access: multi_dimensional_index
	size: resizable
	contents: generic
	date: "$Date$"
	revision: "$Revision$"

class interface
	ECOM_ARRAY [G]

create 

	make (a_dimension_count: INTEGER; some_lower_indices, some_element_counts: ARRAY [INTEGER])
			-- Create a_dimensional_count dimensional array
			-- with lower indices in each dimension as described by some_lower_indices
			-- and element count in each dimension as described by some_element_counts.
		require
			valid_dimension_count: a_dimension_count >= 0
			valid_lower_indices: some_lower_indices /= void and then some_lower_indices.count = a_dimension_count and (a_dimension_count > 0 implies some_lower_indices.lower = 1)
			valid_element_count: some_element_counts /= void and then some_element_counts.count = a_dimension_count and (a_dimension_count > 0 implies some_element_counts.lower = 1) and then are_element_counts_valid (some_element_counts)
		ensure
			valid_dimension_count: dimension_count >= 0
			valid_element_counts: element_counts /= void and then element_counts.count = dimension_count
			valid_lower_indices: lower_indices /= void and then lower_indices.count = dimension_count
			valid_upper_indices: upper_indices /= void and then upper_indices.count = dimension_count

	make_from_array (a: ARRAY [G]; a_dimension_count: INTEGER; some_lower_indices, some_element_counts: ARRAY [INTEGER])
			-- Create a_dimensional_count dimensional array
			-- with lower indices in each dimension as described by some_lower_indices
			-- and element count in each dimension as described by some_element_counts.
		require
			valid_dimension_count: a_dimension_count >= 0
			valid_lower_indices: some_lower_indices /= void and then some_lower_indices.count = a_dimension_count and (a_dimension_count > 0 implies some_lower_indices.lower = 1)
			valid_element_count: some_element_counts /= void and then some_element_counts.count = a_dimension_count and (a_dimension_count > 0 implies some_element_counts.lower = 1) and then are_element_counts_valid (some_element_counts)
			valid_array_size: a.count >= total_count (some_element_counts)
		ensure
			valid_dimension_count: dimension_count >= 0
			valid_element_counts: element_counts /= void and then element_counts.count = dimension_count
			valid_lower_indices: lower_indices /= void and then lower_indices.count = dimension_count
			valid_upper_indices: upper_indices /= void and then upper_indices.count = dimension_count

	make_empty
			-- Create empty array.

feature -- Initialization

	initialize (v: G)
			-- Make each entry have value v
	
feature -- Access

	item (some_indices: ARRAY [INTEGER]): G
			-- Entry at some_indices
		require
			valid_indices: are_indices_valid (some_indices)
	
feature  -- Access

	area: SPECIAL [G]
			-- Special data zone
			-- (from TO_SPECIAL)

	array_item (i: INTEGER): G
			-- Entry at index i, if in index interval
			-- Was declared in ARRAY as synonym of @.
			-- (from ARRAY)
		require -- from TABLE
			valid_key: valid_index (k)
	
feature -- Measurement

	dimension_count: INTEGER
			-- Number of dimensions

	element_counts: ARRAY [INTEGER]
			-- Element count in each dimension

	lower_indices: ARRAY [INTEGER]
			-- Lower indedeces in each dimension

	upper_indices: ARRAY [INTEGER]
			-- Upper indices in each dimension
	
feature  -- Measurement

	count: INTEGER
			-- Number of available indices
			-- Was declared in ARRAY as synonym of capacity.
			-- (from ARRAY)
		ensure then -- from ARRAY
			consistent_with_bounds: Result = upper - lower + 1
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is array made of the same items as other?
			-- (from ARRAY)
		require -- from ANY
			other_not_void: other /= void
		ensure -- from ANY
			symmetric: Result implies other.is_equal (Current)
			consistent: standard_is_equal (other) implies Result
	
feature -- Status report

	are_element_counts_consistent: BOOLEAN
			-- Are element_counts consistent?

	are_element_counts_valid (some_element_counts: ARRAY [INTEGER]): BOOLEAN
			-- Are some_element_counts valid element counts?
		require
			non_void_element_counts: some_element_counts /= void
			valid_element_counts: (some_element_counts.count > 0 implies some_element_counts.lower = 1)

	are_indices_large_enough (some_indices: ARRAY [INTEGER]): BOOLEAN
			-- Are some_indices large enough?

	are_indices_valid (some_indices: ARRAY [INTEGER]): BOOLEAN
			-- Are some_indices valid indices?

	total_count (some_element_counts: ARRAY [INTEGER]): INTEGER
			-- Total number of elements
		require
			valid_counts: are_element_counts_valid (some_element_counts)
		ensure
			valid_count: Result >= 0
	
feature -- Element change

	force (v: like item; some_indices: ARRAY [INTEGER])
			-- Assign item v at indices some_indices.
			-- Resize if necesary.
		require
			valid_indices: are_indices_large_enough (some_indices)
		ensure
			element_inserted: item (some_indices) = v

	put (v: like item; some_indices: ARRAY [INTEGER])
			-- Assign item v at indices some_indices.
		require
			valid_indices: are_indices_valid (some_indices)
		ensure
			element_inserted: item (some_indices) = v
	
feature -- Removal

	discard_items
			-- Remove all elements
		ensure -- from ARRAY
			default_items: all_default
	
feature -- Resizing

	resize (n_upper_indices: ARRAY [INTEGER])
			-- Rearrange array so that it can accommodate n_upper_indices
			-- without losing any previously entered items
			-- or changing their indices;
			-- do nothing if possible.
		require
			are_indices_large_enough (n_upper_indices)
	
feature -- Duplication

	copy (other: like Current)
			-- Reinitialize by copying all the items of other.
			-- (This is also used by clone.)
			-- (from ARRAY)
		require -- from ANY
			other_not_void: other /= void
			type_identity: same_type (other)
		ensure -- from ANY
			is_equal: is_equal (other)
		ensure then -- from ARRAY
			equal_areas: area.is_equal (other.area)
	
invariant

	consistent_upper_indices: upper_indices.count = dimension_count
	consistent_lower_indices: lower_indices.count = dimension_count
	consistent_element_counts: are_element_counts_consistent
	consistent_size: capacity = total_count (element_counts)
	non_negative_count: count >= 0
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from ARRAY
	area_exists: area /= void
	consistent_size: capacity = upper - lower + 1
	non_negative_count: count >= 0
	index_set_has_same_count: valid_index_set
		-- from RESIZABLE
	increase_by_at_least_one: minimal_increase >= 1
		-- from BOUNDED
	valid_count: count <= capacity
	full_definition: full = (count = capacity)
		-- from FINITE
	empty_definition: is_empty = (count = 0)
	non_negative_count: count >= 0
		-- from INDEXABLE
	index_set_not_void: index_set /= void

end -- class ECOM_ARRAY