class HASHED_BIJECTIVE_DICTIONARY [V_ -> HASHABLE, K_ -> HASHABLE]

Features exported to ANY

Direct parents

conformant parents

BIJECTIVE_DICTIONARY

Summary

creation features

exported features

Counting:

To provide iterating facilities:

Agents based features:

Indexing:

Details

make

Create an empty dictionary. Internal storage capacity of the dictionary is initialized using the Default_size value. Then, tuning of needed storage capacity is performed automatically according to usage. If you are really sure that your dictionary is always really bigger than Default_size, you may consider to use with_capacity to save some execution time.

ensure

  • capacity = Default_size

with_capacity (medium_size: INTEGER)

May be used to save some execution time if one is sure that storage size will rapidly become really bigger than Default_size. When first remove occurs, storage size may naturally become smaller than medium_size. Afterall, tuning of storage size is done automatically according to usage.

require

  • medium_size > 0

ensure

  • is_empty
  • capacity >= medium_size

has (k: K_): BOOLEAN

Is there a value currently associated with key k?

require

  • k /= Void

ensure

  • Result implies has_value(at(k))

at (k: K_): V_

Return the value associated to key k. (See also reference_at if V_ is a reference type.)

require

  • has(k)

ensure

  • k.is_equal(key_at(Result))

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.

require

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

ensure

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

fast_has (k: K_): BOOLEAN

Is there a value currently associated with key k?

require

  • k /= Void

ensure

  • Result implies fast_has_value(fast_at(k))

fast_at (k: K_): V_

Return the value associated to key k. (See also reference_at if V_ is a reference type.)

require

  • fast_has(k)

ensure

  • Result = at(k)
  • fast_key_at(Result) = k

fast_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.

require

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

ensure

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

has_value (v: V_): BOOLEAN

Is there a value v?

require

  • v /= Void

ensure

  • Result implies has(key_at(v))

key_at (v: V_): K_

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

require

  • has_value(v)

ensure

  • v.is_equal(at(Result))

fast_has_value (v: V_): BOOLEAN

Is there a value v?

require

  • v /= Void

ensure

  • Result implies fast_has(fast_key_at(v))

fast_key_at (v: V_): K_

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

require

  • fast_has_value(v)

ensure

  • Result = key_at(v)
  • fast_at(Result) = v

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.

require

  • has(k) implies key_at(at(k)).is_equal(k)
  • has_value(v) implies key_at(v).is_equal(k)

ensure

  • value_updated: v = fast_at(k)
  • key_updated: k = fast_key_at(v)

add (v: V_, k: K_)

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

require

  • not has(k)
  • not has_value(v)

ensure

  • count = 1 + old count
  • v = fast_at(k)
  • k = fast_key_at(v)

remove (k: K_)

Remove entry k (which may exist or not before this call).

require

  • k /= Void

ensure

  • not has(k)

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 to select the most appropriate.

require

  • capacity > 0

ensure

  • capacity = old capacity
  • 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 to select the most appropriate.

require

  • capacity > 0

ensure

  • capacity = old capacity
  • 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

  • Result = key_at(item(index))

Default_size: INTEGER

Default size for the storage area in number of items.

internal_key (k: K_): K_

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

require

  • has(k)

ensure

  • Result.is_equal(k)
  • internal_key(Result) = Result
  • at(k) = fast_at(Result)

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

count: INTEGER

Actual count of stored elements.

ensure

  • definition: Result = upper - lower + 1

is_empty: BOOLEAN

Is it empty ?

ensure

  • definition: Result = (count = 0)

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

get_new_iterator_on_keys: ITERATOR[K_]

ensure

  • Result /= Void

is_equal (other: HASHED_BIJECTIVE_DICTIONARY [V_ -> HASHABLE, K_ -> HASHABLE]): BOOLEAN

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

require

  • other /= Void

ensure

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

copy (other: HASHED_BIJECTIVE_DICTIONARY [V_ -> HASHABLE, K_ -> HASHABLE])

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, exists.

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

Do all [V_, K_] associations satisfy test?

See also do_all, exists.

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

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

See also do_all, for_all.

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)

Class invariant