note
	description: "[
			Hash tables with hash function provided by HASHABLE and object equality.
			Implementation uses chaining.
			Search, extension and removal are amortized constant time.
		]"
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: map, lock
	manual_inv: true
	false_guards: true

frozen class
	V_HASH_TABLE [K -> V_HASHABLE, V]

inherit
	V_TABLE [K, V]
		redefine
			is_equal_,
			map,
			lock,
			forget_iterator
		end

create
	make

feature {NONE} -- Initialization

	make (l: V_HASH_LOCK [K])
			-- Create an empty table with lock `l'.
		note
			status: creator
			explicit: wrapping
		require
			l_wrapped: l.is_wrapped
		do
			lock := l
			set_subjects (create {MML_SET [ANY]}.singleton (l))
			l.add_client (Current)
			make_empty_buckets (default_capacity)
		ensure then
			map_empty: map.is_empty
			lock_set: lock = l
			lock_observers_effect: l.observers = old l.observers & Current
			is_empty
			observers_empty: observers.is_empty
			modify (Current)
			modify_model ("observers", l)
		end

feature -- Initialization

	copy_ (other: V_HASH_TABLE [K, V])
			-- Initialize by copying all the items of `other'.
		note
			explicit: wrapping
		require
			lock_wrapped: lock.is_wrapped
			same_lock: lock = other.lock
			no_iterators: observers.is_empty
		local
			it: V_HASH_TABLE_ITERATOR [K, V]
		do
			if other /= Current then
				unwrap
				check other.inv_only ("items_locked", "locked_definition", "buckets_owned", "buckets_count", "buckets_non_empty", "lists_definition", "no_duplicates") end
				make_empty_buckets (other.capacity)

				from
					it := other.new_cursor
				invariant
					is_wrapped
					other.is_wrapped
					it.is_wrapped
					lock.inv_only ("locked_non_void", "owns_definition", "equivalence_definition")
					inv_only ("locked_non_void", "locked_definition")
					1 <= it.index_ and it.index_ <= it.sequence.count + 1
					∀ i: 1 |..| it.sequence.count ¦ map.domain [it.sequence [i]] = (i < it.index_)
					map.domain <= other.map.domain
					map = other.map | map.domain
					∀ x: other.map.domain - map.domain ¦ not domain_has (x)

					modify_model ("map", Current)
					modify_model ("index_", it)
				until
					it.after
				loop
					use_definition (it.value_sequence_from (it.sequence, other.map))
					simple_extend (it.item, it.key)
					it.lemma_sequence_no_duplicates
					it.forth
				variant
					it.sequence.count - it.index_
				end
				check map.domain = other.map.domain end
				other.forget_iterator (it)
			end
		ensure
			map_effect: map ~ old other.map
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("map", Current)
			modify_model ("observers", [Current, other])
		end

feature -- Measurement

	count: INTEGER
			-- Number of elements.
		do
			check inv_only ("count_definition", "bag_definition") end
			use_definition (bag_from (map))
			Result := count_
		end

