elogger API
Overview Classes Cluster Class Index          Top Features

structure.table

Class DS_ARRAYED_SPARSE_TABLE


Direct ancestors

DS_SPARSE_TABLE, KL_IMPORTED_SPECIAL_ROUTINES

Known direct descendants

DS_HASH_TABLE

Features

Invariants

indexing

description

Sparse tables implemented with single arrays. Ancestor of
hash tables which should supply its hashing mechanism.

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

deferred class DS_ARRAYED_SPARSE_TABLE [G, K]

inherit

DS_SPARSE_TABLE
DS_TABLE
DS_SPARSE_CONTAINER
KL_IMPORTED_SPECIAL_ROUTINES

feature -- Access

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

last: G

-- Last item in container
-- (From DS_BILINEAR)

require

not_empty: not is_empty

ensure

has_last: has (Result)

item_for_iteration: G

-- Item at internal cursor position
-- (From DS_TRAVERSABLE)

require

not_off: not off

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

ANY_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY
-- (From KL_IMPORTED_ANY_ROUTINES)

ensure

any_routines_not_void: Result /= Void

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

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)

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

equality_tester: KL_EQUALITY_TESTER[G]

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

new_cursor: DS_ARRAYED_SPARSE_TABLE_CURSOR[G, K]

-- New external cursor for traversal
-- (From DS_TRAVERSABLE)

ensure

cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)

feature -- Measurement

default_capacity: INTEGER

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

ensure

default_capacity_positive: Result >= 0

capacity: INTEGER

-- Maximum number of items in container
-- (From DS_RESIZABLE)

count: INTEGER

-- Number of items in container
-- (From DS_CONTAINER)

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)

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)

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)

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)

off: BOOLEAN

-- Is there no item at internal cursor position?
-- (From DS_TRAVERSABLE)

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

before: BOOLEAN

-- Is there no valid position to left of internal cursor?
-- (From DS_BILINEAR)

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)

found: BOOLEAN

-- Did last call to search succeed?
-- (From DS_SPARSE_CONTAINER)

ensure

definition: Result = (found_position /= No_position)

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

has (k: K): BOOLEAN

-- Is there an item associated with k?
-- (From DS_TABLE)

ensure

valid_key: Result implies valid_key (k)

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)

valid_key (k: K): BOOLEAN

-- Is k a valid key?
-- (From DS_TABLE)

ensure then

defintion: Result = True

is_empty: BOOLEAN

-- Is container empty?
-- (From DS_CONTAINER)

feature -- Cursor movement

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

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

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)

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

go_before

-- Move internal cursor to before position.
-- (From DS_BILINEAR)

ensure

before: before

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

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)

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

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)

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

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_SPARSE_TABLE_CURSOR} -- Cursor implementation

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)

feature {DS_SPARSE_CONTAINER_CURSOR} -- Cursor implementation

after_position: INTEGER

-- Special values for before and after cursor positions
-- (From DS_SPARSE_CONTAINER)

before_position: INTEGER

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_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)

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 -- Setting

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

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

feature {DS_SPARSE_CONTAINER_CURSOR} -- Implementation

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)

feature {DS_ARRAYED_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

invariant

items_not_void: items /= Void
items_count: items.count = capacity + 1
keys_not_void: keys /= Void
keys_count: keys.count = capacity + 1
clashes_not_void: clashes /= Void
clashes_count: clashes.count = capacity + 1
slots_not_void: slots /= Void
slots_count: slots.count = modulus + 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)

-- From DS_SPARSE_CONTAINER
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)

-- From DS_TRAVERSABLE
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)

Documentation generated by edoc