note
	description: "Original values of the attributes of a mismatched object."
	instructions: "[
		This object will contain the original values of the attributes
		of a retrieved object for which a mismatched was detected at
		retrieval time. The value are indexed by the name of the attribute
		in the stored object. One extra entry is provided to contain the
		original name of the class in the storing system, indexed by the
		string 'class'. This allows correct_mismatch to determine the
		original name of its generating class in case class-name
		translation is in effect.
	]"
	library: "Free implementation of ELKS library"
	status: "See notice at end of class."
	legal: "See notice at end of class."
	date: "$Date: 2020-05-19 14:29:33 +0000 (Tue, 19 May 2020) $"
	revision: "$Revision: 104259 $"

class interface
	MISMATCH_INFORMATION

create {MISMATCH_CORRECTOR}
	default_create
			-- Make container with default size


create 
	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)
		require -- from HASH_TABLE
			n_non_negative: n >= 0
		ensure -- from HASH_TABLE
			breathing_space: n < capacity
			more_than_minimum: capacity > Minimum_capacity
			no_status: not special_status

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
			breathing_space: count < capacity

	default_create
			-- Make container with default size

	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)
		require -- from HASH_TABLE
			n_non_negative: n >= 0
		ensure -- from HASH_TABLE
			breathing_space: n < capacity
			more_than_minimum: capacity > Minimum_capacity
			no_status: not special_status

	make_equal (n: INTEGER_32)
			-- Allocate hash table for at least n items.
			-- The table will be resized automatically
			-- if more than n items are inserted.
			-- Use ~ to compare items.
			-- (from HASH_TABLE)
		require -- from HASH_TABLE
			n_non_negative: n >= 0
		ensure -- from HASH_TABLE
			breathing_space: n < capacity
			more_than_minimum: capacity > Minimum_capacity
			no_status: not special_status
			compare_objects: object_comparison
	
