class interface BASIC_HASH[V,K->HASHABLE]

creation
   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
         is_empty;
         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

   from_tuple_table (table: ARRAY[TUPLE[K,V]])
      -- not fully tested
      -- Create the dictionary from a TUPLE table. This
      -- code is untested and due to SmallEiffel limitations
      -- in the -0.74 Betas, probably will not work.
      require
         table /= Void and then table.count >= 1

   from_table (table: COLLECTION[K])
      -- Accept a 2D array that contains
      -- two entries, and create a HASH from them.
      -- the key is assumed to be the first entry.
      -- Example:
      -- create my_hash.from_table( <<
      --                         1, 2,
      --                         3, 4,
      --                         5, 6 >> )
      require
         valid_table: table /= Void and then table.count >= 2 and then table.count \\ 2 = 0

feature(s) from DICTIONARY
   Default_size: INTEGER
      -- Default size for the storage area in muber of items.

feature(s) from DICTIONARY
   -- Counting:

   capacity: INTEGER
      -- Of the buckets storage area.

   count: INTEGER
      -- Actual count of stored elements.

   is_empty: BOOLEAN
      -- Is it empty ?
      ensure
         Result = (count = 0)

feature(s) from DICTIONARY
   -- 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.)
      require
         has(k)

   infix "@" (k: K): V
      -- Return the value associated to key k.
      -- (See also reference_at if V is a reference type.)
      require
         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.
      ensure
         has(k) implies Result = at(k)

feature(s) from DICTIONARY
   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.
      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 may run a little bit faster.
      require
         not has(k)
      ensure
         count = 1 + old count;
         v = at(k)

feature(s) from DICTIONARY
   -- Looking and searching some value:

   occurrences (v: V): INTEGER
      -- Number of occurrences using equal.
      -- See also fast_occurrences to chose the apropriate one.
      ensure
         Result >= 0

   fast_occurrences (v: V): INTEGER
      -- Number of occurrences using =.
      -- See also occurrences to chose the apropriate one.
      ensure
         Result >= 0

   key_at (v: V): K
      -- Retrieve the key used for value v using equal for comparison.
      require
         occurrences(v) = 1
      ensure
         equal(at(Result),v)

   fast_key_at (v: V): K
      -- Retrieve the key used for value v using = for comparison.
      require
         fast_occurrences(v) = 1
      ensure
         at(Result) = v

feature(s) from DICTIONARY
   -- Removing:

   remove (k: K)
      -- Remove entry k (which may exist or not before this call).
      ensure
         not has(k)

   clear
      -- Discard all items.
      ensure
         is_empty;
         capacity = old capacity

feature(s) from DICTIONARY
   -- To provide iterating facilities:

   lower: INTEGER

   upper: INTEGER
      ensure
         Result = count

   valid_index (index: INTEGER): BOOLEAN
      ensure
         Result = index.in_range(lower,upper)

   item (index: INTEGER): V
      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_items: ITERATOR[V]

   get_new_iterator_on_keys: ITERATOR[K]

   key_map_in (buffer: COLLECTION[K])
      -- Append in buffer, all available keys (this may be useful to
      -- speed up the traversal).
      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).
      require
         buffer /= Void
      ensure
         buffer.count = count + old buffer.count

feature(s) from DICTIONARY
   is_equal (other: like Current): 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_not_void: other /= Void
      ensure
         Result implies count = other.count;
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

   is_equal_map (other: like Current): 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: like Current)
      -- Reinitialize by copying all associations of other.
      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

feature(s) from DICTIONARY
   -- Agents based features:

   do_all (action: ROUTINE[ANY,TUPLE[V,K]])
      -- Apply action to every [V,K] associations of Current.

   for_all (test: PREDICATE[ANY,TUPLE[V,K]]): BOOLEAN
      -- Do all [V,K] associations satisfy test?

   exists (test: PREDICATE[ANY,TUPLE[V,K]]): BOOLEAN
      -- Does at least one [V,K] association satisfy test?

feature(s) from DICTIONARY
   -- Other features:

   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)

feature(s) from BASIC_HASH
   -- inherited
   -- implemented here

   from_tuple_table (table: ARRAY[TUPLE[K,V]])
      -- not fully tested
      -- Create the dictionary from a TUPLE table. This
      -- code is untested and due to SmallEiffel limitations
      -- in the -0.74 Betas, probably will not work.
      require
         table /= Void and then table.count >= 1

   from_table (table: COLLECTION[K])
      -- Accept a 2D array that contains
      -- two entries, and create a HASH from them.
      -- the key is assumed to be the first entry.
      -- Example:
      -- create my_hash.from_table( <<
      --                         1, 2,
      --                         3, 4,
      --                         5, 6 >> )
      require
         valid_table: table /= Void and then table.count >= 2 and then table.count \\ 2 = 0

   keys: ARRAY[K]
      -- return a list of the keys to the client.

invariant

    capacity > 0;

    capacity >= count;

    cache_user.in_range(- 1,count);

    cache_user > 0 implies cache_node /= Void;

    cache_user > 0 implies cache_buckets.in_range(0,capacity - 1);

end of BASIC_HASH[V,K->HASHABLE]