indexing
	description: "Structures whose items are accessible through keys"
	library: "Gobo Eiffel Structure Library"
	author: "Eric Bezault <ericb@gobo.demon.co.uk>"
	copyright: "Copyright (c) 1997, Eric Bezault"

deferred class interface
	DS_TABLE [G, K]

feature -- Access

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

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

	count: INTEGER
			-- Number of items in structure
			-- (from DS_CONTAINER)
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is current structure equal to other?
			-- (from DS_CONTAINER)
		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

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

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

	valid_key (k: K): BOOLEAN
			-- Is k a valid key?
	
feature -- Element change

	put (v: G; k: K)
			-- Associate v with key k.
		require
			valid_key: valid_key (k)
		ensure
			valid_entry: valid_entry (k);
			inserted: item (k) = v

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

	remove (k: K)
			-- Remove item associated with k.
		require
			valid_entry: valid_entry (k)
		ensure
			one_less: count = old count - 1

	wipe_out
			-- Remove all items from structure.
			-- (from DS_CONTAINER)
		ensure -- from DS_CONTAINER
			wipe_out: is_empty
	
feature -- Transformation

	swap (k, l: K)
			-- Exchange items associated with k and l.
		require
			valid_k: valid_entry (k);
			valid_l: valid_entry (l)
		ensure
			same_count: count = old count;
			new_k: item (k) = old item (l);
			new_l: item (l) = old item (k)
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
		-- from DS_CONTAINER
	positive_count: count >= 0;
	empty_definition: is_empty = (count = 0);

end -- class DS_TABLE