indexing
description: "Structures that can be traversed and modified through integer access"
library: "Gobo Eiffel Structure Library"
author: "Eric Bezault <ericb@gobo.demon.co.uk>"
copyright: "Copyright (c) 1997, Eric Bezault"
deferred class interface
DS_INDEXABLE [G]
feature -- Access
first: G
-- First item in structure
require -- from DS_EXTENDIBLE
not_empty: not is_empty
ensure then
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
require
not_empty: not is_empty
ensure
definition: Result = item (count)
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)
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
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_entry (i: INTEGER): BOOLEAN
-- Is there an item at index i?
ensure -- from DS_TABLE
valid_key: Result implies valid_index (k)
ensure then
definition: Result = (1 <= i and i <= count)
valid_index (i: INTEGER): BOOLEAN
-- Is i a valid index?
ensure then
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
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.
require
other_not_void: other /= void;
valid_index: valid_index (i)
ensure
new_count: count = old count + other.count
append_last (other: DS_LINEAR [G])
-- Add items of other to end of structure.
require
other_not_void: other /= void
ensure
new_count: count = old count + other.count
extend (other: DS_LINEAR [G]; i: INTEGER)
-- Add items of other at i-th position.
require
other_not_void: other /= void;
extendible: extendible (other.count);
valid_index: valid_index (i)
ensure
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)
ensure -- from DS_EXTENDIBLE
new_count: count = old count + other.count
extend_last (other: DS_LINEAR [G])
-- Add items of other to end of structure.
require
other_not_void: other /= void;
extendible: extendible (other.count)
ensure
new_count: count = old count + other.count
force (v: G; i: INTEGER)
-- Add v at i-th position.
require -- from DS_TABLE
valid_key: valid_index (k)
ensure -- from DS_TABLE
valid_entry: valid_entry (k);
inserted: item (k) = v
ensure then
one_more: count = old count + 1
force_first (v: G)
-- Add v to beginning of structure.
ensure -- from DS_EXTENDIBLE
one_more: count = old count + 1
ensure then
inserted: first = v
force_last (v: G)
-- Add v to end of structure.
ensure
one_more: count = old count + 1;
inserted: last = v
put (v: G; i: INTEGER)
-- Add v at i-th position.
require
extendible: extendible (1);
valid_index: valid_index (i)
ensure
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.
require -- from DS_EXTENDIBLE
extendible: extendible (1)
ensure -- from DS_EXTENDIBLE
one_more: count = old count + 1
ensure then
inserted: first = v
put_last (v: G)
-- Add v to end of structure.
require
extendible: extendible (1)
ensure
one_more: count = old count + 1;
inserted: last = v
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
keep_first (n: INTEGER)
-- Keep n items in structure.
-- (from DS_EXTENDIBLE)
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 in structure.
require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
prune (n: INTEGER; i: INTEGER)
-- Remove n items at and after i-th position.
require
valid_entry: valid_entry (i);
valid_n: 0 <= n and n <= count - i + 1
ensure
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
ensure -- from DS_EXTENDIBLE
new_count: count = old count - n
prune_last (n: INTEGER)
-- Remove n last items from structure.
require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
remove_first
-- Remove an item from structure.
-- (from DS_EXTENDIBLE)
require -- from DS_EXTENDIBLE
not_empty: not is_empty
ensure -- from DS_EXTENDIBLE
one_less: count = old count - 1
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_last
-- Remove last item from structure.
require
not_empty: not is_empty
ensure
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 -- 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);
end -- class DS_INDEXABLE