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

	definite_item (key: K): G
			-- Entry of key k.

	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: 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: 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?

	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?

	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_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.
		require else
				True
		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.
		require else
				True
		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: across
					other as other_cursor
				all
					has (other_cursor.key)
				end
	
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.
		require else
				prunable
		ensure then
			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: 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.
	
feature -- Transformation

	correct_mismatch
			-- Attempt to correct object mismatch during retrieve using Mismatch_information.
	
feature -- Inapplicable

	collection_extend (v: G)
			-- Insert a new occurrence of v.
	
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: 2019-06-29 12:33:09 +0000 (Sat, 29 Jun 2019) $"
	revision: "$Revision: 103320 $"
	copyright: "Copyright (c) 1984-2019, 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 EiffelStudio