indexing
description: "Lists implemented with bilinked cells"
library: "Gobo Eiffel Structure Library"
author: "Eric Bezault <ericb@gobo.demon.co.uk>"
copyright: "Copyright (c) 1997, Eric Bezault"
class interface
DS_BILINKED_LIST [G]
create
make
ensure -- from DS_LINKED_LIST
empty: is_empty
make_equal
ensure -- from DS_LINKED_LIST
empty: is_empty
make_from_linear (other: DS_LINEAR [G])
-- (from DS_LINKED_LIST)
require -- from DS_LINKED_LIST
other_not_void: other /= void
ensure -- from DS_LINKED_LIST
count_set: count = other.count
feature -- Access
first: G
-- First item in list
-- (from DS_LINKED_LIST)
require -- from DS_LINEAR
not_empty: not is_empty
require -- from DS_EXTENDIBLE
not_empty: not is_empty
ensure -- from DS_LINEAR
has_first: has (Result)
ensure then -- from DS_INDEXABLE
definition: Result = item (1)
item (i: INTEGER): G
-- Item at index i
-- Was declared in DS_LINKED_LIST as synonym of @ and item.
-- (from DS_LINKED_LIST)
require -- from DS_TABLE
valid_entry: valid_entry (k)
last: G
-- Last item in list
-- (from DS_LINKED_LIST)
require -- from DS_BILINEAR
not_empty: not is_empty
require -- from DS_INDEXABLE
not_empty: not is_empty
ensure -- from DS_BILINEAR
has_last: has (Result)
ensure -- from DS_INDEXABLE
definition: Result = item (count)
new_cursor: DS_BILINKED_LIST_CURSOR [G]
-- New cursor for traversal
ensure -- from DS_TRAVERSABLE
cursor_not_void: Result /= void;
valid_cursor: valid_cursor (Result)
searcher: DS_BILINKED_LIST_SEARCHER [G]
-- List searcher
infix "@" (i: INTEGER): G
-- Item at index i
-- Was declared in DS_LINKED_LIST as synonym of @ and item.
-- (from DS_LINKED_LIST)
require -- from DS_TABLE
valid_entry: valid_entry (k)
feature -- Measurement
count: INTEGER
-- Number of items in list
-- (from DS_LINKED_LIST)
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 -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is list equal to other?
-- (from DS_LINKED_LIST)
require -- from GENERAL
other_not_void: other /= void
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result
ensure then -- from DS_CONTAINER
same_count: Result implies count = other.count
feature -- Status report
extendible (nb: INTEGER): BOOLEAN
-- May list be extended with nb items?
-- (from DS_LINKED_LIST)
require -- from DS_EXTENDIBLE
positive_n: n >= 0
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 is_empty
is_empty: BOOLEAN
-- Is structure empty?
-- (from DS_CONTAINER)
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)
feature -- Element change
append (other: DS_LINEAR [G]; i: INTEGER)
-- Add items of other at i-th position.
-- Was declared in DS_LINKED_LIST as synonym of extend and append.
-- (from DS_LINKED_LIST)
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_first (other: DS_LINEAR [G])
-- Add items of other to beginning of list.
-- Was declared in DS_LINKED_LIST as synonym of extend_first and append_first.
-- (from DS_LINKED_LIST)
require -- from DS_EXTENDIBLE
other_not_void: other /= void
ensure -- from DS_EXTENDIBLE
new_count: count = old count + other.count
append_last (other: DS_LINEAR [G])
-- Add items of other to end of list.
-- Was declared in DS_LINKED_LIST as synonym of extend_last and append_last.
-- (from DS_LINKED_LIST)
require -- from DS_DYNAMIC
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
append_left (other: DS_LINEAR [G]; a_cursor: like new_cursor)
-- Add items of other to left of a_cursor position.
-- Was declared in DS_BILINKED_LIST as synonym of extend_left and append_left.
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.
-- Was declared in DS_LINKED_LIST as synonym of extend_right and append_right.
-- (from DS_LINKED_LIST)
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 (other: DS_LINEAR [G]; i: INTEGER)
-- Add items of other at i-th position.
-- Was declared in DS_LINKED_LIST as synonym of extend and append.
-- (from DS_LINKED_LIST)
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_first (other: DS_LINEAR [G])
-- Add items of other to beginning of list.
-- Was declared in DS_LINKED_LIST as synonym of extend_first and append_first.
-- (from DS_LINKED_LIST)
require -- from DS_EXTENDIBLE
other_not_void: other /= void;
extendible: extendible (other.count)
ensure -- from DS_EXTENDIBLE
new_count: count = old count + other.count
extend_last (other: DS_LINEAR [G])
-- Add items of other to end of list.
-- Was declared in DS_LINKED_LIST as synonym of extend_last and append_last.
-- (from DS_LINKED_LIST)
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)
ensure -- from DS_DYNAMIC
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.
-- Was declared in DS_BILINKED_LIST as synonym of extend_left and append_left.
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.
-- Was declared in DS_LINKED_LIST as synonym of extend_right and append_right.
-- (from DS_LINKED_LIST)
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.
-- Was declared in DS_LINKED_LIST as synonym of put and force.
-- (from DS_LINKED_LIST)
require -- from DS_TABLE
valid_key: valid_index (k)
ensure -- from DS_TABLE
valid_entry: valid_entry (k);
inserted: item (k) = v
ensure then -- from DS_INDEXABLE
one_more: count = old count + 1
force_first (v: G)
-- Add v to beginning of list.
-- Was declared in DS_LINKED_LIST as synonym of put_first and force_first.
-- (from DS_LINKED_LIST)
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
force_last (v: G)
-- Add v to end of list.
-- Was declared in DS_LINKED_LIST as synonym of put_last and force_last.
-- (from DS_LINKED_LIST)
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
force_left (v: G; a_cursor: like new_cursor)
-- Add v to left of a_cursor position.
-- Was declared in DS_BILINKED_LIST as synonym of put_left and force_left.
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.
-- Was declared in DS_LINKED_LIST as synonym of put_right and force_right.
-- (from DS_LINKED_LIST)
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; i: INTEGER)
-- Add v at i-th position.
-- Was declared in DS_LINKED_LIST as synonym of put and force.
-- (from DS_LINKED_LIST)
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: item (i) = v
put_first (v: G)
-- Add v to beginning of list.
-- Was declared in DS_LINKED_LIST as synonym of put_first and force_first.
-- (from DS_LINKED_LIST)
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
put_last (v: G)
-- Add v to end of list.
-- Was declared in DS_LINKED_LIST as synonym of put_last and force_last.
-- (from DS_LINKED_LIST)
require -- from DS_DYNAMIC
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
put_left (v: G; a_cursor: like new_cursor)
-- Add v to left of a_cursor position.
-- Was declared in DS_BILINKED_LIST as synonym of put_left and force_left.
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; a_cursor: like new_cursor)
-- Add v to right of a_cursor position.
-- Was declared in DS_LINKED_LIST as synonym of put_right and force_right.
-- (from DS_LINKED_LIST)
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; i: INTEGER)
-- Replace item at index i by v.
-- (from DS_LINKED_LIST)
require -- from DS_TABLE
valid_entry: valid_entry (k)
ensure -- from DS_TABLE
replaced: item (k) = v;
same_count: count = old count
feature -- Removal
delete (v: G)
-- Remove all occurrences of v.
-- (Use searcher's comparison criterion.)
ensure -- from DS_DYNAMIC
deleted: not has (v)
keep_first (n: INTEGER)
-- Keep n first items in list.
-- (from DS_LINKED_LIST)
require -- from DS_EXTENDIBLE
valid_n: 0 <= n and n <= count
ensure -- from DS_EXTENDIBLE
new_count: count = n
keep_last (n: INTEGER)
-- Keep n last items of list.
require -- from DS_DYNAMIC
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
prune (n: INTEGER; i: INTEGER)
-- Remove n items at and after i-th position.
-- (from DS_LINKED_LIST)
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_first (n: INTEGER)
-- Remove n first items from list.
-- (from DS_LINKED_LIST)
require -- from DS_EXTENDIBLE
valid_n: 0 <= n and n <= count
ensure -- from DS_EXTENDIBLE
new_count: count = old count - n
prune_last (n: INTEGER)
-- Remove n last items from list.
require -- from DS_DYNAMIC
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
prune_left (n: INTEGER; a_cursor: like new_cursor)
-- Remove n items to left of a_cursor position.
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_LINKED_LIST)
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 (i: INTEGER)
-- Remove item at i-th position.
-- (from DS_LINKED_LIST)
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.
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_first
-- Remove item at beginning of list.
-- (from DS_LINKED_LIST)
require -- from DS_EXTENDIBLE
not_empty: not is_empty
ensure -- from DS_EXTENDIBLE
one_less: count = old count - 1
remove_last
-- Remove item at end of list.
require -- from DS_DYNAMIC
not_empty: not is_empty
require -- from DS_INDEXABLE
not_empty: not is_empty
ensure -- from DS_DYNAMIC
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.
require -- from DS_DYNAMIC
not_empty: not is_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_LINKED_LIST)
require -- from DS_DYNAMIC
not_empty: not is_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 list.
-- (from DS_LINKED_LIST)
ensure -- from DS_CONTAINER
wipe_out: is_empty
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: item (k) = old item (l);
new_l: item (l) = old item (k)
feature -- Duplication
copy (other: like Current)
-- Copy other to list.
-- (from DS_LINKED_LIST)
require -- from GENERAL
other_not_void: other /= void;
type_identity: same_type (other)
ensure -- from GENERAL
is_equal: is_equal (other)
feature -- Setting
set_searcher (a_searcher: like 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: 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);
first_constraint: first_cell /= void implies first_cell.left = void;
-- from DS_CONTAINER
positive_count: count >= 0;
empty_definition: is_empty = (count = 0);
-- from DS_SEARCHABLE
searcher_not_void: searcher /= void;
end -- class DS_BILINKED_LIST