indexing
description: "List structures"
library: "Gobo Eiffel Structure Library"
author: "Eric Bezault <ericb@gobo.demon.co.uk>"
copyright: "Copyright (c) 1997, Eric Bezault"
deferred class interface
DS_LIST [G]
feature -- Access
first: G
-- First item in structure
-- (from DS_INDEXABLE)
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)
ensure then -- from DS_INDEXABLE
definition: Result = item (1)
item (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)
last: G
-- Last item in structure
-- (from DS_INDEXABLE)
require -- from DS_BILINEAR
not_empty: not is_empty
require -- from DS_INDEXABLE
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)
ensure -- from DS_INDEXABLE
definition: Result = item (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)
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
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 -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is current structure equal to other?
-- (from DS_CONTAINER)
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
ensure then -- from DS_CONTAINER
same_count: Result implies count = other.count
feature -- Status report
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
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_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_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
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: item (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; 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: item (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; 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; 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: item (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 (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_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_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 (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_first
-- Remove an item from structure.
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
not_empty: not is_empty
require -- from DS_EXTENDIBLE
not_empty: not is_empty
ensure -- from DS_EXTENDIBLE
one_less: count = old count - 1
ensure -- from DS_EXTENDIBLE
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 is_empty
require -- from DS_INDEXABLE
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
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 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_DYNAMIC)
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 structure.
-- (from DS_CONTAINER)
ensure -- from DS_CONTAINER
wipe_out: is_empty
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 -- 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);
-- from DS_CONTAINER
positive_count: count >= 0;
empty_definition: is_empty = (count = 0);
-- from DS_SEARCHABLE
searcher_not_void: searcher /= void;
end -- class DS_LIST