class AVL_DICTIONARY [V_, K_ -> COMPARABLE]

All features

Associative memory. Values of type V_ are stored using Keys of type K_.

Efficient implementation of DICTIONARY using an AVL balanced tree. AVL stands for the names of G. M. Adel'son-Velskii and E. M. Landis, two Russian mathematicians who first came up with this method of keeping the tree balanced.

Direct parents

conformant parents

SIMPLE_DICTIONARY

non-conformant parents

AVL_TREE

Summary

creation features

exported features

Counting:

Basic access:

Removing:

To provide iterating facilities:

Agents based features:

Implement manifest generic creation.

Indexing:

Adding and removing:

Looking and searching:

Iterating internals:

Details

make

Creates an empty dictionary.

ensure

  • is_empty

capacity: INTEGER

Approximation of the actual internal storage capacity. The capacity will grow automatically when needed (i.e. capacity is not a limit for the number of values stored). Also note that the capacity value may not be always accurate depending of the implementation (anyway, this capacity value is at least equals to count).

at (k: K_): V_

Return the value associated to key k.

See also fast_at, reference_at, has.

require

  • has(k)

fast_at (k: K_): V_

Return the value associated to key k using basic = for comparison.

See also at, reference_at, fast_reference_at.

require

  • fast_has(k)

reference_at (k: K_): V_

Return Void or the value associated with key k. Actually, this feature is useful when the type of values (the type V_) is a reference type, to avoid using has just followed by at to get the corresponding value.

See also fast_reference_at, at, has.

require

  • k /= Void
  • values_are_expanded: Result /= Void implies not Result.is_expanded_type

ensure

  • has(k) implies Result = at(k)

fast_reference_at (k: K_): V_

Same work as reference_at, but basic = is used for comparison.

See also reference_at, at, has.

require

  • k /= Void
  • values_are_expanded: Result /= Void implies not Result.is_expanded_type

ensure

  • fast_has(k) implies Result = fast_at(k)

put (v: V_, k: K_)

Change some existing entry or add the new one. If there is as yet no key k in the dictionary, enter it with item v. Otherwise overwrite the item associated with key k. As the put procedure actually uses is_equal, you may consider to use fast_put for expanded objects as well while trying to get the very best performances.

See also fast_put, add.

require

  • k /= Void

ensure

  • v = at(k)

add (v: V_, k: K_)

To add a new entry k with its associated value v. Actually, this is equivalent to call put, but it may run a little bit faster.

See also put, fast_put.

require

  • not has(k)

ensure

  • count = 1 + old count
  • v = at(k)

fast_put (v: V_, k: K_)

Same job as put, but uses basic = for comparison.

See also put, add.

require

  • k /= Void

ensure

  • v = at(k)

occurrences (v: V_): INTEGER

Number of occurrences using is_equal for comparison.

See also fast_occurrences, fast_has, has.

ensure

  • Result >= 0

fast_occurrences (v: V_): INTEGER

Number of occurrences using basic = for comparison.

See also occurrences, fast_has, has.

ensure

  • Result >= 0

key_at (v: V_): K_

Retrieve the key used for value v using is_equal for comparison.

See also fast_key_at, at.

require

  • occurrences(v) = 1

ensure

  • (create {SAFE_EQUAL[V_]}.default_create).test(at(Result), v)

fast_key_at (v: V_): K_

Retrieve the key used for value v using = for comparison.

See also key_at, at.

require

  • fast_occurrences(v) = 1

ensure

  • at(Result) = v

clear_count

Discard all items (is_empty is True after that call). The internal capacity is not changed by this call.

See also clear_count_and_capacity, remove.

ensure

  • is_empty: count = 0
  • capacity = old capacity

clear_count_and_capacity

Discard all items (is_empty is True after that call). The internal capacity may also be reduced after this call.

See also clear_count, remove.

ensure

  • is_empty: count = 0
  • capacity <= old capacity

item (index: INTEGER): V_

Item at the corresponding index i.

See also lower, upper, valid_index.

require

  • valid_index(index)