feature -- Access

	at alias "@" (key: STRING_8): detachable ANY assign force
			-- Item associated with key, if present
			-- otherwise default value of type G.
			-- Was declared in HASH_TABLE as synonym of item.
			-- (from HASH_TABLE)
		note
			option: stable
		ensure then -- from HASH_TABLE
			default_value_if_not_present: (not has (key)) implies (Result = computed_default_value)

	class_name: STRING_8
			-- Name of generating class which held attribute values
		ensure
			result_exists: Result /= Void

	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

	current_version: detachable IMMUTABLE_STRING_8
			-- Version associated to class_name in the current system.

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

	definite_item (key: STRING_8): detachable ANY
			-- Entry of key k.
			-- (from HASH_TABLE)
		require -- from TABLE
			valid_key: has (key)
		require -- from TABLE
			valid_key: has (key)

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

	generating_type: TYPE [detachable MISMATCH_INFORMATION]
			-- Type of current object
			-- (type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generating_type_not_void: Result /= Void

	generator: STRING_8
			-- Name of current object's generating class
			-- (base class of the type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generator_not_void: Result /= Void
			generator_not_empty: not Result.is_empty

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

	has_item (v: detachable ANY): 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

	has_key (key: STRING_8): BOOLEAN
			-- Is there an item in the table with key key?
			-- Set found_item to the found item.
			-- (from HASH_TABLE)
		ensure then -- from HASH_TABLE
			default_case: (key = computed_default_key) implies (Result = has_default)
			found: Result = found
			item_if_found: found implies (found_item = item (key))

	hash_code_of (a_key: attached STRING_8): INTEGER_32
			-- Hash_code value associated to a_key.
			-- (from HASH_TABLE)
		ensure -- from HASH_TABLE
			non_negative: Result >= 0

	item alias "[]" (key: STRING_8): detachable ANY assign force
			-- Item associated with key, if present
			-- otherwise default value of type G.
			-- Was declared in HASH_TABLE as synonym of at.
			-- (from HASH_TABLE)
		note
			option: stable
		ensure then -- from HASH_TABLE
			default_value_if_not_present: (not has (key)) implies (Result = computed_default_value)

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

	iteration_item (i: INTEGER_32): detachable ANY
			-- Entry at position i.
			-- (from HASH_TABLE)
		require -- from READABLE_INDEXABLE
			valid_index: valid_iteration_index (i)

	key_for_iteration: STRING_8
			-- Key at current iteration position
			-- (from HASH_TABLE)
		require -- from HASH_TABLE
			not_off: not off

	new_cursor: HASH_TABLE_ITERATION_CURSOR [detachable ANY, STRING_8]
			-- Fresh cursor associated with current structure
			-- (from HASH_TABLE)
		require -- from  ITERABLE
			True
		ensure -- from ITERABLE
			result_attached: Result /= Void

	stored_version: detachable IMMUTABLE_STRING_8
			-- Version associated to class_name in the stored system.

	Type_name_key: STRING_8 = "_type_name"
			-- Associated key for retrieving the type name of a mismatch.
	
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)

	iteration_lower: INTEGER_32
			-- Minimum index.
			-- (from HASH_TABLE)

	iteration_upper: INTEGER_32
			-- Maximum index.
			-- (from HASH_TABLE)

	occurrences (v: detachable ANY): 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 (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b either both void
			-- or attached to isomorphic object structures?
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			shallow_implies_deep: standard_equal (a, b) implies Result
			both_or_none_void: (a = Void) implies (Result = (b = Void))
			same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b))
			symmetric: Result implies deep_equal (b, a)

	disjoint (other: HASH_TABLE [detachable ANY, STRING_8]): BOOLEAN
			-- Is Current and other disjoint on their keys?
			-- Use same_keys for comparison.
			-- (from HASH_TABLE)

	frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b either both void or attached
			-- to objects considered equal?
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b))

	frozen is_deep_equal alias "≡≡≡" (other: MISMATCH_INFORMATION): BOOLEAN
			-- Are Current and other attached to isomorphic object structures?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			shallow_implies_deep: standard_is_equal (other) implies Result
			same_type: Result implies same_type (other)
			symmetric: Result implies other.is_deep_equal (Current)

	is_equal (other: MISMATCH_INFORMATION): 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 ~ Current
			consistent: standard_is_equal (other) implies Result

	same_keys (a_search_key, a_key: STRING_8): BOOLEAN
			-- Does a_search_key equal to a_key?
			-- (from HASH_TABLE)

	frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b 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
			instance_free: class
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b))

	frozen standard_is_equal alias "≜" (other: MISMATCH_INFORMATION): 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)

	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 = False
			-- May new items be added?
			-- (from HASH_TABLE)

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

	Full: BOOLEAN = False
			-- Is structure filled to capacity?
			-- (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: detachable ANY): 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)

	is_version_mismatched: BOOLEAN
			-- Is the stored_version different from the current system version?

	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)

	prunable: BOOLEAN
			-- May items be removed? (Answer: yes.)
			-- (from DYNAMIC_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_iteration_index (i: INTEGER_32): BOOLEAN
			-- Is i a valid index?
			-- (from HASH_TABLE)
		ensure -- from READABLE_INDEXABLE
			only_if_in_index_set: Result implies (iteration_lower <= i and i <= iteration_upper)
	
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 = item (key))

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

	extend (new: detachable ANY; key: STRING_8)
			-- Assuming there is no item of key key,
			-- insert new with key.
			-- Set inserted.
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
			-- (from HASH_TABLE)
		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
			default_property: has_default = ((key = computed_default_key) or (old has_default))

	fill (other: CONTAINER [detachable ANY])
			-- 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: detachable ANY; 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.
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
			-- (from HASH_TABLE)
		require -- from TABLE
			valid_key: has (key)
		require else -- from HASH_TABLE
				True
		ensure -- from TABLE
			inserted: definite_item (key) = new
		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)
			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 [detachable ANY, 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: across
					other as other_cursor
				all
					has (other_cursor.key)
				end

	put (new: detachable ANY; 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).
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
			-- (from HASH_TABLE)
		require -- from TABLE
			valid_key: has (key)
		require else -- from HASH_TABLE
				True
		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)))
			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: detachable ANY; 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).
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
			-- (from HASH_TABLE)
		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)

	replace_key (new_key: STRING_8; old_key: STRING_8)
			-- If there is an item of key old_key and no item of key
			-- new_key, replace the former's key by new_key,
			-- set replaced, and set found_item to the item
			-- previously associated with old_key.
			-- Otherwise set not_found or conflict respectively.
			-- If conflict, set found_item to the item previously
			-- associated with new_key.
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
			-- (from HASH_TABLE)
		ensure -- from HASH_TABLE
			same_count: count = old count
			replaced_or_conflict_or_not_found: replaced or conflict or not_found
			old_absent: (replaced and not same_keys (new_key, old_key)) implies (not has (old_key))
			new_present: (replaced or conflict) = has (new_key)
			new_item: replaced implies (item (new_key) = old (item (old_key)))
			not_found_implies_no_old_key: not_found implies old (not has (old_key))
			conflict_iff_already_present: conflict = old has (new_key)
			not_inserted_if_conflict: conflict implies (item (new_key) = old item (new_key))
	
