Automatic generation produced by ISE Eiffel
note description: "Hash tables, used to store items identified by hashable keys" library: "Free implementation of ELKS library" instructions: "See instructions at the end of the class." warning: "[ Modifying an object used as a key by an item present in a table will cause incorrect behavior. If you will be modifying key objects, pass a clone, not the object itself, as key argument to put and replace_key. ]" class interface HASH_TABLE [G, K -> detachable HASHABLE] create make, make_equal feature -- Initialization make (n: INTEGER_32) -- Allocate hash table for at least `n' items. -- The table will be resized automatically -- if more than `n' items are inserted. require n_non_negative: n >= 0 ensure breathing_space: n < capacity more_than_minimum: capacity > Minimum_capacity no_status: not special_status make_equal (n: INTEGER_32) -- Allocate hash table for at least `n' items. -- The table will be resized automatically -- if more than `n' items are inserted. -- Use `~' to compare items. require n_non_negative: n >= 0 ensure breathing_space: n < capacity more_than_minimum: capacity > Minimum_capacity no_status: not special_status compare_objects: object_comparison accommodate (n: INTEGER_32) -- Reallocate table with enough space for `n' items; -- keep all current items. require n >= 0 ensure count_not_changed: count = old count breathing_space: count < capacity feature -- Access found_item: detachable G -- Item, if any, yielded by last search operation item alias "[]" (key: K): detachable G assign force -- Item associated with `key', if present -- otherwise default value of type `G'. -- Was declared in HASH_TABLE as synonym of at. note option: stable ensure then default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value) at alias "@" (key: K): detachable G assign force -- Item associated with `key', if present -- otherwise default value of type `G'. -- Was declared in HASH_TABLE as synonym of item. note option: stable ensure then default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value) has (key: K): BOOLEAN -- Is there an item in the table with key `key'? ensure then default_case: (key = computed_default_key) implies (Result = has_default) has_key (key: K): BOOLEAN -- Is there an item in the table with key `key'? Set found_item to the found item. ensure then default_case: (key = computed_default_key) implies (Result = has_default) found: Result = found item_if_found: found implies (found_item = item (key)) has_item (v: detachable G): BOOLEAN -- Does structure include `v'? -- (Reference or object equality, -- based on object_comparison.) current_keys: ARRAY [K] -- New array containing actually used keys, from 1 to count ensure good_count: Result.count = count item_for_iteration: G -- Element at current iteration position require not_off: not off key_for_iteration: K -- Key at current iteration position require not_off: not off cursor: CURSOR -- Current cursor position ensure cursor_not_void: Result /= Void new_cursor: HASH_TABLE_ITERATION_CURSOR [G, K] -- Fresh cursor associated with current structure iteration_item (i: INTEGER_32): G -- Entry at position `i'. hash_code_of (a_key: attached K): INTEGER_32 -- Hash_code value associated to `a_key'. ensure non_negative: Result >= 0 feature -- Measurement count: INTEGER_32 -- Number of items in table capacity: INTEGER_32 -- Number of items that may be stored. occurrences (v: detachable G): INTEGER_32 -- Number of table items equal to `v'. iteration_lower: INTEGER_32 -- Minimum index. iteration_upper: INTEGER_32 -- Maximum index. feature -- Comparison is_equal (other: like Current): BOOLEAN -- Does table contain the same information as `other'? same_keys (a_search_key, a_key: K): BOOLEAN -- Does `a_search_key' equal to `a_key'? require valid_search_key: valid_key (a_search_key) valid_key: valid_key (a_key) disjoint (other: HASH_TABLE [G, K]): BOOLEAN -- Is `Current' and `other' disjoint on their keys? -- Use same_keys for comparison. feature -- Status report Full: BOOLEAN = False -- Is structure filled to capacity? Extendible: BOOLEAN = False -- May new items be added? prunable: BOOLEAN -- May items be removed? conflict: BOOLEAN -- Did last operation cause a conflict? inserted: BOOLEAN -- Did last operation insert an item? replaced: BOOLEAN -- Did last operation replace an item? removed: BOOLEAN -- Did last operation remove an item? found: BOOLEAN -- Did last operation find the item sought? not_found: BOOLEAN -- Did last operation fail to find the item sought? after: BOOLEAN -- Is cursor past last item? -- Was declared in HASH_TABLE as synonym of off. off: BOOLEAN -- Is cursor past last item? -- Was declared in HASH_TABLE as synonym of after. valid_cursor (c: CURSOR): BOOLEAN -- Can cursor be moved to position `c'? require c_not_void: c /= Void valid_key (k: K): BOOLEAN -- Is `k' a valid key? valid_iteration_index (i: INTEGER_32): BOOLEAN -- Is `i' a valid index? feature -- Cursor movement start -- Bring cursor to first position. forth -- Advance cursor to next occupied position, -- or off if no such position remains. require not_off: not off go_to (c: CURSOR) -- Move to position `c'. require c_not_void: c /= Void valid_cursor: valid_cursor (c) search (key: K) -- Search for item of key `key'. -- If found, set found to true, and set -- found_item to item associated with `key'. ensure found_or_not_found: found or not_found item_if_found: found implies (found_item = item (key)) feature -- Element change put (new: G; key: K) -- Insert `new' with `key' if there is no other item -- associated with the same key. -- Set inserted if and only if an insertion has -- been made (i.e. `key' was not present). -- If so, set position to the insertion position. -- If not, set conflict. -- In either case, set found_item to the item -- now associated with `key' (previous item if -- there was one, `new' otherwise). -- -- To choose between various insert/replace procedures, -- see `instructions' in the Indexing clause. ensure then conflict_or_inserted: conflict or inserted insertion_done: inserted implies item (key) = new now_present: inserted implies has (key) one_more_if_inserted: inserted implies (count = old count + 1) unchanged_if_conflict: conflict implies (count = old count) same_item_if_conflict: conflict implies (item (key) = old (item (key))) found_item_associated_with_key: found_item = item (key) new_item_if_inserted: inserted implies (found_item = new) old_item_if_conflict: conflict implies (found_item = old (item (key))) default_property: has_default = ((inserted and (key = computed_default_key)) or ((conflict or (key /= computed_default_key)) and (old has_default))) force (new: G; key: K) -- Update table so that `new' will be the item associated -- with `key'. -- If there was an item for that key, set found -- and set found_item to that item. -- If there was none, set not_found and set -- found_item to the default value. -- -- To choose between various insert/replace procedures, -- see `instructions' in the Indexing clause. ensure then insertion_done: item (key) = new now_present: has (key) found_or_not_found: found or not_found not_found_if_was_not_present: not_found = not (old has (key)) same_count_or_one_more: (count = old count) or (count = old count + 1) found_item_is_old_item: found implies (found_item = old (item (key))) default_value_if_not_found: not_found implies (found_item = computed_default_value) default_property: has_default = ((key = computed_default_key) or ((key /= computed_default_key) and (old has_default))) extend (new: G; key: K) -- Assuming there is no item of key `key', -- insert `new' with `key'. -- Set inserted. -- -- To choose between various insert/replace procedures, -- see `instructions' in the Indexing clause. require not_present: not has (key) ensure inserted: inserted insertion_done: item (key) = new one_more: count = old count + 1 default_property: has_default = ((key = computed_default_key) or (old has_default)) replace (new: G; key: K) -- Replace item at `key', if present, -- with `new'; do not change associated key. -- Set replaced if and only if a replacement has been made -- (i.e. `key' was present); otherwise set not_found. -- Set found_item to the item previously associated -- with `key' (default value if there was none). -- -- To choose between various insert/replace procedures, -- see `instructions' in the Indexing clause. ensure replaced_or_not_found: replaced or not_found insertion_done: replaced implies item (key) = new no_change_if_not_found: not_found implies item (key) = old (item (key)) found_item_is_old_item: found_item = old (item (key)) replace_key (new_key: K; old_key: K) -- If there is an item of key `old_key' and no item of key -- `new_key', replace the former's key by `new_key', -- set replaced, and set found_item to the item -- previously associated with `old_key'. -- Otherwise set not_found or conflict respectively. -- If conflict, set found_item to the item previously -- associated with `new_key'. -- -- To choose between various insert/replace procedures, -- see `instructions' in the Indexing clause. ensure same_count: count = old count replaced_or_conflict_or_not_found: replaced or conflict or not_found old_absent: (replaced and not same_keys (new_key, old_key)) implies (not has (old_key)) new_present: (replaced or conflict) = has (new_key) new_item: replaced implies (item (new_key) = old (item (old_key))) not_found_implies_no_old_key: not_found implies old (not has (old_key)) conflict_iff_already_present: conflict = old (has (new_key)) not_inserted_if_conflict: conflict implies (item (new_key) = old (item (new_key))) merge (other: HASH_TABLE [G, K]) -- Merge `other' into Current. If `other' has some elements -- with same key as in `Current', replace them by one from -- `other'. require other_not_void: other /= Void ensure inserted: other.current_keys.linear_representation.for_all (agent has) feature -- Removal remove (key: K) -- Remove item associated with `key', if present. -- Set removed if and only if an item has been -- removed (i.e. `key' was present); -- if so, set position to index of removed element. -- If not, set not_found. -- Reset found_item to its default value if removed. ensure removed_or_not_found: removed or not_found not_present: not has (key) one_less: found implies (count = old count - 1) default_case: (key = computed_default_key) implies (not has_default) non_default_case: (key /= computed_default_key) implies (has_default = old has_default) prune (v: detachable G) -- Remove first occurrence of `v', if any, -- after cursor position. -- Move cursor to right neighbor. -- (or after if no right neighbor or `v' does not occur) wipe_out -- Reset all items to default values; reset status. ensure then position_equal_to_zero: item_position = 0 count_equal_to_zero: count = 0 has_default_set: not has_default no_status: not special_status feature -- Conversion linear_representation: ARRAYED_LIST [G] -- Representation as a linear structure ensure then result_exists: Result /= Void good_count: Result.count = count feature -- Duplication copy (other: like Current) -- Re-initialize from `other'. invariant keys_not_void: keys /= Void content_not_void: content /= Void keys_enough_capacity: keys.count <= capacity + 1 content_enough_capacity: content.count <= capacity + 1 valid_iteration_position: off or truly_occupied (iteration_position) control_non_negative: control >= 0 special_status: special_status = (conflict or inserted or replaced or removed or found or not_found) count_big_enough: 0 <= count count_small_enough: count <= capacity slot_count_big_enough: 0 <= count note instruction: "[ Several procedures are provided for inserting an item with a given key. Here is how to choose between them: - Use put if you want to do an insertion only if there was no item with the given key, doing nothing otherwise. (You can find out on return if there was one, and what it was.) - Use force if you always want to insert the item; if there was one for the given key it will be removed, (and you can find out on return what it was). - Use extend if you are sure there is no item with the given key, enabling faster insertion (but unpredictable behavior if this assumption is not true). - Use replace if you want to replace an already present item with the given key, and do nothing if there is none. In addition you can use replace_key to change the key of an already present item, identified by its previous key, or do nothing if there is nothing for that previous key. You can find out on return. To find out whether a key appears in the table, use has. To find out the item, if any, associated with a certain key, use item. Both of these routines perform a search. If you need both pieces of information (does a key appear? And, if so, what is the associated item?), you can avoid performing two redundant traversals by using instead the combination of search, found and found_item as follows: your_table.search (your_key) if your_table.found then what_you_where_looking_for := your_table.found_item ... Do whatever is needed to `what_you_were_looking_for' ... else ... No item was present for `your_key' ... end ]" date: "$Date: 2016-03-02 10:03:36 -0800 (Wed, 02 Mar 2016) $" revision: "$Revision: 98555 $" copyright: "Copyright (c) 1984-2016, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class HASH_TABLE -- Generated by ISE Eiffel --
For more details: www.eiffel.com