ensure

  • Result = at(key(index))

key (index: INTEGER): K_

require

  • valid_index(index)

ensure

  • at(Result) = item(index)

get_new_iterator_on_keys: ITERATOR[K_]

ensure

  • Result /= Void

internal_key (k: K_): K_

Retrieve the internal key object which correspond to the existing entry k (the one memorized into the Current dictionary).

See also has, fast_has.

require

  • has(k)

ensure

  • Result.is_equal(k)

value_memory: V_
set_value_and_key (n: AVL_DICTIONARY_NODE[V_K_])
set_value (n: AVL_DICTIONARY_NODE[V_K_])
exchange_and_discard (n1: AVL_DICTIONARY_NODE[V_K_], n2: AVL_DICTIONARY_NODE[V_K_])

require

  • n1 /= Void
  • n2 /= Void

ensure

  • map_dirty
  • count = old count - 1
  • rebalance

discard_node (n: AVL_DICTIONARY_NODE[V_K_])

require

  • n /= Void

common_lost_nodes: DICTIONARY [V_, K_][WEAK_REFERENCE [G_][ANY_AVL_DICTIONARY_NODE]STRING]
a_new_node: AVL_DICTIONARY_NODE[V_K_]
make

Creates an empty dictionary.

ensure

  • is_empty

deferred count: INTEGER

Actual count of stored elements.

ensure

  • definition: Result = upper - lower + 1

is_empty: BOOLEAN

Is it empty?

ensure

  • definition: Result = (count = 0)

deferred has (k: K_): BOOLEAN

Is there a value currently associated with key k?

See also fast_has, at.

require

  • k /= Void

frozen @ (k: K_): V_

The infix notation which is actually a synonym for at.

require

  • has(k)

ensure

  • definition: Result = at(k)

deferred fast_has (k: K_): BOOLEAN

Is there a value currently associated with key k? Using basic = for comparison.

See also has, at, fast_at.

require

  • k /= Void

deferred remove (k: K_)

Remove entry k (which may exist or not before this call). As the remove procedure actually uses is_equal, you may consider to use fast_remove for expanded objects as well while trying to get the very best performances.

See also fast_remove, clear_count.

require

  • k /= Void

ensure

  • not has(k)

deferred fast_remove (k: K_)

Same job as remove, but uses basic = for comparison.

See also remove, clear_count.

require

  • k /= Void

ensure

  • not has(k)

clear
This feature is obsolete: You must decide to use `clear_count' or `clear_count_and_capacity' (may 9th 2004).
lower: INTEGER

Minimum index.

See also upper, valid_index, item.

upper: INTEGER

Maximum index.

See also lower, valid_index, item.

ensure

  • Result = count

first: V_

The very first item.

See also last, item.

require

  • not is_empty

ensure

  • definition: Result = item(lower)

last: V_

The last item.

See also first, item.

require

  • not is_empty

ensure

  • definition: Result = item(upper)

get_new_iterator_on_items: ITERATOR[V_]

ensure

  • Result /= Void

key_map_in (buffer: COLLECTION[K_])

Append in buffer, all available keys (this may be useful to speed up the traversal).

See also item_map_in.

require

  • buffer /= Void

ensure

  • buffer.count = count + old buffer.count

item_map_in (buffer: COLLECTION[V_])

Append in buffer, all available items (this may be useful to speed up the traversal).

See also key_map_in.

require

  • buffer /= Void

ensure

  • buffer.count = count + old buffer.count

is_equal (other: AVL_DICTIONARY [V_, K_ -> COMPARABLE]): BOOLEAN

Do both dictionaries have the same set of associations? Keys are compared with is_equal and values are comnpared with the basic = operator.

See also is_equal_map.

require

  • other /= Void

ensure

  • Result implies count = other.count
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

is_equal_map (other: AVL_DICTIONARY [V_, K_ -> COMPARABLE]): BOOLEAN

Do both dictionaries have the same set of associations? Both keys and values are compared with is_equal.

See also is_equal.

