indexing
description: "Command history implemented as arrayed circular buffers"
representation: array
access: cursor
size: fixed
author: "Patrick Schoenbach"
class interface
ARRAYED_HISTORY [G -> COMMAND_HISTORY_ENTRY]
create
make (n: INTEGER)
require
number_of_elements_positive: n > 0
feature -- Access
after_index: INTEGER
-- Index of after sentinel
-- (from ARRAYED_CIRCULAR_BUFFER)
before_index: INTEGER
-- Index of before sentinel
-- (from ARRAYED_CIRCULAR_BUFFER)
first: INTEGER
-- Index of first item
-- (from ARRAYED_CIRCULAR_BUFFER)
i_th (i: INTEGER): like item
-- Item at index i
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- from SEQUENCIAL_CONTAINER
valid_index: valid_index (i)
index: INTEGER
-- Current item
-- (from ARRAYED_CIRCULAR_BUFFER)
item: G
-- Current item
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- from SEQUENCIAL_CONTAINER
not_off: not off
last: INTEGER
-- Index of last item
-- (from ARRAYED_CIRCULAR_BUFFER)
Sentinels: INTEGER is 2
-- (from ARRAYED_CIRCULAR_BUFFER)
infix "@" (i: INTEGER): G
-- i-th item
feature -- Measurement
capacity: INTEGER
-- Capacity of buffer
-- (from ARRAYED_CIRCULAR_BUFFER)
ensure then -- from ARRAYED_CIRCULAR_BUFFER
non_negative: Result >= 0
ensure then -- from ARRAYED_CIRCULAR_BUFFER
non_negative: Result >= 0
count: INTEGER
-- (from ARRAYED_CIRCULAR_BUFFER)
feature -- Status report
after: BOOLEAN
-- Is there no valid element to the right of the cursor?
-- (from ARRAYED_CIRCULAR_BUFFER)
before: BOOLEAN
-- Is there no valid element to the left of the cursor?
-- (from ARRAYED_CIRCULAR_BUFFER)
empty: BOOLEAN
-- Is buffer empty?
-- (from ARRAYED_CIRCULAR_BUFFER)
full: BOOLEAN
-- Is buffer entirely filled?
-- (from ARRAYED_CIRCULAR_BUFFER)
Insertable: BOOLEAN is false
-- Can elements be inserted in the middle? (Answer: No)
-- (from ARRAYED_CIRCULAR_BUFFER)
is_executed: BOOLEAN
-- Has current item been executed?
isfirst: BOOLEAN
-- Is cursor on first item?
-- (from ARRAYED_CIRCULAR_BUFFER)
islast: BOOLEAN
-- Is cursor on last item?
-- (from ARRAYED_CIRCULAR_BUFFER)
next (i: INTEGER): INTEGER
-- Index next to i
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- from CIRCULAR_CONTAINER
valid_index: valid_index (i)
off: BOOLEAN
-- Is there no current item?
-- (from ARRAYED_CIRCULAR_BUFFER)
previous (i: INTEGER): INTEGER
-- Index previous to i
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- from CIRCULAR_CONTAINER
valid_index: valid_index (i)
Prunable: BOOLEAN is true
-- Is container prunable? (Answer: Yes)
-- (from ARRAYED_CIRCULAR_BUFFER)
redoable_item: BOOLEAN
-- Is there a redoable item?
Resizable: BOOLEAN is true
-- Is container resizable? (Answer: yes)
-- (from ARRAYED_CIRCULAR_BUFFER)
undoable_item: BOOLEAN
-- Is there an undoable item?
valid_index (i: INTEGER): BOOLEAN
-- Is index i valid?
-- (from ARRAYED_CIRCULAR_BUFFER)
feature -- Cursor movement
back
-- Move cursor to previous item.
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- CIRCULAR_CONTAINER
precursor: True
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.
-- (from ARRAYED_CIRCULAR_BUFFER)
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.
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- CIRCULAR_CONTAINER
precursor: True
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.
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- from SEQUENCIAL_CONTAINER
valid_index: valid_index (i)
ensure -- from SEQUENCIAL_CONTAINER
i_th_position: index = i
start
-- Move cursor to first item.
-- (from ARRAYED_CIRCULAR_BUFFER)
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.
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- CIRCULAR_CONTAINER
precursor: True
require else -- from ARRAYED_CIRCULAR_BUFFER
always_extendable: full or not full
require -- from SEQUENCIAL_CONTAINER
not_full: not full
require else -- from ARRAYED_CIRCULAR_BUFFER
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 -- from ARRAYED_CIRCULAR_BUFFER
cursor_advanced: not old full implies index = next (old index)
ensure then -- from ARRAYED_CIRCULAR_BUFFER
cursor_advanced: not old full implies index = next (old index)
put (v: like item)
-- Replace current item with v,
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- CIRCULAR_CONTAINER
precursor: True
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.
-- (from ARRAYED_CIRCULAR_BUFFER)
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.
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- from SEQUENCIAL_CONTAINER
insertable: insertable;
not_full: not full;
not_after: not after
feature -- Removal
remove
-- Remove last item.
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- CIRCULAR_CONTAINER
precursor: True
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.
-- (from ARRAYED_CIRCULAR_BUFFER)
ensure then -- from CIRCULAR_CONTAINER
capacity_unchanged: capacity = old capacity
ensure -- from SEQUENCIAL_CONTAINER
empty: empty
feature -- Resizing
resize (n: INTEGER)
-- Resize buffer.
-- (from ARRAYED_CIRCULAR_BUFFER)
require -- from SEQUENCIAL_CONTAINER
resizable: resizable;
size_increasing: n > capacity
ensure -- from SEQUENCIAL_CONTAINER
resized: capacity = n
feature -- Basic operations
redo
-- Redo current item.
undo
-- Undo current item.
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from HISTORY_CONTAINER
current_command_executed: not off implies item.is_executed;
-- 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;
-- from ARRAYED_CIRCULAR_BUFFER
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));
end -- class ARRAYED_HISTORY