Section Header
    + name := HASHED_DICTIONARY[V,K];
    - comment :=" Associative memory.\
\Values of type `V' are stored using Keys of type `K'.";
Efficient implementation of DICTIONARY using `hash_code' on keys.
Section Inherit
    - parent_simple_dictionary:Expanded SIMPLE_DICTIONARY[V,K];
Section Public
HASHED_DICTIONARY
    + buckets:NATIVE_ARRAY[HASHED_DICTIONARY_NODE[V,K]];
        The `buckets' storage area is the primary hash table of `capacity'
        elements. To search some key, the first access is done in `buckets'
        using the remainder of the division of the key `hash_code' by
        `capacity'. In order to try to avoid clashes, `capacity' is always a
        prime number (selected using HASH_TABLE_SIZE).
Section Public
    - default_size:INTEGER :=
        Default size for the storage area in number of items.
Counting:
    + capacity:INTEGER;
        Of the `buckets' storage area.
    + count:INTEGER;
        Actual `count' of stored elements.
Basic access:
    - has k:K :BOOLEAN <-
        Is there a value currently associated with key `k'?
    - at k:K :V <-
        Return the value associated to key `k'.
        (See also `reference_at' if V is a reference type.)
    - reference_at k:K :V <-
        Return NULL 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.
    - fast_has k:K :BOOLEAN <-
    - fast_at k:K :V <-
    - fast_reference_at k:K :V <-
        Return NULL 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.
Section Public
    - put v:V to 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'.
    - fast_put v:V to 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'.
    - add v:V to 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.
Removing:
    - remove k:K <-
        Remove entry `k' (which may exist or not before this call).
    - fast_remove k:K <-
    - clear <-
        Discard all items.
To provide iterating facilities:
    - item i:INTEGER :V <-
    - key index:INTEGER :K <-
    - key_map_in buffer:COLLECTION[K] <-
        Append in `buffer', all available keys (this may be useful to
        speed up the traversal).
    - item_map_in buffer:COLLECTION[V] <-
        Append in `buffer', all available items (this may be useful to
        speed up the traversal).
    - copy other:SELF <-
        Reinitialize by copying all associations of `other'.
Other features:
    - internal_key k:K :K <-
        Retrieve the internal key object which correspond to the existing
        entry `k' (the one memorized into the `self' dictionary).
Section Public
    - create:SELF <-
    - 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.
    - 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.
Invariant
[
-? {capacity > 0};
-? {capacity >= count};
-? {cache_user.in_range (-1) to count};
-? {(cache_user > 0) ->> {cache_node != NULL}};
-? {(cache_user > 0) ->> {cache_buckets.in_range 0 to (capacity - 1)}}
];
------------------- OLD --------------------