indexing
	description: "Hash tables, implemented with arrays"
	note: "To avoid performance degradation, make sure that `count <= capacity * 2 // 3%'"
	library: "Gobo Eiffel Structure Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

class interface
	DS_HASH_TABLE [G, K -> HASHABLE]

create 

	make (n: INTEGER)
		require
			positive_n: n >= 0
		ensure
			empty: is_empty;
			capacity_set: capacity = n

	make_equal (n: INTEGER)
		require
			positive_n: n >= 0
		ensure
			empty: is_empty;
			capacity_set: capacity = n

feature -- Access

	first: G
			-- First item in hash table
		require -- from DS_LINEAR
			not_empty: not is_empty
		ensure -- from DS_LINEAR
			has_first: has_item (Result)

	item (k: K): G
			-- Item associated with k
			-- Was declared in DS_HASH_TABLE as synonym of @ and item.
		require -- from DS_TABLE
			valid_entry: has (k)

	last: G
			-- Last item in hash table
		require -- from DS_BILINEAR
			not_empty: not is_empty
		ensure -- from DS_BILINEAR
			has_last: has_item (Result)

	new_cursor: DS_HASH_TABLE_CURSOR [G, K]
			-- New cursor for traversal
		ensure -- from DS_TRAVERSABLE
			cursor_not_void: Result /= void;
			valid_cursor: valid_cursor (Result)

	searcher: DS_HASH_TABLE_SEARCHER [G, K]
			-- Hash table searcher

	infix "@" (k: K): G
			-- Item associated with k
			-- Was declared in DS_HASH_TABLE as synonym of @ and item.
		require -- from DS_TABLE
			valid_entry: has (k)
	
feature -- Measurement

	capacity: INTEGER
			-- Maximum number of items in hash table

	count: INTEGER
			-- Number of items in hash table

	occurrences (v: G): INTEGER
			-- Number of times v appears in structure
			-- (Use searcher's comparison criterion.)
			-- (from DS_SEARCHABLE)
		ensure -- from DS_SEARCHABLE
			positive: Result >= 0;
			has: has_item (v) implies Result >= 1
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is hash table equal to other?
		require -- from GENERAL
			other_not_void: other /= void
		ensure -- from GENERAL
			symmetric: Result implies other.is_equal (Current);
			consistent: standard_is_equal (other) implies Result
		ensure then -- from DS_CONTAINER
			same_count: Result implies count = other.count
	
feature -- Status report

	has_item (v: G): BOOLEAN
			-- Does structure incluse v?
			-- (Use searcher's comparison criterion.)
			-- (from DS_SEARCHABLE)
		ensure -- from DS_SEARCHABLE
			not_empty: Result implies not is_empty

	has (k: K): BOOLEAN
			-- Is there an item associated with k?
		ensure -- from DS_TABLE
			valid_key: Result implies valid_key (k)

	is_empty: BOOLEAN
			-- Is structure empty?
			-- (from DS_CONTAINER)

	is_full: BOOLEAN
			-- Is structure full?
			-- (from DS_RESIZABLE)

	valid_cursor (a_cursor: like new_cursor): BOOLEAN
			-- Is a_cursor a valid cursor?
			-- (A cursor might become invalid if structure
			-- has been modified during traversal.)
			-- (from DS_TRAVERSABLE)
		require -- from DS_TRAVERSABLE
			a_cursor_not_void: a_cursor /= void
		ensure -- from DS_TRAVERSABLE
			is_valid: Result implies a_cursor.is_valid

	valid_key (k: K): BOOLEAN
			-- Is k a valid key?
		ensure then
			key_not_void: Result implies k /= void
	
feature -- Element change

	force (v: G; k: K)
			-- Associate v with key k.
			-- Resize hash table if necessary.
		require -- from DS_TABLE
			valid_key: valid_key (k)
		ensure -- from DS_TABLE
			valid_entry: has (k);
			inserted: item (k) = v
		ensure then
			one_more: (not old has (k)) implies (count = old count + 1)

	put (v: G; k: K)
			-- Associate v with key k.
		require
			not_full: not is_full;
			valid_key: valid_key (k)
		ensure
			one_more: (not old has (k)) implies (count = old count + 1);
			inserted: has (k) and then item (k) = v

	replace (v: G; k: K)
			-- Replace item associated with k by v.
		require -- from DS_TABLE
			valid_entry: has (k)
		ensure -- from DS_TABLE
			replaced: item (k) = v;
			same_count: count = old count
	
feature -- Removal

	remove (k: K)
			-- Remove item associated with k.
		require -- from DS_TABLE
			valid_entry: has (k)
		ensure -- from DS_TABLE
			one_less: count = old count - 1
		ensure then
			removed: not has (k)

	wipe_out
			-- Remove all items.
		ensure -- from DS_CONTAINER
			wipe_out: is_empty
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize hash table so that it can contain
			-- at least n items. Do not lose any item.
		require -- from DS_RESIZABLE
			n_large_enough: n >= capacity
		ensure -- from DS_RESIZABLE
			capacity_set: capacity = n
	
feature -- Transformation

	swap (k, l: K)
			-- Exchange items associated with k and l.
			-- (from DS_TABLE)
		require -- from DS_TABLE
			valid_k: has (k);
			valid_l: has (l)
		ensure -- from DS_TABLE
			same_count: count = old count;
			new_k: item (k) = old item (l);
			new_l: item (l) = old item (k)
	
feature -- Duplication

	copy (other: like Current)
			-- Copy other to current hash table.
		require -- from GENERAL
			other_not_void: other /= void;
			type_identity: same_type (other)
		ensure -- from GENERAL
			is_equal: is_equal (other)
	
feature -- Setting

	set_searcher (a_searcher: like searcher)
			-- Set searcher to a_searcher.
			-- (from DS_SEARCHABLE)
		require -- from DS_SEARCHABLE
			a_searcher_not_void: a_searcher /= void
		ensure -- from DS_SEARCHABLE
			searcher_set: searcher = a_searcher
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	storage_not_void: storage /= void;
	dead_cell: dead_cell /= void;
	valid_position: storage.valid_index (position);
	capacity_definition: capacity = storage.count - 1;
	lower_definition: storage.lower = 0;
		-- from DS_CONTAINER
	positive_count: count >= 0;
	empty_definition: is_empty = (count = 0);
		-- from DS_SEARCHABLE
	searcher_not_void: searcher /= void;
		-- from DS_RESIZABLE
	count_constraint: count <= capacity;
	full_definition: is_full = (count = capacity);

end -- class DS_HASH_TABLE