copy (other: AVL_DICTIONARY [V_, K_ -> COMPARABLE])

Reinitialize by copying all associations of other.

require

  • same_dynamic_type(other)

ensure

  • is_equal(other)

do_all (action: ROUTINE[TUPLE[TUPLE 2[V_K_]]])

Apply action to every [V_, K_] associations of Current.

See also for_all, exist.

for_all (test: PREDICATE[TUPLE[TUPLE 2[V_K_]]]): BOOLEAN

Do all [V_, K_] associations satisfy test?

See also do_all, exist.

exists (test: PREDICATE[TUPLE[TUPLE 2[V_K_]]]): BOOLEAN

Does at least one [V_, K_] association satisfy test?

See also for_all, do_all.

manifest_make (needed_capacity: INTEGER)

Manifest creation of a dictionary.

manifest_put (index: INTEGER, v: V_, k: K_)

require

  • not has(k)

manifest_semicolon_check: INTEGER

Put semicolons between successive value-key pairs.

key_safe_equal (k1: K_, k2: K_): BOOLEAN

Because keys are never Void, we do not rely on the SAFE_EQUAL class.

require

  • k1 /= Void
  • k2 /= Void

valid_index (i: INTEGER): BOOLEAN

True when i is valid (i.e., inside actual bounds).

See also lower, upper, item.

ensure

  • definition: Result = (lower <= i and i <= upper)

debug_string: STRING
count: INTEGER
remove (e: E_)
fast_remove (e: E_)
root: AVL_TREE_NODE[E_]
rebalance: BOOLEAN
item_memory: E_
deferred set_value_and_key (n: AVL_TREE_NODE[E_])
deferred set_value (n: AVL_TREE_NODE[E_])
fast_do_insert (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > old node_height(n))

do_insert (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > old node_height(n))

left_grown (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) - node_height(n.left) + 1 = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > 1 + old node_height(n.right).max(node_height(n.left) - 1))

right_grown (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) - 1 - node_height(n.left) = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > 1 + old node_height(n.left).max(node_height(n.right) - 1))

fast_do_remove (n: AVL_TREE_NODE[E_], e: E_): AVL_TREE_NODE[E_]

ensure

  • Result = Void or else Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < old node_height(n))

do_remove (n: AVL_TREE_NODE[E_], e: E_): AVL_TREE_NODE[E_]

ensure

  • Result = Void or else Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < old node_height(n))

remove_right (n1: AVL_TREE_NODE[E_], n2: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • n1 /= Void
  • n2 /= Void

ensure

  • Result = Void or else Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < old node_height(n2))

left_shrunk (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) - node_height(n.left) - 1 = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < 1 + old node_height(n.right).max(node_height(n.left) + 1))

right_shrunk (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) + 1 - node_height(n.left) = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < 1 + old node_height(n.left).max(node_height(n.right) + 1))

deferred exchange_and_discard (n1: AVL_TREE_NODE[E_], n2: AVL_TREE_NODE[E_])

require

  • n1 /= Void
  • n2 /= Void

ensure

  • map_dirty
  • count = old count - 1
  • rebalance

clear_nodes (node: AVL_TREE_NODE[E_])
node_height (node: AVL_TREE_NODE[E_]): INTEGER
has (e: E_): BOOLEAN

Is element e in the set?

fast_has (e: E_): BOOLEAN

Is element e in the set?

build_map

require

  • build_needed: map_dirty

ensure

  • build_done: not map_dirty

map: FAST_ARRAY[AVL_TREE_NODE[E_]]

Elements in a row for iteration. See build_map.

map_dirty: BOOLEAN

True when the map needs to be built again for the iterators. See build_map.

new_node: AVL_TREE_NODE[E_]
deferred a_new_node: AVL_TREE_NODE[E_]
deferred discard_node (n: AVL_TREE_NODE[E_])

require

  • n /= Void

lost_nodes: WEAK_REFERENCE[AVL_TREE_NODE[E_]]
balanced: INTEGER
imbalanced_left: INTEGER
imbalanced_right: INTEGER

Class invariant