feature -- Search

	has_key (k: K): BOOLEAN
			-- Is key `k' contained?
			-- (Uses object equality.)
		do
			Result := cell_for_key (k) /= Void
		end

	key (k: K): K
			-- Element of `map.domain' equivalent to `v' according to object equality.
		do
			if attached cell_for_key (k) as c then
				Result := c.item.left
			else
				check
					from_precondition: False
				then
				end
			end
		end

	item alias "[]" (k: K): V assign force
			-- Value associated with `k'.
		do
			if attached cell_for_key (k) as c then
				Result := c.item.right
			else
				check
					from_precondition: False
				then
				end
			end
		end

feature -- Iteration

	new_cursor: V_HASH_TABLE_ITERATOR [K, V]
			-- New iterator pointing to a position in the map, from which it can traverse all elements by going `forth'.
		note
			status: impure
		do
			create Result.make (Current)
			Result.start
		end

	at_key (k: K): V_HASH_TABLE_ITERATOR [K, V]
			-- New iterator pointing to a position with key `k'.
			-- If key does not exist, iterator is off.
		note
			status: impure
		do
			create Result.make (Current)
			Result.search_key (k)
		end

feature -- Comparison

	is_equal_ (other: like Current): BOOLEAN
			-- Is the abstract state of Current equal to that of `other'?
		local
			i: INTEGER
			l: V_LINKED_LIST [MML_PAIR [K, V]]
		do
			check inv_only ("count_definition", "subjects_definition") end
			check other.inv_only ("count_definition", "subjects_definition") end
			if count_ = other.count_ then
				from
					Result := True
					i := 1
				invariant
					inv
					1 <= i and i <= lists.count + 1
					Result implies ∀ j: 1 |..| (i - 1) ¦
							∀ k: 1 |..| lists [j].sequence.count ¦
								other.map.domain [lists [j].sequence [k].left] and then
								other.map [lists [j].sequence [k].left] = lists [j].sequence [k].right
					not Result implies i > 1 and then not
							(∀ k: 1 |..| lists [i - 1].sequence.count ¦
									other.map.domain [lists [i - 1].sequence [k].left] and then
									other.map [lists [i - 1].sequence [k].left] = lists [i - 1].sequence [k].right)
				until
					i > buckets.count or not Result
				loop
					l := buckets [i]
					Result := has_list (l, other)
					i := i + 1
				variant
					lists.count - i
				end
			end
			if Result then
				other.map.domain.lemma_subset (map.domain)
			end
		end

feature -- Extension

	extend (v: V; k: K)
			-- Extend table with key-value pair <`k', `v'>.
		note
			explicit: wrapping
		do
			check lock.inv_only ("owns_definition") end
			check inv_only ("items_locked", "locked_definition") end
			auto_resize (count_ + 1)
			simple_extend (v, k)
		end

feature -- Removal

	remove (k: K)
			-- Remove key `k' and its associated value.
		note
			explicit: wrapping
		local
			idx, i_: INTEGER
		do
			unwrap
			check lock.inv_only ("owns_definition", "equivalence_definition", "hash_definition") end
			idx := index (k)
			i_ := remove_equal (buckets [idx], k)
			count_ := count_ - 1
			k.lemma_transitive (domain_item (k), create {MML_SET [K]}.singleton (buckets_ [idx] [i_]))
			map := map.removed (buckets_ [idx] [i_])
			buckets_ := buckets_.replaced_at (idx, buckets_ [idx].removed_at (i_))
			wrap
			auto_resize (count_)
		end

	wipe_out
			-- Remove all elements.
		note
			explicit: wrapping
		do
			unwrap
			make_empty_buckets (default_capacity)
		end

feature {NONE} -- Performance parameters

	default_capacity: INTEGER = 16
			-- Default size of `buckets'.

	target_load_factor: INTEGER = 75
			-- Approximate percentage of elements per bucket that bucket array has after automatic resizing.

	growth_rate: INTEGER = 2
			-- Rate by which bucket array grows and shrinks.