feature -- Removal

	prune (v: detachable ANY)
			-- Remove first occurrence of v, if any,
			-- after cursor position.
			-- Move cursor to right neighbor.
			-- (or after if no right neighbor or v does not occur)
			-- (from HASH_TABLE)
		require -- from COLLECTION
			prunable: prunable

	prune_all (v: detachable ANY)
			-- Remove all occurrences of v.
			-- (Reference or object equality,
			-- based on object_comparison.)
			-- (from COLLECTION)
		require -- from COLLECTION
			prunable: prunable
		ensure -- from COLLECTION
			no_more_occurrences: not has_item (v)

	remove (key: STRING_8)
			-- Remove item associated with key, if present.
			-- Set removed if and only if an item has been
			-- removed (i.e. key was present);
			-- if so, set position to index of removed element.
			-- If not, set not_found.
			-- Reset found_item to its default value if removed.
			-- (from HASH_TABLE)
		require -- from DYNAMIC_TABLE
			prunable: prunable
			valid_key: has (key)
		require else -- from HASH_TABLE
				prunable
		ensure then -- from HASH_TABLE
			removed_or_not_found: removed or not_found
			not_present: not has (key)
			one_less: found implies (count = old count - 1)
			default_case: (key = computed_default_key) implies (not has_default)
			non_default_case: (key /= computed_default_key) implies (has_default = old has_default)

	wipe_out
			-- Reset all items to default values; reset status.
			-- (from HASH_TABLE)
		require -- from COLLECTION
			prunable: prunable
		ensure -- from COLLECTION
			wiped_out: is_empty
		ensure then -- from HASH_TABLE
			position_equal_to_zero: item_position = 0
			count_equal_to_zero: count = 0
			has_default_set: not has_default
			no_status: not special_status
	
feature -- Transformation

	correct_mismatch
			-- Attempt to correct object mismatch during retrieve using Mismatch_information.
			-- (from HASH_TABLE)
	
feature -- Conversion

	linear_representation: ARRAYED_LIST [detachable ANY]
			-- 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: MISMATCH_INFORMATION)
			-- 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: Current ~ other

	frozen deep_copy (other: MISMATCH_INFORMATION)
			-- 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: MISMATCH_INFORMATION
			-- New object structure recursively duplicated from Current.
			-- (from ANY)
		ensure -- from ANY
			deep_twin_not_void: Result /= Void
			deep_equal: deep_equal (Current, Result)

	frozen standard_copy (other: MISMATCH_INFORMATION)
			-- 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: MISMATCH_INFORMATION
			-- 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: MISMATCH_INFORMATION
			-- New object equal to Current
			-- twin calls copy; to change copying/twinning semantics, redefine copy.
			-- (from ANY)
		ensure -- from ANY
			twin_not_void: Result /= Void
			is_equal: Result ~ Current
	
feature -- Basic operations

	frozen default: detachable MISMATCH_INFORMATION
			-- 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)
		ensure -- from ANY
			instance_free: class

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

	frozen do_nothing
			-- Execute a null action.
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
	
feature -- Inapplicable

	bag_put (v: detachable ANY)
			-- Ensure that structure includes v.
			-- (from TABLE)
		require -- from COLLECTION
			extendible: Extendible
		ensure -- from COLLECTION
			item_inserted: is_inserted (v)

	collection_extend (v: detachable ANY)
			-- Insert a new occurrence of v.
			-- (from HASH_TABLE)
		require -- from COLLECTION
			extendible: Extendible
		ensure -- from COLLECTION
			item_inserted: is_inserted (v)
	
feature -- Correction

	Mismatch_information: MISMATCH_INFORMATION
			-- Original attribute values of mismatched object
			-- (from MISMATCH_CORRECTOR)
	
feature -- Output

	Io: STD_FILES
			-- Handle to standard file setup
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			io_not_void: Result /= Void

	out: STRING_8
			-- Printable representation of attributes values
		ensure -- from ANY
			out_not_void: Result /= Void

	print (o: detachable ANY)
			-- Write terse external representation of o
			-- on standard output.
			-- (from ANY)
		ensure -- from ANY
			instance_free: class

	frozen tagged_out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- (from ANY)
		ensure -- from ANY
			tagged_out_not_void: Result /= Void
	
feature -- Platform

	Operating_environment: OPERATING_ENVIRONMENT
			-- Objects available from the operating system
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			operating_environment_not_void: Result /= Void
	
feature -- Settings

	set_versions (a_stored_version: like stored_version; a_current_version: like current_version)
			-- Set stored_version with a_stored_version.
			-- Set current_version with a_current_version.
		ensure
			stored_version_set: stored_version = a_stored_version
			current_version_set: current_version = a_current_version
	
invariant
		-- from HASH_TABLE
	keys_not_void: keys /= Void
	content_not_void: content /= Void
	keys_enough_capacity: keys.count <= capacity + 1
	content_enough_capacity: content.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)
	count_big_enough: 0 <= count
	count_small_enough: count <= capacity
	slot_count_big_enough: 0 <= count

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

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

		-- from READABLE_INDEXABLE
	consistent_boundaries: iteration_lower <= iteration_upper or else iteration_lower = iteration_upper + 1

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

Generated by ISE EiffelStudio