indexing
	description: "Circular buffers implemented as an arrayed list"
	author: "Patrick Schoenbach"
	comment: "Originally, this class was designed to use ARRAYED_CIRCULARof EiffelBase for the implementation. This class contains adesign error though (the postcondition %'moved_back%' in feature%'back%' is wrongly inherited from BILINEAR). ISE has beennotified about the problem. Until it is fixed, ARRAYED_LISThas been used for implementation and the original version ofthis class that depends on ARRAYED_CIRCULAR has been renamed to%'arrayed_circular_buffer.e.orig%'. As soon as the problem isfixed, the original version should be used instead of this one."

class interface
	ARRAYED_CIRCULAR_BUFFER [G]

create 

	make (n: INTEGER)
			-- Create buffer with n items.
		require
			size_positive: n > 0
		ensure
			capacity_set: capacity = n;
			filled: list.count = n + sentinels;
			on_first_item: index = 1

feature -- Initialization

	make (n: INTEGER)
			-- Create buffer with n items.
		require
			size_positive: n > 0
		ensure
			capacity_set: capacity = n;
			filled: list.count = n + sentinels;
			on_first_item: index = 1
	
feature -- Access

	after_index: INTEGER
			-- Index of after sentinel

	before_index: INTEGER
			-- Index of before sentinel

	first: INTEGER
			-- Index of first item

	i_th (i: INTEGER): like item
			-- Item at index i
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)

	index: INTEGER
			-- Current item

	item: G
			-- Current item
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off

	last: INTEGER
			-- Index of last item

	Sentinels: INTEGER is 2
	
feature -- Measurement

	capacity: INTEGER
			-- Capacity of buffer
		ensure then
			non_negative: Result >= 0

	count: INTEGER
	
feature -- Status report

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

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

	empty: BOOLEAN
			-- Is buffer empty?

	full: BOOLEAN
			-- Is buffer entirely filled?

	Insertable: BOOLEAN is false
			-- Can elements be inserted in the middle? (Answer: No)

	isfirst: BOOLEAN
			-- Is cursor on first item?

	islast: BOOLEAN
			-- Is cursor on last item?

	next (i: INTEGER): INTEGER
			-- Index next to i
		require -- from CIRCULAR_CONTAINER
			valid_index: valid_index (i)

	off: BOOLEAN
			-- Is there no current item?

	previous (i: INTEGER): INTEGER
			-- Index previous to i
		require -- from CIRCULAR_CONTAINER
			valid_index: valid_index (i)

	Prunable: BOOLEAN is true
			-- Is container prunable? (Answer: Yes)

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

	valid_index (i: INTEGER): BOOLEAN
			-- Is index i valid?
		ensure then
			valid_index_definition: Result = (1 <= i) and (i <= list.count)
	
feature -- Cursor movement

	back
			-- Move cursor to previous item.
		require -- from TWO_WAY_SEQUENCIAL_CONTAINER
			not_before: not before
		ensure then -- from CIRCULAR_CONTAINER
			previous_position: index = previous (old index)

	finish
			-- Move cursor to last item.
		require -- from TWO_WAY_SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from TWO_WAY_SEQUENCIAL_CONTAINER
			cursor_at_end: islast

	forth
			-- Move cursor to next item.
		require -- from SEQUENCIAL_CONTAINER
			not_after: not after
		ensure then -- from CIRCULAR_CONTAINER
			next_position: index = next (old index)

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

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

	extend (v: like item)
			-- Add v to the end of buffer.
			-- Remove all elements between cursor and end, if cursor not at
			-- end.
		require -- from SEQUENCIAL_CONTAINER
			not_full: not full
		require else
			always_extendable: full or not full
		ensure then -- from CIRCULAR_CONTAINER
			extended: i_th (last) = v;
			add_item_if_not_full: (old index = old last and not full) implies count = old count + 1;
			capacity_unchanged: capacity = old capacity
		ensure then
			cursor_advanced: not old full implies index = next (old index)

	put (v: like item)
			-- Replace current item with v,
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
		ensure then -- from CIRCULAR_CONTAINER
			capacity_unchanged: capacity = old capacity

	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

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

	remove
			-- Remove last item.
		require -- from SEQUENCIAL_CONTAINER
			prunable: prunable;
			not_empty: not empty;
			not_off: not off
		ensure then -- from CIRCULAR_CONTAINER
			count_decreased: count = old count - 1;
			cursor_unchanged: not old islast implies index = old index;
			capacity_unchanged: capacity = old capacity

	wipe_out
			-- Clear entire buffer.
		ensure -- from SEQUENCIAL_CONTAINER
			empty: empty
		ensure then -- from CIRCULAR_CONTAINER
			capacity_unchanged: capacity = old capacity
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize buffer.
		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);
	capacity_definition: capacity = list.count - sentinels;
	after_definition: after = not empty implies (index = after_index);
	after_index_constraint: not empty implies after_index = next (last);
	before_definition: after = not empty implies (index = before_index);
	before_index_constraint: not empty implies before_index = previous (first);
	after_sentinel_empty: not empty implies i_th (after_index) = void;
	before_sentinel_empty: not empty implies i_th (before_index) = void;
		-- from CIRCULAR_CONTAINER
	not_off_yields_existing_item: not off implies item /= void;
	empty_definition: empty = (count = 0);
	full_definition: full = (count = capacity);
	count_in_range: count >= 0 and count <= capacity;
	isfirst_definition: isfirst = (not empty and then (index = first));
	islast_definition: islast = (not empty and then (index = last));
		-- from TWO_WAY_SEQUENCIAL_CONTAINER
	off_definition: off = (before or after);
		-- 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 ARRAYED_CIRCULAR_BUFFER