    indexing
    	description: "[
    		Translations of class names between a storing and a retrieving
    		system. Values in this table are names of classes in the retrieving
    		system, indexed by names of generating classes in the storing
    		system (i.e. with no generic arguments). Values may have generic
    		arguments (e.g. "MY_CLASS [DOUBLE]"), thus allowing a very simple
    		conversion of a non-generic class into a generic class. The
    		presence of entries in this table affects all retrieve operations
    		for objects stored using `independent_store'.
    	]"
    	legal: "See notice at end of class."
    	date: "$Date: 2006-06-24 12:08:58 -0700 (Sat, 24 Jun 2006) $"
    	revision: "$Revision: 60288 $"
    	status: "See notice at end of class."

    class interface
    	CLASS_NAME_TRANSLATIONS

    create
    	default_create
    			-- Make table with current translations

    feature -- Initialization

    	accommodate (n: INTEGER_32)
    			-- Reallocate table with enough space for `n' items;
    			-- keep all current items.
    			-- (from HASH_TABLE)
    		require -- from HASH_TABLE
    			n >= 0
    		ensure -- from HASH_TABLE
    			count_not_changed: count = old count
    			slot_count_same_as_count: used_slot_count = count
    			breathing_space: count < capacity * initial_occupation

    	default_create
    			-- Make table with current translations

    	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.
    			-- (from HASH_TABLE)
    		ensure -- from HASH_TABLE
    			breathing_space: n < capacity * initial_occupation
    			minimum_space: minimum_capacity < capacity * initial_occupation
    			more_than_minimum: capacity >= minimum_capacity
    			no_status: not special_status

    feature -- Access

    	current_keys: ARRAY [STRING_8]
    			-- New array containing actually used keys, from 1 to count
    			-- (from HASH_TABLE)
    		ensure -- from HASH_TABLE
    			good_count: Result.count = count

    	cursor: CURSOR
    			-- Current cursor position
    			-- (from HASH_TABLE)
    		ensure -- from HASH_TABLE
    			cursor_not_void: Result /= Void

    	found_item: STRING_8
    			-- Item, if any, yielded by last search operation
    			-- (from HASH_TABLE)

    	generating_type: STRING_8
    			-- Name of current object's generating type
    			-- (type of which it is a direct instance)
    			-- (from ANY)

    	generator: STRING_8
    			-- Name of current object's generating class
    			-- (base class of the type of which it is a direct instance)
    			-- (from ANY)

    	has (key: STRING_8): BOOLEAN
    			-- Is there an item in the table with key `key'?
    			-- (from HASH_TABLE)
    		ensure then -- from HASH_TABLE
    			default_case: (key = computed_default_key) implies (Result = has_default)

    	has_item (v: STRING_8): BOOLEAN
    			-- Does structure include `v'?
    			-- (Reference or object equality,
    			-- based on object_comparison.)
    			-- (from HASH_TABLE)
    		ensure -- from CONTAINER
    			not_found_in_empty: Result implies not is_empty

    	item alias "[]" (key: STRING_8): STRING_8 assign put
    			-- Item associated with `key', if present
    			-- otherwise default value of type `G'
    			-- Was declared in HASH_TABLE as synonym of infix "@".
    			-- (from HASH_TABLE)
    		require -- from TABLE
    			valid_key: valid_key (key)
    		ensure then -- from HASH_TABLE
    			default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value)

    	item_for_iteration: STRING_8
    			-- Element at current iteration position
    			-- (from HASH_TABLE)
    		require -- from HASH_TABLE
    			not_off: not off

    	key_for_iteration: STRING_8
    			-- Key at current iteration position
    			-- (from HASH_TABLE)
    		require -- from HASH_TABLE
    			not_off: not off
    		ensure -- from HASH_TABLE
    			at_iteration_position: Result = key_at (iteration_position)

    	infix "@" (key: STRING_8): STRING_8 assign put
    			-- Item associated with `key', if present
    			-- otherwise default value of type `G'
    			-- Was declared in HASH_TABLE as synonym of item.
    			-- (from HASH_TABLE)
    		require -- from TABLE
    			valid_key: valid_key (key)
    		ensure then -- from HASH_TABLE
    			default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value)

    feature -- Measurement

    	capacity: INTEGER_32
    			-- Number of items that may be stored.
    			-- (from HASH_TABLE)

    	count: INTEGER_32
    			-- Number of items in table
    			-- (from HASH_TABLE)

    	occurrences (v: STRING_8): INTEGER_32
    			-- Number of table items equal to `v'.
    			-- (from HASH_TABLE)
    		ensure -- from BAG
    			non_negative_occurrences: Result >= 0

    feature -- Comparison

    	frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
    			-- Are `some' and `other' either both void
    			-- or attached to isomorphic object structures?
    			-- (from ANY)
    		ensure -- from ANY
    			shallow_implies_deep: standard_equal (some, other) implies Result
    			both_or_none_void: (some = Void) implies (Result = (other = Void))
    			same_type: (Result and (some /= Void)) implies some.same_type (other)
    			symmetric: Result implies deep_equal (other, some)

    	frozen equal (some: ANY; other: like arg #1): BOOLEAN
    			-- Are `some' and `other' either both void or attached
    			-- to objects considered equal?
    			-- (from ANY)
    		ensure -- from ANY
    			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))

    	is_equal (other: like Current): BOOLEAN
    			-- Does table contain the same information as `other'?
    			-- (from HASH_TABLE)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			symmetric: Result implies other.is_equal (Current)
    			consistent: standard_is_equal (other) implies Result

    	frozen standard_equal (some: ANY; other: like arg #1): BOOLEAN
    			-- Are `some' and `other' either both void or attached to
    			-- field-by-field identical objects of the same type?
    			-- Always uses default object comparison criterion.
    			-- (from ANY)
    		ensure -- from ANY
    			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))

    	frozen standard_is_equal (other: like Current): BOOLEAN
    			-- Is `other' attached to an object of the same type
    			-- as current object, and field-by-field identical to it?
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			same_type: Result implies same_type (other)
    			symmetric: Result implies other.standard_is_equal (Current)

    feature -- Status report

    	after: BOOLEAN
    			-- Is cursor past last item?
    			-- Was declared in HASH_TABLE as synonym of off.
    			-- (from HASH_TABLE)
    		ensure -- from HASH_TABLE
    			definition: Result = ((not has_default and (iteration_position >= capacity)) or (has_default and (iteration_position = (capacity + 1))))

    	changeable_comparison_criterion: BOOLEAN
    			-- May object_comparison be changed?
    			-- (Answer: yes by default.)
    			-- (from CONTAINER)

    	conflict: BOOLEAN
    			-- Did last operation cause a conflict?
    			-- (from HASH_TABLE)

    	conforms_to (other: ANY): BOOLEAN
    			-- Does type of current object conform to type
    			-- of `other' (as per Eiffel: The Language, chapter 13)?
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void

    	extendible: BOOLEAN is True
    			-- May new items be added? (Answer: yes.)
    			-- (from HASH_TABLE)

    	found: BOOLEAN
    			-- Did last operation find the item sought?
    			-- (from HASH_TABLE)

    	full: BOOLEAN is False
    			-- Is structure filled to capacity? (Answer: no.)
    			-- (from HASH_TABLE)

    	inserted: BOOLEAN
    			-- Did last operation insert an item?
    			-- (from HASH_TABLE)

    	is_empty: BOOLEAN
    			-- Is structure empty?
    			-- (from FINITE)
    		require -- from  CONTAINER
    			True

    	is_inserted (v: STRING_8): BOOLEAN
    			-- Has `v' been inserted by the most recent insertion?
    			-- (By default, the value returned is equivalent to calling
    			-- `has (v)'. However, descendants might be able to provide more
    			-- efficient implementations.)
    			-- (from COLLECTION)

    	not_found: BOOLEAN
    			-- Did last operation fail to find the item sought?
    			-- (from HASH_TABLE)

    	object_comparison: BOOLEAN
    			-- Must search operations use equal rather than `='
    			-- for comparing references? (Default: no, use `='.)
    			-- (from CONTAINER)

    	off: BOOLEAN
    			-- Is cursor past last item?
    			-- Was declared in HASH_TABLE as synonym of after.
    			-- (from HASH_TABLE)
    		ensure -- from HASH_TABLE
    			definition: Result = ((not has_default and (iteration_position >= capacity)) or (has_default and (iteration_position = (capacity + 1))))

    	prunable: BOOLEAN
    			-- May items be removed? (Answer: yes.)
    			-- (from HASH_TABLE)

    	removed: BOOLEAN
    			-- Did last operation remove an item?
    			-- (from HASH_TABLE)

    	replaced: BOOLEAN
    			-- Did last operation replace an item?
    			-- (from HASH_TABLE)

    	same_type (other: ANY): BOOLEAN
    			-- Is type of current object identical to type of `other'?
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			definition: Result = (conforms_to (other) and other.conforms_to (Current))

    	valid_cursor (c: CURSOR): BOOLEAN
    			-- Can cursor be moved to position `c'?
    			-- (from HASH_TABLE)
    		require -- from HASH_TABLE
    			c_not_void: c /= Void

    	valid_key (k: STRING_8): BOOLEAN
    			-- Is `k' a valid key?
    			-- (Answer: always yes for hash tables in this version)
    			-- (from HASH_TABLE)
    		require -- from  TABLE
    			True
    		ensure then -- from HASH_TABLE
    			Result

    feature -- Status setting

    	compare_objects
    			-- Ensure that future search operations will use equal
    			-- rather than `=' for comparing references.
    			-- (from CONTAINER)
    		require -- from CONTAINER
    			changeable_comparison_criterion: changeable_comparison_criterion
    		ensure -- from CONTAINER
    			object_comparison

    	compare_references
    			-- Ensure that future search operations will use `='
    			-- rather than equal for comparing references.
    			-- (from CONTAINER)
    		require -- from CONTAINER
    			changeable_comparison_criterion: changeable_comparison_criterion
    		ensure -- from CONTAINER
    			reference_comparison: not object_comparison

    feature -- Cursor movement

    	forth
    			-- Advance cursor to next occupied position,
    			-- or off if no such position remains.
    			-- (from HASH_TABLE)
    		require -- from HASH_TABLE
    			not_off: not off

    	go_to (c: CURSOR)
    			-- Move to position `c'.
    			-- (from HASH_TABLE)
    		require -- from HASH_TABLE
    			c_not_void: c /= Void
    			valid_cursor: valid_cursor (c)

    	search (key: STRING_8)
    			-- Search for item of key `key'.
    			-- If found, set found to true, and set
    			-- found_item to item associated with `key'.
    			-- (from HASH_TABLE)
    		ensure -- from HASH_TABLE
    			found_or_not_found: found or not_found
    			item_if_found: found implies (found_item = content.item (position))

    	start
    			-- Bring cursor to first position.
    			-- (from HASH_TABLE)

    feature -- Element change

    	extend (new: STRING_8; key: STRING_8)
    			-- Assuming there is no item of key `key',
    			-- insert `new' with `key'.
    			-- Set inserted.
    		require -- from HASH_TABLE
    			not_present: not has (key)
    		ensure -- from HASH_TABLE
    			inserted: inserted
    			insertion_done: item (key) = new
    			one_more: count = old count + 1
    			same_slot_count_or_one_more_unless_reallocated: (used_slot_count = old used_slot_count) or (used_slot_count = old used_slot_count + 1) or (used_slot_count = count)
    			default_property: has_default = ((key = computed_default_key) or (old has_default))

    	fill (other: CONTAINER [STRING_8])
    			-- Fill with as many items of `other' as possible.
    			-- The representations of `other' and current structure
    			-- need not be the same.
    			-- (from COLLECTION)
    		require -- from COLLECTION
    			other_not_void: other /= Void
    			extendible: extendible

    	force (new: STRING_8; key: STRING_8)
    			-- 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.
    		require else -- from HASH_TABLE
    			True
    		ensure then -- from HASH_TABLE
    			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)
    			same_slot_count_or_one_more_unless_reallocated: (used_slot_count = old used_slot_count) or (used_slot_count = old used_slot_count + 1) or (used_slot_count = count)
    			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)))

    	merge (other: HASH_TABLE [STRING_8, STRING_8])
    			-- Merge `other' into Current. If `other' has some elements
    			-- with same key as in `Current', replace them by one from
    			-- `other'.
    			-- (from HASH_TABLE)
    		require -- from HASH_TABLE
    			other_not_void: other /= Void
    		ensure -- from HASH_TABLE
    			inserted: other.current_keys.linear_representation.for_all (agent has)

    	put (new: STRING_8; key: STRING_8)
    			-- 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).
    		require -- from TABLE
    			valid_key: valid_key (key)
    		ensure then -- from HASH_TABLE
    			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)))
    			slot_count_unchanged_if_conflict: conflict implies (used_slot_count = old used_slot_count)
    			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)))

    	replace (new: STRING_8; key: STRING_8)
    			-- 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).
    		ensure -- from HASH_TABLE
    			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))

    feature -- Removal

    	clear_all
    			-- Reset all items to default values; reset status.
    		require -- from COLLECTION
    			prunable: prunable
    		ensure -- from COLLECTION
    			wiped_out: is_empty
    		ensure then -- from HASH_TABLE
    			position_equal_to_zero: position = 0
    			count_equal_to_zero: count = 0
    			used_slot_count_equal_to_zero: used_slot_count = 0
    			has_default_set: not has_default
    			no_status: not special_status

    feature -- Conversion

    	linear_representation: ARRAYED_LIST [STRING_8]
    			-- Representation as a linear structure
    			-- (from HASH_TABLE)
    		require -- from  CONTAINER
    			True
    		ensure then -- from HASH_TABLE
    			result_exists: Result /= Void
    			good_count: Result.count = count

    feature -- Duplication

    	copy (other: like Current)
    			-- Re-initialize from `other'.
    			-- (from HASH_TABLE)
    		require -- from ANY
    			other_not_void: other /= Void
    			type_identity: same_type (other)
    		ensure -- from ANY
    			is_equal: is_equal (other)

    	frozen deep_copy (other: like Current)
    			-- Effect equivalent to that of:
    			--		copy (`other' . deep_twin)
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    		ensure -- from ANY
    			deep_equal: deep_equal (Current, other)

    	frozen deep_twin: like Current
    			-- New object structure recursively duplicated from Current.
    			-- (from ANY)
    		ensure -- from ANY
    			deep_equal: deep_equal (Current, Result)

    	frozen standard_copy (other: like Current)
    			-- Copy every field of `other' onto corresponding field
    			-- of current object.
    			-- (from ANY)
    		require -- from ANY
    			other_not_void: other /= Void
    			type_identity: same_type (other)
    		ensure -- from ANY
    			is_standard_equal: standard_is_equal (other)

    	frozen standard_twin: like Current
    			-- New object field-by-field identical to `other'.
    			-- Always uses default copying semantics.
    			-- (from ANY)
    		ensure -- from ANY
    			standard_twin_not_void: Result /= Void
    			equal: standard_equal (Result, Current)

    	frozen twin: like Current
    			-- New object equal to `Current'
    			-- twin calls copy; to change copying/twining semantics, redefine copy.
    			-- (from ANY)
    		ensure -- from ANY
    			twin_not_void: Result /= Void
    			is_equal: Result.is_equal (Current)

    feature -- Basic operations

    	frozen default: like Current
    			-- Default value of object's type
    			-- (from ANY)

    	frozen default_pointer: POINTER
    			-- Default value of type `POINTER'
    			-- (Avoid the need to write `p'.default for
    			-- some `p' of type `POINTER'.)
    			-- (from ANY)

    	default_rescue
    			-- Process exception for routines with no Rescue clause.
    			-- (Default: do nothing.)
    			-- (from ANY)

    	frozen do_nothing
    			-- Execute a null action.
    			-- (from ANY)

    feature -- Output

    	io: STD_FILES
    			-- Handle to standard file setup
    			-- (from ANY)

    	out: STRING_8
    			-- Printable representation of translations

    	print (some: ANY)
    			-- Write terse external representation of `some'
    			-- on standard output.
    			-- (from ANY)

    	frozen tagged_out: STRING_8
    			-- New string containing terse printable representation
    			-- of current object
    			-- Was declared in ANY as synonym of out.
    			-- (from ANY)

    feature -- Platform

    	operating_environment: OPERATING_ENVIRONMENT
    			-- Objects available from the operating system
    			-- (from ANY)

    invariant
    		-- from HASH_TABLE
    	keys_not_void: keys /= Void
    	content_not_void: content /= Void
    	deleted_marks_not_void: deleted_marks /= Void
    	keys_same_capacity_plus_one: keys.count = capacity + 1
    	content_same_capacity_plus_one: content.count = capacity + 1
    	deleted_same_capacity: deleted_marks.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)
    	max_occupation_meaningful: (max_occupation > 0) and (max_occupation < 1)
    	initial_occupation_meaningful: (initial_occupation > 0) and (initial_occupation < 1)
    	sized_generously_enough: initial_occupation < max_occupation
    	count_big_enough: 0 <= count
    	count_small_enough: count <= capacity
    	breathing_space: count <= capacity * max_occupation
    	count_no_more_than_slot_count: count <= used_slot_count
    	slot_count_big_enough: 0 <= count
    	slot_count_small_enough: used_slot_count <= capacity

    		-- from FINITE
    	empty_definition: is_empty = (count = 0)
    	non_negative_count: count >= 0

    		-- from ANY
    	reflexive_equality: standard_is_equal (Current)
    	reflexive_conformance: conforms_to (Current)

    indexing
    	library: "EiffelBase: Library of reusable components for Eiffel."
    	copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
    	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
    	source: "[
    		Eiffel Software
    		356 Storke Road, 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 CLASS_NAME_TRANSLATIONS