indexing
description: "Adapter for linked lists"
author: "Patrick Schoenbach"
deferred class interface
LIST_ADAPTER [G]
feature -- Access
first: G
-- First item in structure
-- (from DS_INDEXABLE)
require -- from DS_LINEAR
not_empty: not empty
require -- from DS_EXTENDIBLE
not_empty: not empty
ensure -- from DS_LINEAR
has_first: has (Result)
ensure then -- from DS_INDEXABLE
definition: Result = i_th (1)
ensure then -- from DS_INDEXABLE
definition: Result = i_th (1)
index: INTEGER
-- Current index
item: G
-- Current item
require -- from SEQUENCIAL_CONTAINER
not_off: not off
i_th (k: INTEGER): G
-- Item associated with k
-- Was declared in DS_TABLE as synonym of @ and item.
-- (from DS_TABLE)
require -- from SEQUENCIAL_CONTAINER
valid_index: valid_index (i)
require -- from DS_TABLE
valid_entry: valid_entry (k)
require -- from DS_TABLE
valid_entry: valid_entry (k)
last: G
-- Last item in structure
-- (from DS_INDEXABLE)
require -- from DS_BILINEAR
not_empty: not empty
require -- from DS_INDEXABLE
not_empty: not empty
require -- from DS_INDEXABLE
not_empty: not empty
ensure -- from DS_BILINEAR
has_last: has (Result)
ensure -- from DS_INDEXABLE
definition: Result = i_th (count)
ensure -- from DS_INDEXABLE
definition: Result = i_th (count)
new_cursor: DS_BILINEAR_CURSOR [G]
-- New cursor for traversal
-- (from DS_BILINEAR)
ensure -- from DS_TRAVERSABLE
cursor_not_void: Result /= void;
valid_cursor: valid_cursor (Result)
list_searcher: DS_BILINEAR_SEARCHER [G]
-- Structure searcher
-- (from DS_BILINEAR)
infix "@" (k: INTEGER): G
-- Item associated with k
-- Was declared in DS_TABLE as synonym of @ and item.
-- (from DS_TABLE)
require -- from DS_TABLE
valid_entry: valid_entry (k)
feature -- Measurement
capacity: INTEGER
-- Capacity of list
count: INTEGER
-- Number of items in structure
-- (from DS_CONTAINER)
occurrences (v: G): INTEGER
-- Number of times v appears in structure
-- (Use searcher's comparison criterion.)
-- (from DS_SEARCHABLE)
ensure -- from DS_SEARCHABLE
positive: Result >= 0;
has: has (v) implies Result >= 1
feature -- Status report
after: BOOLEAN
-- Is there no valid item to the left of cursor?
before: BOOLEAN
-- Is there no valid item to the right of cursor?
extendible (n: INTEGER): BOOLEAN
-- May structure be extended with n items?
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
positive_n: n >= 0
require -- from DS_EXTENDIBLE
positive_n: n >= 0
Full: BOOLEAN is false
-- Is container full? (Answer: no)
has (v: G): BOOLEAN
-- Does structure incluse v?
-- (Use searcher's comparison criterion.)
-- (from DS_SEARCHABLE)
ensure -- from DS_SEARCHABLE
not_empty: Result implies not empty
Insertable: BOOLEAN is true
-- Can items be inserted in the middle of container? (Answer: yes)
empty: BOOLEAN
-- Is structure empty?
-- (from DS_CONTAINER)
isfirst: BOOLEAN
-- Is cursor on first item?
islast: BOOLEAN
-- Is cursor on last item?
off: BOOLEAN
-- Is cursor off the list?
Prunable: BOOLEAN is true
-- Can items be removed from container? (Answer: yes)
Resizable: BOOLEAN is false
-- Can container be resized? (Answer: no)
sorted (sorter: DS_SORTER [G]): BOOLEAN
-- Is structure sorted according to sorter's criterion?
-- (from DS_SORTABLE)
require -- from DS_SORTABLE
sorter_not_void: sorter /= void
valid_cursor (a_cursor: like new_cursor): BOOLEAN
-- Is a_cursor a valid cursor?
-- (A cursor might become invalid if structure
-- has been modified during traversal.)
-- (from DS_TRAVERSABLE)
require -- from DS_TRAVERSABLE
a_cursor_not_void: a_cursor /= void
ensure -- from DS_TRAVERSABLE
is_valid: Result implies a_cursor.is_valid
valid_entry (i: INTEGER): BOOLEAN
-- Is there an item at index i?
-- (from DS_INDEXABLE)
ensure -- from DS_TABLE
valid_key: Result implies valid_index (k)
ensure then -- from DS_INDEXABLE
definition: Result = (1 <= i and i <= count)
valid_index (i: INTEGER): BOOLEAN
-- Is i a valid index?
-- (from DS_INDEXABLE)
ensure then -- from DS_INDEXABLE
definition: Result = (1 <= i and i <= count + 1)
ensure then -- from DS_INDEXABLE
definition: Result = (1 <= i and i <= count + 1)
feature -- Cursor movement
finish
-- Move cursor to last item.
forth
-- Move cursor forwards.
require -- from SEQUENCIAL_CONTAINER
not_after: not after
ensure then -- from LINEAR_CONTAINER
next_position: index = old index + 1
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
append_first (other: DS_LINEAR [G])
-- Add items of other to structure.
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
other_not_void: other /= void
require -- from DS_EXTENDIBLE
other_not_void: other /= void
ensure -- from DS_EXTENDIBLE
new_count: count = old count + other.count
ensure -- from DS_EXTENDIBLE
new_count: count = old count + other.count
append (other: DS_LINEAR [G]; i: INTEGER)
-- Add items of other at i-th position.
-- (from DS_INDEXABLE)
require -- from DS_INDEXABLE
other_not_void: other /= void;
valid_index: valid_index (i)
ensure -- from DS_INDEXABLE
new_count: count = old count + other.count
append_last (other: DS_LINEAR [G])
-- Add items of other to end of structure.
-- (from DS_INDEXABLE)
require -- from DS_DYNAMIC
other_not_void: other /= void
require -- from DS_INDEXABLE
other_not_void: other /= void
require -- from DS_INDEXABLE
other_not_void: other /= void
ensure -- from DS_DYNAMIC
new_count: count = old count + other.count
ensure -- from DS_INDEXABLE
new_count: count = old count + other.count
ensure -- from DS_INDEXABLE
new_count: count = old count + other.count
append_left (other: DS_LINEAR [G]; a_cursor: like new_cursor)
-- Add items of other to left of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
other_not_void: other /= void;
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_before: not a_cursor.before
ensure -- from DS_DYNAMIC
new_count: count = old count + other.count
append_right (other: DS_LINEAR [G]; a_cursor: like new_cursor)
-- Add items of other to right of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
other_not_void: other /= void;
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_after: not a_cursor.after
ensure -- from DS_DYNAMIC
new_count: count = old count + other.count
extend (v: G)
-- Add v to end of container.
require -- from SEQUENCIAL_CONTAINER
not_full: not full
ensure then -- from LINEAR_CONTAINER
extended: i_th (count) = v;
count_increased: count = old count + 1;
index_unchanged: not old empty implies index = old index
extend_first (other: DS_LINEAR [G])
-- Add items of other to structure.
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
other_not_void: other /= void;
extendible: extendible (other.count)
require -- from DS_EXTENDIBLE
other_not_void: other /= void;
extendible: extendible (other.count)
ensure -- from DS_EXTENDIBLE
new_count: count = old count + other.count
ensure -- from DS_EXTENDIBLE
new_count: count = old count + other.count
list_extend (other: DS_LINEAR [G]; i: INTEGER)
-- Add items of other at i-th position.
-- (from DS_INDEXABLE)
require -- from DS_INDEXABLE
other_not_void: other /= void;
extendible: extendible (other.count);
valid_index: valid_index (i)
ensure -- from DS_INDEXABLE
new_count: count = old count + other.count
extend_last (other: DS_LINEAR [G])
-- Add items of other to end of structure.
-- (from DS_INDEXABLE)
require -- from DS_DYNAMIC
other_not_void: other /= void;
extendible: extendible (other.count)
require -- from DS_INDEXABLE
other_not_void: other /= void;
extendible: extendible (other.count)
require -- from DS_INDEXABLE
other_not_void: other /= void;
extendible: extendible (other.count)
ensure -- from DS_DYNAMIC
new_count: count = old count + other.count
ensure -- from DS_INDEXABLE
new_count: count = old count + other.count
ensure -- from DS_INDEXABLE
new_count: count = old count + other.count
extend_left (other: DS_LINEAR [G]; a_cursor: like new_cursor)
-- Add items of other to left of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
other_not_void: other /= void;
extendible: extendible (other.count);
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_before: not a_cursor.before
ensure -- from DS_DYNAMIC
new_count: count = old count + other.count
extend_right (other: DS_LINEAR [G]; a_cursor: like new_cursor)
-- Add items of other to right of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
other_not_void: other /= void;
extendible: extendible (other.count);
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_after: not a_cursor.after
ensure -- from DS_DYNAMIC
new_count: count = old count + other.count
force (v: G; i: INTEGER)
-- Add v at i-th position.
-- (from DS_INDEXABLE)
require -- from DS_TABLE
valid_key: valid_index (k)
ensure -- from DS_TABLE
valid_entry: valid_entry (k);
inserted: i_th (k) = v
ensure then -- from DS_INDEXABLE
one_more: count = old count + 1
force_first (v: G)
-- Add v to beginning of structure.
-- (from DS_INDEXABLE)
ensure then -- from DS_DYNAMIC
inserted: first = v
ensure -- from DS_EXTENDIBLE
one_more: count = old count + 1
ensure then -- from DS_INDEXABLE
inserted: first = v
ensure then -- from DS_INDEXABLE
inserted: first = v
force_last (v: G)
-- Add v to end of structure.
-- (from DS_INDEXABLE)
ensure -- from DS_DYNAMIC
one_more: count = old count + 1;
inserted: last = v
ensure -- from DS_INDEXABLE
one_more: count = old count + 1;
inserted: last = v
ensure -- from DS_INDEXABLE
one_more: count = old count + 1;
inserted: last = v
force_left (v: G; a_cursor: like new_cursor)
-- Add v to left of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_before: not a_cursor.before
ensure -- from DS_DYNAMIC
one_more: count = old count + 1
force_right (v: G; a_cursor: like new_cursor)
-- Add v to right of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_after: not a_cursor.after
ensure -- from DS_DYNAMIC
one_more: count = old count + 1
put (v: G)
-- Replace current item with v.
require -- from SEQUENCIAL_CONTAINER
not_off: not off
ensure then -- from LINEAR_CONTAINER
replaced: item = v;
count_unchanged: count = old count;
index_unchanged: index = old index
list_put (v: G; i: INTEGER)
-- Add v at i-th position.
-- (from DS_INDEXABLE)
require -- from DS_INDEXABLE
extendible: extendible (1);
valid_index: valid_index (i)
ensure -- from DS_INDEXABLE
one_more: count = old count + 1;
valid_entry: valid_entry (i);
inserted: i_th (i) = v
put_first (v: G)
-- Add v to beginning of structure.
-- (from DS_INDEXABLE)
require -- DS_DYNAMIC
precursor: True
require -- from DS_EXTENDIBLE
extendible: extendible (1)
ensure then -- from DS_DYNAMIC
inserted: first = v
ensure -- from DS_EXTENDIBLE
one_more: count = old count + 1
ensure then -- from DS_INDEXABLE
inserted: first = v
ensure then -- from DS_INDEXABLE
inserted: first = v
put_last (v: G)
-- Add v to end of structure.
-- (from DS_INDEXABLE)
require -- from DS_DYNAMIC
extendible: extendible (1)
require -- from DS_INDEXABLE
extendible: extendible (1)
require -- from DS_INDEXABLE
extendible: extendible (1)
ensure -- from DS_DYNAMIC
one_more: count = old count + 1;
inserted: last = v
ensure -- from DS_INDEXABLE
one_more: count = old count + 1;
inserted: last = v
ensure -- from DS_INDEXABLE
one_more: count = old count + 1;
inserted: last = v
put_left (v: G)
-- Insert v to the left of current position.
require -- from SEQUENCIAL_CONTAINER
insertable: insertable;
not_full: not full;
not_before: not before
ensure then -- from LINEAR_CONTAINER
inserted: i_th (index - 1) = v;
count_increased: count = old count + 1;
index_increased: index = old index + 1
list_put_left (v: G; a_cursor: like new_cursor)
-- Add v to left of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
extendible: extendible (1);
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_before: not a_cursor.before
ensure -- from DS_DYNAMIC
one_more: count = old count + 1
put_right (v: G)
-- Insert v to the right of current position.
require -- from SEQUENCIAL_CONTAINER
insertable: insertable;
not_full: not full;
not_after: not after
ensure then -- from LINEAR_CONTAINER
inserted: i_th (index + 1) = v;
count_increased: count = old count + 1;
index_unchanged: index = old index
list_put_right (v: G; a_cursor: like new_cursor)
-- Add v to right of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
extendible: extendible (1);
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_after: not a_cursor.after
ensure -- from DS_DYNAMIC
one_more: count = old count + 1
replace (v: G; k: INTEGER)
-- Replace item associated with k by v.
-- (from DS_TABLE)
require -- from DS_TABLE
valid_entry: valid_entry (k)
ensure -- from DS_TABLE
replaced: i_th (k) = v;
same_count: count = old count
feature -- Removal
delete (v: G)
-- Remove all occurrences of v.
-- (Use searcher's comparison criterion.)
-- (from DS_DYNAMIC)
ensure -- from DS_DYNAMIC
deleted: not has (v)
keep_first (n: INTEGER)
-- Keep n items in structure.
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
valid_n: 0 <= n and n <= count
require -- from DS_EXTENDIBLE
valid_n: 0 <= n and n <= count
ensure -- from DS_EXTENDIBLE
new_count: count = n
ensure -- from DS_EXTENDIBLE
new_count: count = n
keep_last (n: INTEGER)
-- Keep n last items in structure.
-- (from DS_INDEXABLE)
require -- from DS_DYNAMIC
valid_n: 0 <= n and n <= count
require -- from DS_INDEXABLE
valid_n: 0 <= n and n <= count
require -- from DS_INDEXABLE
valid_n: 0 <= n and n <= count
ensure -- from DS_DYNAMIC
new_count: count = n
ensure -- from DS_INDEXABLE
new_count: count = n
ensure -- from DS_INDEXABLE
new_count: count = n
prune_first (n: INTEGER)
-- Remove n items from structure.
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
valid_n: 0 <= n and n <= count
require -- from DS_EXTENDIBLE
valid_n: 0 <= n and n <= count
ensure -- from DS_EXTENDIBLE
new_count: count = old count - n
ensure -- from DS_EXTENDIBLE
new_count: count = old count - n
prune (n: INTEGER; i: INTEGER)
-- Remove n items at and after i-th position.
-- (from DS_INDEXABLE)
require -- from DS_INDEXABLE
valid_entry: valid_entry (i);
valid_n: 0 <= n and n <= count - i + 1
ensure -- from DS_INDEXABLE
new_count: count = old count - n
prune_last (n: INTEGER)
-- Remove n last items from structure.
-- (from DS_INDEXABLE)
require -- from DS_DYNAMIC
valid_n: 0 <= n and n <= count
require -- from DS_INDEXABLE
valid_n: 0 <= n and n <= count
require -- from DS_INDEXABLE
valid_n: 0 <= n and n <= count
ensure -- from DS_DYNAMIC
new_count: count = old count - n
ensure -- from DS_INDEXABLE
new_count: count = old count - n
ensure -- from DS_INDEXABLE
new_count: count = old count - n
prune_left (n: INTEGER; a_cursor: like new_cursor)
-- Remove n items to left of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
valid_n: 0 <= n and n < a_cursor.index
ensure -- from DS_DYNAMIC
new_count: count = old count - n
prune_right (n: INTEGER; a_cursor: like new_cursor)
-- Remove n items to right of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
valid_n: 0 <= n and n <= count - a_cursor.index
ensure -- from DS_DYNAMIC
new_count: count = old count - n
remove
-- Remove current item.
require -- from SEQUENCIAL_CONTAINER
prunable: prunable;
not_empty: not empty;
not_off: not off
ensure then -- from LINEAR_CONTAINER
count_decreased: count = old count - 1;
index_unchanged: not off implies index = old index
remove_first
-- Remove an item from structure.
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
not_empty: not empty
require -- from DS_EXTENDIBLE
not_empty: not empty
ensure -- from DS_EXTENDIBLE
one_less: count = old count - 1
ensure -- from DS_EXTENDIBLE
one_less: count = old count - 1
list_remove (k: INTEGER)
-- Remove item associated with k.
-- (from DS_TABLE)
require -- from DS_TABLE
valid_entry: valid_entry (k)
ensure -- from DS_TABLE
one_less: count = old count - 1
remove_at (a_cursor: like new_cursor)
-- Remove item at a_cursor position.
-- Move a_cursor to next position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_off: not a_cursor.off
ensure -- from DS_DYNAMIC
one_less: count = old count - 1
remove_last
-- Remove last item from structure.
-- (from DS_INDEXABLE)
require -- from DS_DYNAMIC
not_empty: not empty
require -- from DS_INDEXABLE
not_empty: not empty
require -- from DS_INDEXABLE
not_empty: not empty
ensure -- from DS_DYNAMIC
one_less: count = old count - 1
ensure -- from DS_INDEXABLE
one_less: count = old count - 1
ensure -- from DS_INDEXABLE
one_less: count = old count - 1
remove_left (a_cursor: like new_cursor)
-- Remove item to left of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
not_empty: not empty;
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_before: not a_cursor.before;
not_first: not a_cursor.is_first
ensure -- from DS_DYNAMIC
one_less: count = old count - 1
remove_right (a_cursor: like new_cursor)
-- Remove item to right of a_cursor position.
-- (from DS_DYNAMIC)
require -- from DS_DYNAMIC
not_empty: not empty;
cursor_not_void: a_cursor /= void;
valid_cursor: valid_cursor (a_cursor);
not_before: not a_cursor.after;
not_first: not a_cursor.is_last
ensure -- from DS_DYNAMIC
one_less: count = old count - 1
wipe_out
-- Remove all items from structure.
-- (from DS_CONTAINER)
ensure -- from SEQUENCIAL_CONTAINER
empty: empty
ensure -- from DS_CONTAINER
wipe_out: empty
ensure -- from DS_CONTAINER
wipe_out: empty
feature -- Resizing
resize (n: INTEGER)
-- Resize history to n items.
require -- from SEQUENCIAL_CONTAINER
resizable: resizable;
size_increasing: n > capacity
ensure -- from SEQUENCIAL_CONTAINER
resized: capacity = n
feature -- Transformation
swap (k, l: INTEGER)
-- Exchange items associated with k and l.
-- (from DS_TABLE)
require -- from DS_TABLE
valid_k: valid_entry (k);
valid_l: valid_entry (l)
ensure -- from DS_TABLE
same_count: count = old count;
new_k: i_th (k) = old i_th (l);
new_l: i_th (l) = old i_th (k)
feature -- Setting
set_searcher (a_searcher: like list_searcher)
-- Set searcher to a_searcher.
-- (from DS_SEARCHABLE)
require -- from DS_SEARCHABLE
a_searcher_not_void: a_searcher /= void
ensure -- from DS_SEARCHABLE
searcher_set: list_searcher = a_searcher
feature -- Sort
sort (sorter: DS_SORTER [G])
-- Sort structure using sorter's algorithm.
-- (from DS_SORTABLE)
require -- from DS_SORTABLE
sorter_not_void: sorter /= void
ensure -- from DS_SORTABLE
sorted: sorted (sorter)
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from LINEAR_CONTAINER
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;
-- from DS_CONTAINER
positive_count: count >= 0;
empty_definition: empty = (count = 0);
-- from DS_SEARCHABLE
searcher_not_void: list_searcher /= void;
end -- class LIST_ADAPTER