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]