indexing
	description: "Simple tables"
	author: "Patrick Schoenbach"
	access: index
	representation: array
	size: fixed
	contents: generic

class interface
	SIMPLE_TABLE [G]

create 

	make (n: INTEGER)
			-- (from DS_ARRAYED_LIST)
		require -- from DS_ARRAYED_LIST
			positive_n: n >= 0
		ensure -- from DS_ARRAYED_LIST
			empty: empty;
			capacity_set: capacity = n

feature -- Access

	i_th (i: INTEGER): G
			-- Item at index i
			-- Was declared in DS_ARRAYED_LIST as synonym of @ and item.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_TABLE
			valid_entry: valid_entry (k)
		require -- from INDEXED_CONTAINER
			valid_index: valid_index (i)

	infix "@" (i: INTEGER): G
			-- Item at index i
			-- Was declared in DS_ARRAYED_LIST as synonym of @ and item.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_TABLE
			valid_entry: valid_entry (k)
		require -- from INDEXED_CONTAINER
			valid_index: valid_index (i)
	
feature -- Measurement

	capacity: INTEGER
			-- Maximum number of items in list
			-- (from DS_ARRAYED_LIST)

	count: INTEGER
			-- Number of items in list
			-- (from DS_ARRAYED_LIST)
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is list equal to other?
			-- (from DS_ARRAYED_LIST)
		require -- DS_CONTAINER
			precursor: True
		require -- from GENERAL
			other_not_void: other /= void
		ensure then -- from DS_CONTAINER
			same_count: Result implies count = other.count
		ensure -- from GENERAL
			symmetric: Result implies other.is_equal (Current);
			consistent: standard_is_equal (other) implies Result
	
feature -- Status report

	full: BOOLEAN
			-- Is container full?

	empty: BOOLEAN
			-- Is structure empty?
			-- (from DS_CONTAINER)

	Resizable: BOOLEAN is true
			-- Is container resizable? (Answer: Yes)

	valid_index (i: INTEGER): BOOLEAN
			-- Is i a valid index?
			-- (from DS_INDEXABLE)
		ensure then -- from DS_INDEXABLE
			definition: Result = (1 <= i and i <= count + 1)
		ensure then -- from DS_INDEXABLE
			definition: Result = (1 <= i and i <= count + 1)
	
feature -- Element change

	put (v: G; i: INTEGER)
			-- Add v at i-th position.
			-- (from DS_ARRAYED_LIST)
		require -- from DS_INDEXABLE
			extendible: extendible (1);
			valid_index: valid_index (i)
		require -- from INDEXED_CONTAINER
			not_full: not full;
			valid_index: valid_index (i)
		ensure -- from DS_INDEXABLE
			one_more: count = old count + 1;
;
			inserted: i_th (i) = v
		ensure -- from INDEXED_CONTAINER
			extended: i_th (i) = v
	
feature -- Duplication

	copy (other: like Current)
			-- Copy other to current list.
			-- (from DS_ARRAYED_LIST)
		require -- from GENERAL
			other_not_void: other /= void;
			type_identity: same_type (other)
		ensure -- from GENERAL
			is_equal: is_equal (other)
	
feature -- removal

	wipe_out
			-- Remove all items from list.
			-- (from DS_ARRAYED_LIST)
		require -- DS_CONTAINER
			precursor: True
		require -- from INDEXED_CONTAINER
			not_empty: not empty
		ensure -- from DS_CONTAINER
			wipe_out: empty
		ensure -- from INDEXED_CONTAINER
			empty: empty
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
		-- from INDEXED_CONTAINER
	empty_definition: empty = (count = 0);
	full_definition: full = (count = capacity);
		-- from DS_CONTAINER
	positive_count: count >= 0;
	empty_definition: empty = (count = 0);
		-- from DS_RESIZABLE
	count_constraint: count <= capacity;

end -- class SIMPLE_TABLE