indexing
	description: "Simple linear containers"
	author: "Patrick Schoenbach"
	access: cursor
	representation: linked
	contents: generic

deferred class interface
	LINEAR_CONTAINER [G]

feature -- Access

	i_th (i: INTEGER): G
			-- i-th item
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)

	index: INTEGER
			-- Current index
			-- (from SEQUENCIAL_CONTAINER)

	item: G
			-- Current item
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
	
feature -- Measurement

	capacity: INTEGER
			-- Size of container
			-- (from SEQUENCIAL_CONTAINER)

	count: INTEGER
			-- Number of elements
			-- (from SEQUENCIAL_CONTAINER)
	
feature -- Status report

	after: BOOLEAN
			-- Is there no valid cursor position to the right of cursor?
			-- (from SEQUENCIAL_CONTAINER)

	before: BOOLEAN
			-- Is there no valid cursor position to the left of cursor?
			-- (from SEQUENCIAL_CONTAINER)

	empty: BOOLEAN
			-- Is container empty?
			-- (from SEQUENCIAL_CONTAINER)

	full: BOOLEAN
			-- Is container full?
			-- (from SEQUENCIAL_CONTAINER)

	insertable: BOOLEAN
			-- Can elements be inserted in the middle?
			-- (from SEQUENCIAL_CONTAINER)

	isfirst: BOOLEAN
			-- Is cursor on first element?
			-- (from SEQUENCIAL_CONTAINER)

	islast: BOOLEAN
			-- Is cursor on last element?
			-- (from SEQUENCIAL_CONTAINER)

	off: BOOLEAN
			-- Is there no current item?
			-- (from SEQUENCIAL_CONTAINER)

	prunable: BOOLEAN
			-- Is container prunable?
			-- (from SEQUENCIAL_CONTAINER)

	resizable: BOOLEAN
			-- Is container resizable?
			-- (from SEQUENCIAL_CONTAINER)

	valid_index (i: INTEGER): BOOLEAN
			-- Is index i valid?
			-- (from SEQUENCIAL_CONTAINER)
	
feature -- Cursor movement

	forth
			-- Move cursor forwards.
		require -- from SEQUENCIAL_CONTAINER
			not_after: not after
		ensure then
			next_position: index = old index + 1

	go_i_th (i: INTEGER)
			-- Move cursor to the i-th position.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)
		ensure -- from SEQUENCIAL_CONTAINER
			i_th_position: index = i

	start
			-- Move cursor to first element.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from SEQUENCIAL_CONTAINER
			cursor_at_start: isfirst
	
feature -- Element change

	extend (v: G)
			-- Add v to the end of structure.
		require -- from SEQUENCIAL_CONTAINER
			not_full: not full
		ensure then
			extended: i_th (count) = v;
			count_increased: count = old count + 1;
			index_unchanged: not old empty implies index = old index

	put (v: G)
			-- Replace current item with v.
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
		ensure then
			replaced: item = v;
			count_unchanged: count = old count;
			index_unchanged: index = old index

	put_left (v: G)
			-- Insert v to the left of cursor.
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_before: not before
		ensure then
			inserted: i_th (index - 1) = v;
			count_increased: count = old count + 1;
			index_increased: index = old index + 1

	put_right (v: G)
			-- Insert v to the right of cursor.
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_after: not after
		ensure then
			inserted: i_th (index + 1) = v;
			count_increased: count = old count + 1;
			index_unchanged: index = old index
	
feature -- Removal

	remove
			-- Remove current item.
		require -- from SEQUENCIAL_CONTAINER
			prunable: prunable;
			not_empty: not empty;
			not_off: not off
		ensure then
			count_decreased: count = old count - 1;
			index_unchanged: not off implies index = old index

	wipe_out
			-- Empty container.
			-- (from SEQUENCIAL_CONTAINER)
		ensure -- from SEQUENCIAL_CONTAINER
			empty: empty
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize container to n elements.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			resizable: resizable;
			size_increasing: n > capacity
		ensure -- from SEQUENCIAL_CONTAINER
			resized: capacity = n
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	after_definition: after = (index = count + 1);
	before_definition: before = (index = 0);
	isfirst_definition: isfirst = (not empty and then (index = 1));
	islast_definition: islast = (not empty and then (index = count));
		-- from SEQUENCIAL_CONTAINER
	empty_definition: empty = (count = 0);
	off_definition: off = (before or after);
	empty_constraint: empty implies off;
	count_range: 0 <= count and count <= capacity;

end -- class LINEAR_CONTAINER