note
	description: "[
		Maps where key-value pairs can be updated, added and removed.
		Keys are unique with respect to object equality.
		]"
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: map, lock
	manual_inv: true
	false_guards: true

deferred class
	V_TABLE [K -> ANY, V]

inherit
	V_MAP [K, V]

feature -- Search

	item alias "[]" (k: K): V assign force
			-- Value associated with `k'.
		deferred
		end

feature -- Iteration

	new_cursor: V_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
		deferred
		end

feature -- Replacement

	put (v: V; k: K)
			-- Associate `v' with key `k'.
		note
			status: nonvariant
		require
			lock_wrapped: lock.is_wrapped
			k_locked: lock.locked [k]
			has_key: domain_has (k)
			no_iterators: observers.is_empty
		local
			it: V_TABLE_ITERATOR [K, V]
		do
			check inv_only ("locked_non_void", "locked_definition", "lock_non_current", "items_locked", "no_duplicates") end
			check lock.inv_only ("owns_definition", "equivalence_definition") end
			it := at_key (k)
			it.put (v)
			forget_iterator (it)
		ensure
			map_effect: map ~ old map.updated (domain_item (k), v)
			observers_restored: observers ~ old observers
			same_domain: map.domain ~ old map.domain
			modify_model (["map", "observers"], Current)
		end

feature -- Extension

	extend (v: V; k: K)
			-- Extend table with key-value pair <`k', `v'>.
		require
			k_locked: lock.locked [k]
			fresh_key: not domain_has (k)
			lock_wrapped: lock.is_wrapped
			no_iterators: observers.is_empty
		deferred
		ensure
			abstract_effect: domain_has (k)
			map_effect: map ~ old map.updated (k, v)
			modify_model ("map", Current)
		end

	force (v: V; k: K)
			-- Make sure that `k' is associated with `v'.
			-- Add `k' if not already present.
		note
			status: nonvariant
		require
			k_locked: lock.locked [k]
			lock_wrapped: lock.is_wrapped
			no_iterators: observers.is_empty
		local
			it: V_TABLE_ITERATOR [K, V]
		do
			check inv_only ("locked_non_void", "locked_definition", "lock_non_current", "items_locked", "no_duplicates") end
			check lock.inv_only ("owns_definition", "equivalence_definition") end
			it := at_key (k)
			if it.after then
				forget_iterator (it)
				extend (v, k)
			else
				it.put (v)
				forget_iterator (it)
			end
		ensure
			map_effect_has: old domain_has (k) implies map ~ old map.updated (domain_item (k), v)
			map_effect_not_has: not old domain_has (k) implies map ~ old map.updated (k, v)
			observers_restored: observers ~ old observers
			modify_model (["map", "observers"], Current)
		end

feature -- Removal

	remove (k: K)
			-- Remove key `k' and its associated value.
		require
			v_locked: lock.locked [k]
			has_key: domain_has (k)
			lock_wrapped: lock.is_wrapped
			no_iterators: observers.is_empty
		deferred
		ensure
			map_effect: map ~ old map.removed (domain_item (k))
			modify_model ("map", Current)
		end

	wipe_out
			-- Remove all elements.
		require
			no_iterators: observers.is_empty
		deferred
		ensure
			map_effect: map.is_empty
			modify_model ("map", Current)
		end

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