feature {V_CONTAINER, V_ITERATOR, V_LOCK} -- Implementation

	buckets: V_ARRAY [V_LINKED_LIST [MML_PAIR [K, V]]]
			-- Element storage.
		attribute
		end

	count_: INTEGER
			-- Number of elements.
		attribute
		end

	capacity: INTEGER
			-- Bucket array size.
		require
			buckets_closed: buckets.closed
		do
			Result := buckets.count
		ensure
			definition: Result = buckets.sequence.count
		end

	bucket_index (hc, n: INTEGER): INTEGER
			-- The bucket an item with hash code `hc' belongs,
			-- if there are `n' buckets in total.
		note
			explicit: contracts
		require
			reads ([])
			n_positive: n > 0
			hc_non_negative: 0 <= hc
		do
			Result := hc \\ n + 1
		ensure
			in_bounds: 1 <= Result and Result <= n
		end

	index (k: K): INTEGER
			-- Index of `k' into in `buckets'.
		require
			k_closed: k.closed
			buckets_closed: buckets.closed
			positive_capacity: buckets.sequence.count > 0
		do
			check k.inv end
			Result := bucket_index (k.hash_code, capacity)
		ensure
			definition: Result = bucket_index (k.hash_code_, buckets.sequence.count)
		end

	cell_for_key (k: K): detachable V_LINKABLE [MML_PAIR [K, V]]
			-- Cell of one of the buckets where the key is equal to `k' according to object equality.
			-- Void if the list has no such cell.
		require
			closed: closed
			k_closed_with_subjects: k.is_closed_with_subjects
			lock_closed: lock.closed
		do
			check inv_only ("locked_definition", "owns_definition", "buckets_non_empty", "buckets_lower", "buckets_count",
						"lists_definition", "lists_counts", "buckets_content", "domain_not_too_small", "map_implementation",
						"items_locked", "no_duplicates", "valid_buckets") end
			check lock.inv_only ("owns_definition", "equivalence_definition", "hash_domain_definition", "hash_definition") end
			Result := cell_equal (buckets [index (k)], k)
			check ∀ j: 1 |..| buckets_ [index (k)].count ¦ buckets_ [index (k)] [j] = lists [index (k)].sequence [j].left end
			if domain_has (k) and then attached Result then
				k.lemma_transitive (Result.item.left, create {MML_SET [K]}.singleton (domain_item (k)))
			end
		ensure
			definition_not_found: not domain_has (k) implies Result = Void
			definition_found: domain_has (k) implies Result /= Void and then
				Result.item.left = domain_item (k) and then map [Result.item.left] = Result.item.right
		end

	cell_equal (list: V_LINKED_LIST [MML_PAIR [K, V]]; k: K): detachable V_LINKABLE [MML_PAIR [K, V]]
			-- Cell of `list' where the key is equal to `k' according to object equality.
			-- Void if the list has no such cell.
		require
			list_closed: list.closed
			k_closed_with_subjects: k.is_closed_with_subjects
			list_keys_closed_with_subjects: ∀ i: 1 |..| list.sequence.count ¦ list.sequence [i].left.is_closed_with_subjects
		do
			check list.inv_only ("cells_domain", "cells_exist", "cells_linked", "cells_first", "first_cell_empty", "sequence_implementation") end
			if not list.is_empty then
				Result := cell_before (list, k)
				if Result = Void then
					Result := list.first_cell
				else
					Result := Result.right
				end
			end
		ensure
			definition_not_found: Result = Void implies
				∀ i: 1 |..| list.sequence.count ¦ not k.is_model_equal (list.sequence [i].left)
			definition_found: Result /= Void implies list.cells.has (Result) and list.sequence.has (Result.item) and k.is_model_equal (Result.item.left)
		end

	cell_before (list: V_LINKED_LIST [MML_PAIR [K, V]]; k: K): detachable V_LINKABLE [MML_PAIR [K, V]]
			-- Cell of `list' to the left of the cell where the key is equal to `k' according to object equality.
			-- Void if the first list element is equal to `k'; last cell if no list element is equal to `k'.
		require
			list_closed: list.closed
			not_empty: not list.sequence.is_empty
			k_closed_with_subjects: k.is_closed_with_subjects
			list_keys_closed_with_subjects: ∀ i: 1 |..| list.sequence.count ¦ list.sequence [i].left.is_closed_with_subjects
		local
			j_: INTEGER
		do
			check list.inv_only ("cells_domain", "cells_exist", "cells_first", "first_cell_empty", "sequence_implementation") end
			if attached list.first_cell as c then
				if not k.is_equal_ (c.item.left) then
					from
						j_ := 1
						Result := c
					invariant
						list.inv_only ("cells_domain", "cells_exist", "cells_linked", "cells_first", "cells_last", "first_cell_empty", "sequence_implementation")
						1 <= j_ and j_ <= list.sequence.count
						Result = list.cells [j_]
						list.sequence.domain [j_ + 1] implies Result.right = list.cells [j_ + 1]
						∀ l: 1 |..| j_ ¦ not k.is_model_equal (list.sequence [l].left)
					until
						attached Result.right as r implies k.is_equal_ (r.item.left)
					loop
						Result := r
						j_ := j_ + 1
					variant
						list.sequence.count - j_
					end
				end
			else
				check from_precondition: False then end
			end
		ensure
			definition_not_found: Result /= Void and then Result.right = Void implies
				∀ i: 1 |..| list.sequence.count ¦ not k.is_model_equal (list.sequence [i].left)
			definition_found_first: Result = Void implies k.is_model_equal (list.sequence.first.left)
			definition_found_later: Result /= Void and then attached Result.right as r implies
				list.cells.has (Result) and list.cells.has (r) and k.is_model_equal (r.item.left)
		end

	make_empty_buckets (n: INTEGER)
			-- Create an empty set with `buckets' of size `n'.
		require
			open: is_open
			n_positive: n > 0
			no_iterators: observers.is_empty
			inv_only ("lock_exists", "subjects_definition", "A2")
		local
			i: INTEGER
		do
			create buckets.make (1, n)
			check buckets.inv_only ("owns_definition"); buckets.area.inv_only ("default_owns") end
			from
				i := 1
			invariant
				1 <= i and i <= n + 1
				buckets.is_wrapped
				buckets.sequence.count = n
				∀ j: 1 |..| (i - 1) ¦
						buckets.sequence [j].is_wrapped and
						buckets.sequence [j].is_fresh and
						buckets.sequence [j].sequence.is_empty and
						buckets.sequence [j].observers.is_empty
				∀ k: 1 |..| (i - 1) ¦ ∀ l: 1 |..| (i - 1) ¦
							k /= l implies buckets.sequence [k] /= buckets.sequence [l]
				modify_model ("sequence", buckets)
			until
				i > n
			loop
				buckets [i] := create {V_LINKED_LIST [MML_PAIR [K, V]]}
				i := i + 1
			end

			count_ := 0
			create map
			create buckets_.constant ({MML_SEQUENCE [K]}.empty_sequence, buckets.sequence.count)
			check map.domain.is_empty end
			wrap
		ensure
			wrapped: is_wrapped
			map_effect: map.is_empty
			locked_effect: locked.is_empty
			capacity_effect: lists.count = n
			modify_field (["buckets", "count_", "map", "lists", "buckets_", "locked", "bag", "owns", "closed"], Current)
		end

	remove_at (it: V_HASH_TABLE_ITERATOR [K, V])
			-- Remove element to which `it' points.
		require
			wrapped: is_wrapped
			it_open: it.is_open
			valid_target: it.target = Current
			lock_wrapped: lock.is_wrapped
			only_iterator: observers ~ create {MML_SET [ANY]}.singleton (it)
			1 <= it.bucket_index and it.bucket_index <= lists.count
			list_iterator_wrapped: it.list_iterator.is_wrapped
			it.inv_only ("target_which_bucket", "list_iterator_not_off")
		local
			idx_, i_: INTEGER
		do
			unwrap
			idx_ := it.bucket_index
			i_ := it.list_iterator.index_
			check it.list_iterator.inv_only ("subjects_definition", "A2", "sequence_definition") end

			check lists [idx_].observers ~ create {MML_SET [ANY]}.singleton (it.list_iterator) end
			it.list_iterator.remove

			count_ := count_ - 1
			map := map.removed (buckets_ [idx_] [i_])
			buckets_ := buckets_.replaced_at (idx_, buckets_ [idx_].removed_at (i_))
			wrap
		ensure
			wrapped: is_wrapped
			list_iterator_wrapped: it.list_iterator.is_wrapped
			map_effect: map = old (map.removed (buckets_ [it.bucket_index] [it.list_iterator.index_]))
			same_index: it.list_iterator.index_ = old it.list_iterator.index_
			same_lists: lists = old lists
			buckets_effect: buckets_ = old (buckets_.replaced_at (it.bucket_index, buckets_ [it.bucket_index].removed_at (it.list_iterator.index_)))
			modify_model ("map", Current)
			modify_model (["index_", "sequence"], it.list_iterator)
		end

	remove_equal (list: V_LINKED_LIST [MML_PAIR [K, V]]; k: K): INTEGER
			-- Remove an element where key is equal to `k' from `list'; return the index of the element in the prestate.
		note
			status: impure
		require
			list_wrapped: list.is_wrapped
			not_empty: not list.sequence.is_empty
			lock_wrapped: lock.is_wrapped
			key_locked: lock.locked [k]
			list_keys_owned: ∀ i: 1 |..| list.sequence.count ¦ lock.locked [list.sequence [i].left]
			has_equal: ∃ i: 1 |..| list.sequence.count ¦ k.is_model_equal (list.sequence [i].left)
			no_observers: list.observers.is_empty
		local
			c: V_LINKABLE [MML_PAIR [K, V]]
		do
			check lock.inv_only ("owns_definition") end
			c := cell_before (list, k)
			if c = Void then
				Result := 1
				list.remove_front
			else
				Result := list.cells.index_of (c) + 1
				check list.inv_only ("cells_domain", "cells_exist", "cells_linked", "cells_last", "sequence_implementation") end
				list.remove_after (c, Result - 1)
			end
		ensure
			list_wrapped: list.is_wrapped
			found: k.is_model_equal ((old list.sequence) [Result].left)
			removed: list.sequence ~ old list.sequence.removed_at (Result)
			modify_model ("sequence", list)
		end

	replace_at (it: V_HASH_TABLE_ITERATOR [K, V]; v: V)
			-- Replace the value at the element to which `it' points.
		require
			wrapped: is_wrapped
			it_open: it.is_open
			valid_target: it.target = Current
			lock_wrapped: lock.is_wrapped
			only_iterator: observers ~ create {MML_SET [ANY]}.singleton (it)
			1 <= it.bucket_index and it.bucket_index <= lists.count
			list_iterator_wrapped: it.list_iterator.is_wrapped
			it.inv_only ("target_which_bucket", "list_iterator_not_off")
		local
			idx_, i_: INTEGER
			x: K
		do
			unwrap
			idx_ := it.bucket_index
			i_ := it.list_iterator.index_
			check it.list_iterator.inv_only ("subjects_definition", "A2", "sequence_definition") end
			x := it.list_iterator.item.left
			check x = buckets_ [idx_] [i_] end

			check lists [idx_].observers ~ create {MML_SET [ANY]}.singleton (it.list_iterator) end
			it.list_iterator.put (create {MML_PAIR [K, V]}.make (x, v))

			map := map.updated (x, v)
			check map.domain = map.domain.old_ end
			wrap
		ensure
			wrapped: is_wrapped
			list_iterator_wrapped: it.list_iterator.is_wrapped
			map_effect: map = old (map.updated (buckets_ [it.bucket_index] [it.list_iterator.index_], v))
			same_index: it.list_iterator.index_ = old it.list_iterator.index_
			modify_field (["map", "bag", "closed"], Current)
			modify_model (["sequence", "box"], it.list_iterator)
		end

	simple_extend (v: V; k: K)
			-- Extend table with key-value pair <`k', `v'> without resizing the buckets.
		require
			wrapped: is_wrapped
			k_locked: lock.locked [k]
			fresh_key: not domain_has (k)
			lock_wrapped: lock.is_wrapped
			no_iterators: observers.is_empty
		local
			idx: INTEGER
			list: V_LINKED_LIST [MML_PAIR [K, V]]
		do
			unwrap
			check lock.inv_only ("owns_definition", "equivalence_definition", "hash_domain_definition", "hash_definition") end
			idx := index (k)
			list := buckets [idx]
			list.extend_back (create {MML_PAIR [K, V]}.make (k, v))
			buckets_ := buckets_.replaced_at (idx, buckets_ [idx] & k)
			map := map.updated (k, v)
			count_ := count_ + 1
			wrap
		ensure
			wrapped: is_wrapped
			map_effect: map ~ old map.updated (k, v)
			map_domain_effect: map.domain ~ old map.domain & k
			capacity_unchanged: lists.count = old lists.count
			modify_model ("map", Current)
		end

	auto_resize (new_count: INTEGER)
			-- Resize `buckets' to an optimal size for `new_count'.
		require
			wrapped: is_wrapped
			no_iterators: observers.is_empty
			lock_wrapped: lock.is_wrapped
		do
			check inv end
			if new_count * target_load_factor // 100 > growth_rate * capacity then
				resize (capacity * growth_rate)
			elseif capacity > default_capacity and new_count * target_load_factor // 100 < capacity // growth_rate then
				resize (capacity // growth_rate)
			end
			check inv_only ("locked_definition") end
		ensure
			wrapped: is_wrapped
			map_unchanged: map ~ old map
			locked_unchanged: locked ~ old locked
			modify_model ("map", Current)
		end

	resize (c: INTEGER)
			-- Resize `buckets' to `c'.
		require
			wrapped: is_wrapped
			c_positive: c > 0
			no_iterators: observers.is_empty
			lock_wrapped: lock.is_wrapped
		local
			i: INTEGER
			b: like buckets
			it: V_LINKED_LIST_ITERATOR [MML_PAIR [K, V]]
		do
			b := buckets
			check lock.inv_only ("owns_definition") end
			unwrap
			make_empty_buckets (c)
			from
				i := 1
			invariant
				is_wrapped
				∀ j: 1 |..| b.sequence.count ¦ b.sequence [j].is_wrapped
				lists.count = c
				inv_only ("locked_definition")
				locked <= locked.old_
				∀ x: locked ¦ map [x] = map.old_ [x]
				∀ k: 1 |..| buckets_.old_.count ¦ ∀ l: 1 |..| buckets_.old_ [k].count ¦
							map.domain [buckets_.old_ [k] [l]] = (k < i)
				modify_model ("map", Current)
				modify_field (["observers", "closed"], lists.old_.range)
			until
				i > b.count
			loop
				from
					it := b [i].new_cursor
				invariant
					is_wrapped
					it.is_wrapped
					inv_only ("locked_definition")
					1 <= it.index_ and it.index_ <= b.sequence [i].count + 1
					lists.count = c
					∀ k: 1 |..| buckets_.old_.count ¦ ∀ l: 1 |..| buckets_.old_ [k].count ¦
								map.domain [buckets_.old_ [k] [l]] = (k < i or (k = i and l < it.index_))
					locked <= locked.old_
					∀ x: locked ¦ map [x] = map.old_ [x]
					modify_model ("map", Current)
					modify_model ("index_", it)
				until
					it.after
				loop
					check it.inv_only ("sequence_definition") end
					check lock.inv_only ("equivalence_definition") end

					simple_extend (it.item.right, it.item.left)
					it.forth
				variant
					lists.old_ [i].count - it.index_
				end
				i := i + 1
			end
		ensure
			wrapped: is_wrapped
			capacity_effect: lists.count = c
			map_unchanged: map = old map
			modify_model ("map", Current)
		end

	has_list (list: V_LINKED_LIST [MML_PAIR [K, V]]; other: like Current): BOOLEAN
			-- Does `other' contain all elements stored in the bucket `list'?
		require
			list_closed: list.closed
			other_closed: other.closed
			lock_closed: lock.closed
			other_lock_closed: other.lock.closed
			list_items_locked: ∀ j: 1 |..| list.sequence.count ¦ lock.locked [list.sequence [j].left]
		local
			c: V_LINKABLE [MML_PAIR [K, V]]
			i_: INTEGER
		do
			check list.inv_only ("cells_domain", "first_cell_empty", "cells_first", "cells_last", "cells_exist", "cells_linked", "sequence_implementation") end
			check lock.inv_only ("owns_definition") end
			check other.lock.inv_only ("owns_definition") end
			from
				Result := True
				c := list.first_cell
				i_ := 1
			invariant
				other.inv_only ("items_locked", "locked_definition")
				1 <= i_ and i_ <= list.sequence.count + 1
				i_ <= list.sequence.count implies c = list.cells [i_]
				i_ = list.sequence.count + 1 implies c = Void
				Result implies ∀ j: 1 |..| (i_ - 1) ¦
						other.map.domain [list.sequence [j].left] and then other.map [list.sequence [j].left] = list.sequence [j].right
				not Result implies i_ > 1 and then
					(not other.map.domain [list.sequence [i_ - 1].left] or else other.map [list.sequence [i_ - 1].left] /= list.sequence [i_ - 1].right)
			until
				c = Void or not Result
			loop
				Result := other.has_key (c.item.left) and then
					(other.key (c.item.left) = c.item.left and other.item (c.item.left) = c.item.right)
				if other.domain_has (c.item.left) and not Result then
					check other.inv_only ("no_duplicates") end
					check other.lock.inv_only ("equivalence_definition") end
					c.item.left.lemma_transitive (other.key (c.item.left), other.map.domain / other.key (c.item.left))
				end
				c := c.right
				i_ := i_ + 1
			variant
				list.sequence.count - i_
			end
		ensure
			definition: Result = ∀ j: 1 |..| list.sequence.count ¦
						other.map.domain [list.sequence [j].left] and then other.map [list.sequence [j].left] = list.sequence [j].right
		end

feature -- Specification

	map: MML_MAP [K, V]
			-- Map of keys to values.
		note
			status: ghost
		attribute
			check is_executable: False then end
		end

	buckets_: MML_SEQUENCE [MML_SEQUENCE [K]]
			-- Abstract element storage.
		note
			status: ghost
		attribute
			check is_executable: False then end
		end

	lock: V_HASH_LOCK [K]
			-- Helper object for keeping items consistent.
		note
			status: ghost
		attribute
			check is_executable: False then end
		end

	forget_iterator (it: V_ITERATOR [V])
			-- Remove `it' from `observers'.
		note
			status: ghost
			explicit: contracts, wrapping
		local
			i, j: INTEGER
		do
			check it.inv_only ("subjects_definition", "A2") end
			unwrap
			check attached {V_HASH_TABLE_ITERATOR [K, V]} it as htit then
				check htit.inv_only ("target_is_bucket", "owns_definition") end
				check htit.list_iterator.inv_only ("subjects_definition", "default_owns", "A2") end
				i := htit.bucket_index
				htit.unwrap
				set_observers (observers / htit)

				if lists.domain [i] then
					lemma_lists_domain (i)
					lists [i].forget_iterator (htit.list_iterator)
				else
					htit.list_iterator.unwrap
				end

				from
					j := 1
				invariant
					1 <= j and j <= lists.count + 1
					htit.list_iterator.is_open
					∀ k: 1 |..| lists.count ¦ lists [k].is_wrapped and then
							lists [k].observers = if k >= j and k /= i
								then lists [k].observers.old_
								else lists [k].observers.old_ / htit.list_iterator end
					inv_only ("A2", "items_locked", "no_duplicates", "valid_buckets")
					modify_field (["observers", "closed"], lists.range)
				until
					j > lists.count
				loop
					if j /= i then
						lists [j].unwrap
						lists [j].observers := lists [j].observers / htit.list_iterator
						lists [j].wrap
					end
					j := j + 1
				end
			end
			wrap
		end

feature {V_CONTAINER, V_ITERATOR, V_LOCK} -- Specification

	lists: MML_SEQUENCE [V_LINKED_LIST [MML_PAIR [K, V]]]
			-- Cache of `buckets.sequence' (required in the invariant of the iterator).
		note
			status: ghost
		attribute
			check is_executable: False then end
		end

	lemma_lists_domain (i: INTEGER)
			-- `lock' is not in the ownership domain of any of the `lists'.
		note
			status: lemma
		require
			1 <= i and i <= lists.count
			lists [i].closed
		do
			check lists [i].inv_only ("owns_definition") end
			check ∀ j: 1 |..| lists [i].cells.count ¦ lists [i].cells [j].inv_only ("default_owns") end
			check not lists [i].transitive_owns [lock] end
		ensure
			not lists [i].ownership_domain [lock]
		end

	lemma_domain
			-- `lock' is not in the ownership domain of `Current'.
		note
			status: lemma
		require
			closed
		do
			check inv_only ("owns_definition") end
			check buckets.inv_only ("owns_definition"); buckets.area.inv_only ("default_owns") end

			check ∀ i: 1 |..| lists.count ¦ lists [i].inv_only ("owns_definition") end
			check ∀ i: 1 |..| lists.count ¦ ∀ j: 1 |..| lists [i].cells.count ¦ lists [i].cells [j].inv_only ("default_owns") end
			check ∀ i: 1 |..| lists.count ¦ not lists [i].transitive_owns [lock] end
			check not transitive_owns [lock] end
		ensure
			not ownership_domain [lock]
		end

invariant
		-- Abstract state:
	buckets_non_empty: not buckets_.is_empty
	valid_buckets: ∀ x: map.domain ¦ lock.hash.domain [x] and then lock.hash [x] >= 0 and then
			buckets_ [bucket_index (lock.hash [x], buckets_.count)].has (x)
	domain_not_too_small: ∀ i: 1 |..| buckets_.count ¦
			∀ j: 1 |..| buckets_ [i].count ¦ map.domain [buckets_ [i] [j]]
	no_precise_duplicates: ∀ i: 1 |..| buckets_.count ¦ -- ToDo: within is enough?
			∀ j: 1 |..| buckets_.count ¦
				∀ k: 1 |..| buckets_ [i].count ¦
					∀ l: 1 |..| buckets_ [j].count ¦
						i /= j or k /= l implies buckets_ [i] [k] /= buckets_ [j] [l]
		-- Concrete state:
	count_definition: count_ = map.count
	buckets_exist: buckets /= Void
	buckets_owned: owns [buckets]
	buckets_lower: buckets.lower_ = 1
	lists_definition: lists = buckets.sequence
	all_lists_exist: lists.non_void
	owns_definition: owns = create {MML_SET [ANY]}.singleton (buckets) + lists.range
	buckets_count: buckets_.count = lists.count
	lists_distinct: lists.no_duplicates
	lists_counts: ∀ i: 1 |..| buckets_.count ¦ lists [i].sequence.count = buckets_ [i].count
	buckets_content: ∀ i: 1 |..| buckets_.count ¦ ∀ j: 1 |..| buckets_ [i].count ¦ buckets_ [i] [j] = lists [i].sequence [j].left
	map_implementation: ∀ i: 1 |..| buckets_.count ¦ ∀ j: 1 |..| buckets_ [i].count ¦
				map [buckets_ [i] [j]] = lists [i].sequence [j].right
		-- Iterators:
	array_observers: buckets.observers.is_empty
	iterators_type: ∀ o: observers ¦ attached {V_HASH_TABLE_ITERATOR [K, V]} o
	list_observers_same: ∀ i: 1 |..| lists.count ¦ ∀ j: 1 |..| lists.count ¦ lists [i].observers = lists [j].observers
	list_observers_count: ∀ i: 1 |..| lists.count ¦ lists [i].observers.count <= observers.count

note
	copyright: "Copyright (c) 1984-2021, 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