Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

structure.table

Class DS_MULTIARRAYED_HASH_TABLE


Direct ancestors

DS_MULTIARRAYED_SPARSE_TABLE

Creation

Features

Invariants

indexing

description

Hash tables implemented with multi-arrays. %
%Keys are hashed using hash_code from HASHABLE.

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 17:54:24 $

revision

$Revision: 1.6 $

class

DS_MULTIARRAYED_HASH_TABLE [G, K -> HASHABLE]

inherit

DS_MULTIARRAYED_SPARSE_TABLE

create

make (n: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of default_chunk_size.
-- Use = as comparison criterion for items.
-- Use equal as comparison criterion for keys.

-- (From DS_SPARSE_TABLE)

require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
before: before
ensure then
chunk_size_set: chunk_size = default_chunk_size
make_equal (n: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of default_chunk_size.
-- Use equal as comparison criterion for items.
-- Use equal as comparison criterion for keys.

-- (From DS_SPARSE_TABLE)

require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
before: before
ensure then
chunk_size_set: chunk_size = default_chunk_size
make_default

-- Create an empty table and allocate memory space
-- for at least default_capacity items. Array
-- chunks will have a size of default_chunk_size.
-- Use = as comparison criterion for items.
-- Use equal as comparison criterion for keys.

-- (From DS_CONTAINER)

ensure
empty: is_empty
ensure then
before: before
ensure then
chunk_size_set: chunk_size = default_chunk_size
make_with_chunk_size (n: INTEGER; a_chunk_size: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of a_chunk_size.
-- Use = as comparison criterion for items.
-- Use equal as comparison criterion for keys.

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

require
positive_n: n >= 0
a_chunk_size_positive: a_chunk_size > 0
ensure
empty: is_empty
capacity_set: capacity = n
chunk_size_set: chunk_size = a_chunk_size
before: before
make_equal_with_chunk_size (n: INTEGER; a_chunk_size: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of a_chunk_size.
-- Use equal as comparison criterion for items.
-- Use equal as comparison criterion for keys.

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

require
positive_n: n >= 0
a_chunk_size_positive: a_chunk_size > 0
ensure
empty: is_empty
capacity_set: capacity = n
chunk_size_set: chunk_size = a_chunk_size
before: before
make_map (n: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of default_chunk_size.
-- Use = as comparison criterion for items.
-- Use = as comparison criterion for keys.

-- (From DS_SPARSE_TABLE)

require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
before: before
ensure then
chunk_size_set: chunk_size = default_chunk_size
make_map_equal (n: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of default_chunk_size.
-- Use equal as comparison criterion for items.
-- Use = as comparison criterion for keys.

-- (From DS_SPARSE_TABLE)

require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
before: before
ensure then
chunk_size_set: chunk_size = default_chunk_size
make_map_default

-- Create an empty table and allocate memory space
-- for at least default_capacity items. Array
-- chunks will have a size of default_chunk_size.
-- Use = as comparison criterion for items.
-- Use = as comparison criterion for keys.

-- (From DS_SPARSE_TABLE)

ensure
empty: is_empty
capacity_set: capacity = default_capacity
before: before
ensure then
chunk_size_set: chunk_size = default_chunk_size
make_map_with_chunk_size (n: INTEGER; a_chunk_size: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of a_chunk_size.
-- Use = as comparison criterion for items.
-- Use = as comparison criterion for keys.

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

require
positive_n: n >= 0
a_chunk_size_positive: a_chunk_size > 0
ensure
empty: is_empty
capacity_set: capacity = n
chunk_size_set: chunk_size = a_chunk_size
before: before
make_map_equal_with_chunk_size (n: INTEGER; a_chunk_size: INTEGER)

-- Create an empty table and allocate memory space
-- for at least n items. Array chunks will have
-- a size of a_chunk_size.
-- Use equal as comparison criterion for items.
-- Use = as comparison criterion for keys.

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

require
positive_n: n >= 0
a_chunk_size_positive: a_chunk_size > 0
ensure
empty: is_empty
capacity_set: capacity = n
chunk_size_set: chunk_size = a_chunk_size
before: before
make_with_equality_testers (n: INTEGER;an_item_tester: like equality_tester;a_key_tester: like key_equality_tester)

-- Create an empty table and allocate memory space for at
-- least n items. Array chunks will have a size of
-- default_chunk_size.
-- Use an_item_tester as comparison criterion for items.
-- Use a_key_tester as comparison criterion for keys.

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
chunk_size_set: chunk_size = default_chunk_size
before: before
equality_tester_set: equality_tester = an_item_tester
key_equality_tester_set: key_equality_tester = a_key_tester
make_with_chunk_size_and_equality_testers (n: INTEGER;a_chunk_size: INTEGER; an_item_tester: like equality_tester;a_key_tester: like key_equality_tester)

-- Create an empty table and allocate memory space for at
-- least n items. Array chunks will have a size of a_chunk_size.
-- Use an_item_tester as comparison criterion for items.
-- Use a_key_tester as comparison criterion for keys.

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

require
positive_n: n >= 0
a_chunk_size_positive: a_chunk_size > 0
ensure
empty: is_empty
capacity_set: capacity = n
chunk_size_set: chunk_size = a_chunk_size
before: before
equality_tester_set: equality_tester = an_item_tester
key_equality_tester_set: key_equality_tester = a_key_tester

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
any_array_: KL_ARRAY_ROUTINES [ANY]

-- Routines that ought to be in class ARRAY

-- (From KL_IMPORTED_ARRAY_ROUTINES)

ensure
any_array_routines_not_void: Result /= Void
array_special_integer_: KL_ARRAY_ROUTINES [SPECIAL [INTEGER]]

-- Routines that ought to be in class ARRAY

-- (From KL_IMPORTED_ARRAY_ROUTINES)

ensure
special_integer_array_routines_not_void: Result /= Void
boolean_array_: KL_ARRAY_ROUTINES [BOOLEAN]

-- Routines that ought to be in class ARRAY

-- (From KL_IMPORTED_ARRAY_ROUTINES)

ensure
boolean_array_routines_not_void: Result /= Void
integer_array_: KL_ARRAY_ROUTINES [INTEGER]

-- Routines that ought to be in class ARRAY

-- (From KL_IMPORTED_ARRAY_ROUTINES)

ensure
integer_array_routines_not_void: Result /= Void
special_any_: KL_SPECIAL_ROUTINES [ANY]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_any_routines_not_void: Result /= Void
special_boolean_: KL_SPECIAL_ROUTINES [BOOLEAN]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_boolean_routines_not_void: Result /= Void
special_character_: KL_SPECIAL_ROUTINES [CHARACTER]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_character_routines_not_void: Result /= Void
special_integer_: KL_SPECIAL_ROUTINES [INTEGER]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_integer_routines_not_void: Result /= Void
special_string_: KL_SPECIAL_ROUTINES [STRING]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_string_routines_not_void: Result /= Void
string_array_: KL_ARRAY_ROUTINES [STRING]

-- Routines that ought to be in class ARRAY

-- (From KL_IMPORTED_ARRAY_ROUTINES)

ensure
string_array_routines_not_void: Result /= Void
equality_tester: KL_EQUALITY_TESTER [G]

-- Equality tester;
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

first: G

-- First item in container

-- (From DS_LINEAR)

require
not_empty: not is_empty
ensure
has_first: has (Result)
found_item: G

-- Item found by last call to search

-- (From DS_SPARSE_CONTAINER)

require
item_found: found
found_key: K

-- Key of item found by last call to search

-- (From DS_SPARSE_TABLE)

require
key_found: found
infix "@" (k: K): G

-- Item associated with k

-- (From DS_TABLE)

require
has_k: has (k)
item (k: K): G

-- Item associated with k

-- (From DS_TABLE)

require
has_k: has (k)
item_for_iteration: G

-- Item at internal cursor position

-- (From DS_TRAVERSABLE)

require
not_off: not off
key (k: K): K

-- Key associated with k

-- (From DS_SPARSE_TABLE)

require
has_k: has (k)
key_equality_tester: KL_EQUALITY_TESTER [K]

-- Equality tester for keys;
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SPARSE_CONTAINER)

key_for_iteration: K

-- Key at internal cursor position

-- (From DS_SPARSE_TABLE)

require
not_off: not off
last: G

-- Last item in container

-- (From DS_BILINEAR)

require
not_empty: not is_empty
ensure
has_last: has (Result)
new_cursor: DS_MULTIARRAYED_HASH_TABLE_CURSOR [G, K]

-- New external cursor for traversal

-- (From DS_TRAVERSABLE)

ensure
cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)
value (k: K): G

-- Item associated with k;
-- Return default value if no such item

-- (From KL_VALUES)

require
k_not_void: k /= Void
require else
True

feature -- Measurement

capacity: INTEGER

-- Maximum number of items in container

-- (From DS_RESIZABLE)

chunk_size: INTEGER

-- Size of array chunks

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

count: INTEGER

-- Number of items in container

-- (From DS_CONTAINER)

default_capacity: INTEGER

-- Initial capacity in make_default
-- (Default value: 10)

-- (From DS_RESIZABLE)

ensure
default_capacity_positive: Result >= 0
default_chunk_size: INTEGER

-- Default value for chunk_size
-- (Default value: 30000)

-- (From DS_MULTIARRAYED_SPARSE_TABLE)

ensure
default_chunk_size_positive: Result > 0
occurrences (v: G): INTEGER

-- Number of times v appears in container
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
positive: Result >= 0
has: has (v) implies Result >= 1

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is table equal to other?
-- Do not take cursor positions, capacity
-- nor equality_tester into account.

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

after: BOOLEAN

-- Is there no valid position to right of internal cursor?

-- (From DS_LINEAR)

before: BOOLEAN

-- Is there no valid position to left of internal cursor?

-- (From DS_BILINEAR)

equality_tester_settable (a_tester: like equality_tester): BOOLEAN

-- Can set_equality_tester be called with a_tester
-- as argument in current state of container?
-- (Default answer: True.)

-- (From DS_SEARCHABLE)

found: BOOLEAN

-- Did last call to search succeed?

-- (From DS_SPARSE_CONTAINER)

ensure
definition: Result = (found_position /= No_position)
has (k: K): BOOLEAN

-- Is there an item associated with k?

-- (From DS_TABLE)

ensure
valid_key: Result implies valid_key (k)
has_item (v: G): BOOLEAN

-- Does container include v?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
not_empty: Result implies not is_empty
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_first: BOOLEAN

-- Is internal cursor on first item?

-- (From DS_LINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = first)
is_full: BOOLEAN

-- Is container full?

-- (From DS_RESIZABLE)

is_last: BOOLEAN

-- Is internal cursor on last item?

-- (From DS_BILINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = last)
key_equality_tester_settable (a_tester: like key_equality_tester): BOOLEAN

-- Can set_key_equality_tester be called with a_tester
-- as argument in current state of container?

-- (From DS_SPARSE_TABLE)

off: BOOLEAN

-- Is there no item at internal cursor position?

-- (From DS_TRAVERSABLE)

same_equality_tester (other: DS_SEARCHABLE [G]): BOOLEAN

-- Does container use the same comparison
-- criterion as other?

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: G): BOOLEAN

-- Are v and u considered equal?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

same_position (a_cursor: like new_cursor): BOOLEAN

-- Is internal cursor at same position as a_cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
valid_cursor (a_cursor: DS_CURSOR [G]): BOOLEAN

-- Is a_cursor a valid cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
valid_key (k: K): BOOLEAN

-- Is k a valid key?

-- (From DS_TABLE)

ensure then
defintion: Result = True

feature -- Cursor movement

back

-- Move internal cursor to previous position.

-- (From DS_BILINEAR)

require
not_before: not before
finish

-- Move internal cursor to last position.

-- (From DS_BILINEAR)

ensure
empty_behavior: is_empty implies before
not_empty_behavior: not is_empty implies is_last
forth

-- Move internal cursor to next position.

-- (From DS_LINEAR)

require
not_after: not after
go_after

-- Move internal cursor to after position.

-- (From DS_LINEAR)

ensure
after: after
go_before

-- Move internal cursor to before position.

-- (From DS_BILINEAR)

ensure
before: before
go_to (a_cursor: like new_cursor)

-- Move internal cursor to a_cursor's position.

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
ensure
same_position: same_position (a_cursor)
search_back (v: G)

-- Move internal cursor to first position at or before current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.

-- (From DS_BILINEAR)

require
not_off: not off or before
search_forth (v: G)

-- Move internal cursor to first position at or after current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
not_off: not off or after
start

-- Move internal cursor to first position.

-- (From DS_LINEAR)

ensure
empty_behavior: is_empty implies after
not_empty_behavior: not is_empty implies is_first

feature -- Element change

force (v: G; k: K)

-- Associate v with key k.
-- Resize table if necessary.
-- Do not move cursors.

-- (From DS_TABLE)

require
valid_key: valid_key (k)
ensure
inserted: has (k) and then item (k) = v
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
force_last (v: G; k: K)

-- Associate v with key k. Put v at the end of table
-- if no item was already associated with k, or replace
-- existing item otherwise.
-- Resize table if necessary.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

ensure
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
inserted: has (k) and then item (k) = v
last: (not old has (k)) implies last = v
force_new (v: G; k: K)

-- Associate v with key k.
-- Resize table if necessary.
-- Do not move cursors.

-- (From DS_TABLE)

require
valid_key: valid_key (k)
new_item: not has (k)
ensure
one_more: count = old count + 1
inserted: has (k) and then item (k) = v
put (v: G; k: K)

-- Associate v with key k.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
not_full: not is_full
ensure
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
inserted: has (k) and then item (k) = v
put_last (v: G; k: K)

-- Associate v with key k. Put v at the end of table
-- if no item was already associated with k, or replace
-- existing item otherwise.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
not_full: not is_full
ensure
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
inserted: has (k) and then item (k) = v
last: (not old has (k)) implies last = v
put_new (v: G; k: K)

-- Associate v with key k.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
not_full: not is_full
new_item: not has (k)
ensure
one_more: count = old count + 1
inserted: has (k) and then item (k) = v
replace (v: G; k: K)

-- Replace item associated with k by v.
-- Do not move cursors.

-- (From DS_TABLE)

require
has_k: has (k)
ensure
replaced: item (k) = v
same_count: count = old count
replace_found_item (v: G)

-- Replace item associated with
-- the key of found_item by v.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
item_found: found
ensure
replaced: found_item = v
same_count: count = old count
swap (k, l: K)

-- Exchange items associated with k and l.

-- (From DS_TABLE)

require
valid_k: has (k)
valid_l: has (l)
ensure
same_count: count = old count
new_k: item (k) = old item (l)
new_l: item (l) = old item (k)

feature -- Removal

remove (k: K)

-- Remove item associated with k.
-- Move any cursors at this position forth.

-- (From DS_TABLE)

require
valid_key: valid_key (k)
ensure
same_count: (not old has (k)) implies (count = old count)
one_less: (old has (k)) implies (count = old count - 1)
removed: not has (k)
remove_found_item

-- Remove item found by last call to search.
-- Move any cursors at this position forth.

-- (From DS_SPARSE_CONTAINER)

require
item_found: found
ensure
one_less: count = old count - 1
wipe_out

-- Remove all items from container.
-- Move all cursors off.

-- (From DS_CONTAINER)

ensure
wiped_out: is_empty

feature -- Resizing

resize (n: INTEGER)

-- Resize container so that it can contain
-- at least n items. Do not lose any item.
-- Do not move cursors.

-- (From DS_RESIZABLE)

require
n_large_enough: n >= capacity
ensure
capacity_set: capacity = n

feature -- Duplication

cloned_object: like Current

-- Clone of current object

-- (From KL_CLONABLE)

ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)
copy (other: like Current)

-- Copy other to current container.
-- Move all cursors off (unless other = Current).

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)
to_array: ARRAY [G]

-- Array containing the same items as current
-- container in the same order

-- (From DS_LINEAR)

ensure
to_array_not_void: Result /= Void
same_count: Result.count = count

feature -- Setting

set_equality_tester (a_tester: like equality_tester)

-- Set equality_tester to a_tester.
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

require
equality_tester_settable: equality_tester_settable (a_tester)
ensure
equality_tester_set: equality_tester = a_tester
set_key_equality_tester (a_tester: like key_equality_tester)

-- Set key_equality_tester to a_tester.
-- A void key equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SPARSE_TABLE)

require
key_equality_tester_settable: key_equality_tester_settable (a_tester)
ensure
key_equality_tester_set: key_equality_tester = a_tester

feature -- Optimization

compress

-- Remove holes between stored items. May avoid
-- resizing when calling force_last for example.
-- Do not lose any item. Do not move cursors.

-- (From DS_SPARSE_CONTAINER)

ensure
same_count: count = old count
compressed: last_position = count
not_reszied: capacity = old capacity

feature -- Search

search (k: K)

-- Search for item at key k.
-- If found, set found to true, and set
-- found_item to item associated with k.

-- (From DS_SPARSE_CONTAINER)

ensure then
found_set: found = has (k)
found_item_set: found implies (found_item = item (k))

feature {DS_CURSOR} -- Cursor implementation

add_traversing_cursor (a_cursor: like new_cursor)

-- Add a_cursor to the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
after_position: INTEGER

-- Special values for before and after cursor positions

-- (From DS_SPARSE_CONTAINER)

cursor_after (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to right of a_cursor?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_back (a_cursor: like new_cursor)

-- Move a_cursor to previous position.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_before: not cursor_before (a_cursor)
cursor_before (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to left of a_cursor?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_finish (a_cursor: like new_cursor)

-- Move a_cursor to last position.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_before (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_last (a_cursor)
cursor_forth (a_cursor: like new_cursor)

-- Move a_cursor to next position.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_after: not cursor_after (a_cursor)
cursor_go_after (a_cursor: like new_cursor)

-- Move a_cursor to after position.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_after: cursor_after (a_cursor)
cursor_go_before (a_cursor: like new_cursor)

-- Move a_cursor to before position.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_before: cursor_before (a_cursor)
cursor_go_to (a_cursor, other: like new_cursor)

-- Move a_cursor to other's position.

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
other_valid: valid_cursor (other)
ensure
same_position: cursor_same_position (a_cursor, other)
cursor_is_first (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on first item?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = first)
cursor_is_last (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on last item?

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = last)
cursor_item (a_cursor: like new_cursor): G

-- Item at a_cursor position

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor)
cursor_key (a_cursor: like new_cursor): K

-- Key at a_cursor position

-- (From DS_SPARSE_TABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor)
cursor_off (a_cursor: like new_cursor): BOOLEAN

-- Is there no item at a_cursor position?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_same_position (a_cursor, other: like new_cursor): BOOLEAN

-- Is a_cursor at same position as other?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
cursor_search_back (a_cursor: like new_cursor; v: G)

-- Move a_cursor to first position at or before its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move before if not found.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_before (a_cursor)
cursor_search_forth (a_cursor: like new_cursor; v: G)

-- Move a_cursor to first position at or after its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_after (a_cursor)
cursor_start (a_cursor: like new_cursor)

-- Move a_cursor to first position.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_after (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_first (a_cursor)
remove_traversing_cursor (a_cursor: like new_cursor)

-- Remove a_cursor from the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void

feature {DS_MULTIARRAYED_SPARSE_TABLE_CURSOR} -- Implementation

clashes_item (i: INTEGER): INTEGER

-- Item at position i in clashes

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
items_item (i: INTEGER): G

-- Item at position i in items

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
items_put (v: G; i: INTEGER)

-- Put v at position i in items.

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
ensure
inserted: items_item (i) = v
keys_item (i: INTEGER): K

-- Item at position i in keys

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
last_position: INTEGER

-- All slots to the right of this position
-- are guaranteed to be free

-- (From DS_SPARSE_CONTAINER)

valid_position (i: INTEGER): BOOLEAN

-- Is there a slot at position i?

-- (From DS_SPARSE_CONTAINER)

ensure
definition: Result = (1 <= i and i <= capacity)
valid_slot (i: INTEGER): BOOLEAN

-- Is there an item at position i?

-- (From DS_SPARSE_CONTAINER)

require
valid_i: valid_position (i)

invariant

chunk_size_positive: chunk_size > 0
items_not_void: items /= Void
items_count1: capacity = 0 implies items.count = 0
items_count2: capacity > 0 implies (items.count = ((capacity) // chunk_size) + 1)
special_item_routines_not_void: special_item_routines /= Void
array_special_item_routines_not_void: array_special_item_routines /= Void
keys_not_void: keys /= Void
keys_count1: capacity = 0 implies keys.count = 0
keys_count2: capacity > 0 implies (keys.count = ((capacity) // chunk_size) + 1)
special_key_routines_not_void: special_key_routines /= Void
array_special_key_routines_not_void: array_special_key_routines /= Void
clashes_not_void: clashes /= Void
clashes_count1: capacity = 0 implies clashes.count = 0
clashes_count2: capacity > 0 implies (clashes.count = ((capacity) // chunk_size) + 1)
slots_not_void: slots /= Void
slots_count: slots.count = (modulus // chunk_size) + 1

-- From DS_CONTAINER
positive_count: count >= 0
empty_definition: is_empty = (count = 0)

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

valid_position: position = No_position or else valid_position (position)
capacity_constraint: capacity < modulus

-- From DS_BILINEAR
not_both: initialized implies (not (after and before))
before_constraint: initialized implies (before implies off)

-- From DS_LINEAR
after_constraint: initialized implies (after implies off)

empty_constraint: initialized implies (is_empty implies off)
internal_cursor_not_void: initialized implies (internal_cursor /= Void)
valid_internal_cursor: initialized implies valid_cursor (internal_cursor)

-- From DS_RESIZABLE
count_constraint: count <= capacity
full_definition: is_full = (count = capacity)

end