class interface DICTIONARY[V,K->HASHABLE]
   -- 
   --  Associative memory. 
   --  Values of type V are stored using Keys of type K.
   -- 

creation
   make
      --  Internal initial storage size of the dictionary is set to
      --  the default Default_size value. Then, tuning of needed storage 
      --  size is done automatically according to usage. 
      --  If you are really sure that your dictionary is always really
      --  bigger than Default_size, you may use with_capacity to save some 
      --  execution time.

      ensure
         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
         empty;
         capacity = medium_size

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


feature(s) from DICTIONARY
   --  Counting :

   count: INTEGER
      --  Actual count of stored elements.


   empty: BOOLEAN
      ensure
         Result = (count = 0)

feature(s) from DICTIONARY
   --  Basic access :

   has (k: K): BOOLEAN
      --  Is there an item currently associated with key k ?


   at (k: K): V
      --  Return the item stored at key k.

      require
         has(k)

   infix "@" (k: K): V
      --  Return the item stored at key k.

      require
         has(k)

feature(s) from DICTIONARY
   --  The only way to add or to change an entry :

   put (v: V; k: K)
      --  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)

feature(s) from DICTIONARY
   --  Looking and Searching :

   nb_occurrences (v: V): INTEGER
      --  Number of occurrences using equal.
      --  See also fast_nb_occurrences to chose
      --  the apropriate one.

      ensure
         Result >= 0

   fast_nb_occurrences (v: V): INTEGER
      --  Number of occurrences using =.

      ensure
         Result >= 0

   key_at (v: V): K
      --  Retrieve the key used for value v using equal for comparison. 

      require
         nb_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_nb_occurrences(v) = 1
      ensure
         at(Result) = v

   capacity: INTEGER

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
         empty

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

   lower: INTEGER

   upper: INTEGER
      ensure
         Result = count

   valid_index (idx: INTEGER): BOOLEAN
      ensure
         Result = (1 <= idx and then idx <= count)

   item (idx: INTEGER): V
      require
         valid_index(idx)
      ensure
         Result = at(key(idx))

   key (idx: INTEGER): K
      require
         valid_index(idx)
      ensure
         at(Result) = item(idx)

feature(s) from DICTIONARY
   is_equal (other: like Current): BOOLEAN
      --  Is other attached to an object considered equal to 
      --  current object ?

      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

   copy (other: like Current)
      --  Update current object using fields of object attached
      --  to other, so as to yield equal objects.

      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

invariant
   keys.upper = store.upper and store.upper = chain.upper;
   buckets.upper = modulus - 1;
   - 1 <= first_free_slot and first_free_slot <= chain.upper;

end of DICTIONARY[V,K->HASHABLE]