deferred class BIJECTIVE_DICTIONARY [V_, K_]

All features

Bijective associative memory. As for ordinary DICTIONARY, Values of type V_ are stored using Keys of type K_, but, in a BIJECTIVE_DICTIONARY, given one value of type V_, you can retrieve the unique corresponding key of type K_. In other words, with a BIJECTIVE_DICTIONARY, one key of type K_ gives you access to one value of type V_ which can be used to retrieve back the same unique original key.

At time beeing, the only one available implementation is the HASHED_BIJECTIVE_DICTIONARY class.

See also DICTIONARY class if you do not have a unique value for each key. By the way, also note that the interface of DICTIONARY is similar to the interface of BIJECTIVE_DICTIONARY in order to allow you to move from one to the other.

Direct parents

conformant parents

TRAVERSABLE

Known children

conformant children

HASHED_BIJECTIVE_DICTIONARY

Summary

exported features

Counting:

Basic access:

Removing:

To provide iterating facilities:

Agents based features:

Other features:

Implement manifest generic creation.

Indexing:

Details

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?

require

  • k /= Void

ensure

  • Result implies has_value(at(k))

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

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

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

deferred 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

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

deferred has_value (v: V_): BOOLEAN

Is there a value v?

require

  • v /= Void

ensure

  • Result implies has(key_at(v))

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

deferred fast_has_value (v: V_): BOOLEAN

Is there a value v?

require

  • v /= Void

ensure

  • Result implies fast_has(fast_key_at(v))

deferred 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

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

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

deferred remove (k: K_)

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

require

  • k /= Void

ensure

  • not has(k)

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

ensure

  • is_empty: count = 0
  • capacity = old capacity

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

ensure

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

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

lower: INTEGER

Minimum index.

See also upper, valid_index, item.

upper: INTEGER

Maximum index.

See also lower, valid_index, item.

ensure

  • Result = count

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

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)

deferred key (index: INTEGER): K_

require

  • valid_index(index)

ensure

  • Result = key_at(item(index))

get_new_iterator_on_items: ITERATOR[V_]

ensure

  • Result /= Void

get_new_iterator_on_keys: ITERATOR[K_]

ensure

  • Result /= Void

is_equal (other: BIJECTIVE_DICTIONARY [V_, K_]): 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: BIJECTIVE_DICTIONARY [V_, K_])

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.

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

deferred make
frozen 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

frozen val_safe_equal (v1: V_, v2: V_): BOOLEAN

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

require

  • v1 /= Void
  • v2 /= Void

manifest_make (needed_capacity: INTEGER)

Manifest creation of a dictionary.

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

require

  • v /= Void
  • k /= Void
  • not has(k)

manifest_semicolon_check: INTEGER

Put semicolons between successive value-key pairs.

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)