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