indexing
	description: "Simple indexed containers"
	author: "Patrick Schoenbach"
	access: index
	size: fixed
	contents: generic

deferred class interface
	INDEXED_CONTAINER [G]

feature -- Access

	i_th (i: INTEGER): G
			-- i-th item
			-- Was declared in INDEXED_CONTAINER as synonym of i_th and @.
		require
			valid_index: valid_index (i)

	infix "@" (i: INTEGER): G
			-- i-th item
			-- Was declared in INDEXED_CONTAINER as synonym of i_th and @.
		require
			valid_index: valid_index (i)
	
feature -- Measurement

	capacity: INTEGER
			-- Size of history

	count: INTEGER
			-- Number of elements
	
feature -- Status report

	empty: BOOLEAN
			-- Is container empty?

	full: BOOLEAN
			-- Is the container full?

	resizable: BOOLEAN
			-- Is container resizable?

	valid_index (i: INTEGER): BOOLEAN
			-- Is index i valid?
	
feature -- Element change

	put (v: G; i: INTEGER)
			-- Put v at i-th position
		require
			not_full: not full;
			valid_index: valid_index (i)
		ensure
			extended: i_th (i) = v
	
feature -- Removal

	wipe_out
			-- Empty container.
		require
			not_empty: not empty
		ensure
			empty: empty
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	empty_definition: empty = (count = 0);
	full_definition: full = (count = capacity);

end -- class INDEXED_CONTAINER