indexing
	description: "Container with unidirectional sequencial access"
	names: sequencial, unidirectional
	access: cursor
	author: "Patrick Schoenbach"

deferred class interface
	SEQUENCIAL_CONTAINER [G]

feature -- Access

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

	index: INTEGER
			-- Current index

	item: G
			-- Current item
		require
			not_off: not off
	
feature -- Measurement

	capacity: INTEGER
			-- Size of container

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

	after: BOOLEAN
			-- Is there no valid cursor position to the right of cursor?

	before: BOOLEAN
			-- Is there no valid cursor position to the left of cursor?

	empty: BOOLEAN
			-- Is container empty?

	full: BOOLEAN
			-- Is container full?

	insertable: BOOLEAN
			-- Can elements be inserted in the middle?

	isfirst: BOOLEAN
			-- Is cursor on first element?

	islast: BOOLEAN
			-- Is cursor on last element?

	off: BOOLEAN
			-- Is there no current item?

	prunable: BOOLEAN
			-- Is container prunable?

	resizable: BOOLEAN
			-- Is container resizable?

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

	forth
			-- Move cursor forwards.
		require
			not_after: not after

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

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

	extend (v: G)
			-- Add v to the end of structure.
		require
			not_full: not full

	put (v: G)
			-- Replace current item with v.
		require
			not_off: not off

	put_left (v: G)
			-- Insert v to the right of cursor.
		require
			insertable: insertable;
			not_full: not full;
			not_before: not before

	put_right (v: G)
			-- Insert v to the right of cursor.
		require
			insertable: insertable;
			not_full: not full;
			not_after: not after
	
feature -- Removal

	remove
			-- Remove current item.
		require
			prunable: prunable;
			not_empty: not empty;
			not_off: not off

	wipe_out
			-- Empty container.
		ensure
			empty: empty
	
feature -- Resizing

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

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	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 SEQUENCIAL_CONTAINER