Automatic generation produced by ISE Eiffel
note 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 [REAL_64]"), 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. ]" library: "Free implementation of ELKS library" status: "See notice at end of class." legal: "See notice at end of class." date: "$Date: 2018-11-14 05:55:55 -0900 (Wed, 14 Nov 2018) $" revision: "$Revision: 102462 $" class interface CLASS_NAME_TRANSLATIONS create default_create -- Make table with current translations create {CLASS_NAME_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) 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 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) 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 make_from_iterable_tuples (other: ITERABLE [TUPLE [STRING_8, STRING_8]]) -- (from HASH_TABLE) feature -- Access at alias "@" (key: STRING_8): detachable STRING_8 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) 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 definite_item (key: STRING_8): STRING_8 -- Entry of key k. -- (from HASH_TABLE) require -- from TABLE valid_key: has (key) require -- from TABLE valid_key: has (key) found_item: detachable STRING_8 -- Item, if any, yielded by last search operation -- (from HASH_TABLE) generating_type: TYPE [detachable CLASS_NAME_TRANSLATIONS] -- 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: 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 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 STRING_8 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: STRING_8 -- Element at current iteration position -- (from HASH_TABLE) require -- from HASH_TABLE not_off: not off iteration_item (i: INTEGER_32): STRING_8 -- 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 [STRING_8, STRING_8] -- Fresh cursor associated with current structure -- (from HASH_TABLE) require -- from ITERABLE True ensure -- from ITERABLE result_attached: Result /= Void 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: 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 (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 [STRING_8, 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: CLASS_NAME_TRANSLATIONS): 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: CLASS_NAME_TRANSLATIONS): 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: CLASS_NAME_TRANSLATIONS): 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: 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) 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: 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 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 -- 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 [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: ∀ o: other ¦ item (@o.key) = o 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: 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: 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) 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 usage instructions at end of class. -- (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: STRING_8) -- 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: STRING_8) -- 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. 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 [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: CLASS_NAME_TRANSLATIONS) -- 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: CLASS_NAME_TRANSLATIONS) -- 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: CLASS_NAME_TRANSLATIONS -- 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: CLASS_NAME_TRANSLATIONS) -- 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: CLASS_NAME_TRANSLATIONS -- 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: CLASS_NAME_TRANSLATIONS -- 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 CLASS_NAME_TRANSLATIONS -- 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: STRING_8) -- Ensure that structure includes v. -- (from TABLE) require -- from COLLECTION extendible: Extendible ensure -- from COLLECTION item_inserted: is_inserted (v) collection_extend (v: STRING_8) -- 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 translations 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 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-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 -- class CLASS_NAME_TRANSLATIONS -- Generated by Eiffel Studio --
For more details: eiffel.org