note description: "Unicode strings" remark: "[ Unless specified otherwise, STRING and CHARACTER are supposed to contain characters whose code follows the unicode character set. In other words characters whose code is between 128 and 255 should follow the ISO 8859-1 Latin-1 character set. ]" remark2: "[ By default UC_STRING is implemented using the UTF-8 encoding. Use UC_UTF*_STRING to specify the encoding explicitly. ]" library: "Gobo Eiffel Kernel Library" copyright: "Copyright (c) 2001-2018, Eric Bezault and others" license: "MIT License" date: "$Date: 2019-02-07 22:54:15 +0000 (Thu, 07 Feb 2019) $" revision: "$Revision: 102807 $" class interface UC_STRING create make (suggested_capacity: INTEGER_32) -- Create empty string, or remove all characters from -- existing string. -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL non_negative_size: suggested_capacity >= 0 ensure -- from READABLE_STRING_GENERAL empty_string: count = 0 area_allocated: byte_capacity >= suggested_capacity ensure then byte_count_set: byte_count = 0 byte_capacity_set: byte_capacity >= suggested_capacity make_empty -- Create empty string. -- (ELKS 2001 STRING) ensure -- from READABLE_STRING_GENERAL empty: count = 0 area_allocated: byte_capacity >= 0 make_from_string (a_string: STRING_8) -- Initialize from the character sequence of a_string. -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 string_exists: a_string /= Void ensure -- from READABLE_STRING_8 not_shared_implementation: Current /= a_string implies not shared_with (a_string) initialized: same_string (a_string) ensure then same_unicode: same_unicode_string (a_string) make_from_utf8 (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-8 representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf8: Utf8.valid_utf8 (s) make_filled (c: CHARACTER_8; n: INTEGER_32) -- Create string of length n filled with character c. -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 valid_count: n >= 0 ensure -- from READABLE_STRING_8 count_set: count = n area_allocated: byte_capacity >= n filled: occurrences (c) = count ensure then filled_code: code_occurrences (c.code) = count make_filled_code (a_code: INTEGER_32; n: INTEGER_32) -- Create string of length n filled with unicode -- character of code a_code. require valid_code: Unicode.valid_code (a_code) valid_count: n >= 0 ensure count_set: count = n filled: code_occurrences (a_code) = count make_filled_unicode (c: UC_CHARACTER; n: INTEGER_32) -- Create string of length n filled with unicode character c. require c_not_void: c /= Void valid_count: n >= 0 ensure count_set: count = n filled: unicode_occurrences (c) = count make_from_substring (a_string: STRING_8; start_index, end_index: INTEGER_32) -- Initialize from the character sequence of a_string -- between start_index and end_index inclusive. require a_string_not_void: a_string /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= a_string.count meaningful_interval: start_index <= end_index + 1 ensure initialized: same_unicode_string (a_string.substring (start_index, end_index)) make_from_utf16 (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-16 representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16: Utf16.valid_utf16 (s) make_from_utf16le (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-16LE representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16le: Utf16.valid_utf16le (s) make_from_utf16be (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-16BE representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16be: Utf16.valid_utf16be (s) make_from_string_general (a_string: STRING_GENERAL) -- Initialize from the character sequence of a_string. require a_string_not_void: a_string /= Void ensure same_unicode: same_unicode_string (a_string) make_from_substring_general (a_string: STRING_GENERAL; start_index, end_index: INTEGER_32) -- Initialize from the character sequence of a_string -- between start_index and end_index inclusive. require a_string_not_void: a_string /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= a_string.count meaningful_interval: start_index <= end_index + 1 ensure initialized: same_unicode_string (a_string.substring (start_index, end_index)) feature -- Initialization adapt (s: STRING_8): UC_STRING -- Object of a type conforming to the type of s, -- initialized with attributes from s -- (from STRING_8) ensure -- from STRING_8 adapt_not_void: Result /= Void shared_implementation: Result.shared_with (s) from_c (c_string: POINTER) -- Reset contents of string from contents of c_string, -- a string created by some C function. -- (from STRING_8) require -- from STRING_8 c_string_exists: c_string /= default_pointer ensure -- from STRING_8 no_zero_byte: not has ('%U') from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32) -- Reset contents of string from substring of c_string, -- between start_pos and end_pos, -- and c_string created by some C function. -- (from STRING_8) require -- from STRING_8 c_string_exists: c_string /= default_pointer start_position_big_enough: start_pos >= 1 end_position_big_enough: start_pos <= end_pos + 1 ensure -- from STRING_8 valid_count: count = end_pos - start_pos + 1 make (suggested_capacity: INTEGER_32) -- Create empty string, or remove all characters from -- existing string. -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL non_negative_size: suggested_capacity >= 0 ensure -- from READABLE_STRING_GENERAL empty_string: count = 0 area_allocated: byte_capacity >= suggested_capacity ensure then byte_count_set: byte_count = 0 byte_capacity_set: byte_capacity >= suggested_capacity make_from_c (c_string: POINTER) -- Initialize from contents of c_string, -- a string created by some C function. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 c_string_exists: c_string /= default_pointer make_from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32) -- Initialize from substring of c_string, -- between start_pos and end_pos, -- c_string created by some C function. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 c_string_exists: c_string /= default_pointer start_position_big_enough: start_pos >= 1 end_position_big_enough: start_pos <= end_pos + 1 make_from_cil (a_system_string: detachable SYSTEM_STRING) -- Initialize Current with a_system_string. -- (from STRING_8) require -- from READABLE_STRING_8 is_dotnet: {PLATFORM}.is_dotnet make_from_string (a_string: STRING_8) -- Initialize from the character sequence of a_string. -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 string_exists: a_string /= Void ensure -- from READABLE_STRING_8 not_shared_implementation: Current /= a_string implies not shared_with (a_string) initialized: same_string (a_string) ensure then same_unicode: same_unicode_string (a_string) feature -- Access Any_: KL_ANY_ROUTINES -- Routines that ought to be in class ANY -- (from KL_IMPORTED_ANY_ROUTINES) ensure -- from KL_IMPORTED_ANY_ROUTINES instance_free: class any_routines_not_void: Result /= Void at alias "@" (i: INTEGER_32): CHARACTER_8 -- Character at index i -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 True require -- from TABLE valid_key: valid_index (i) require -- from TO_SPECIAL valid_index: valid_index (i) ensure then definition: Result = item (i) case_insensitive_hash_code: INTEGER_32 -- Hash code value of the lower case version of Current. -- (from READABLE_STRING_GENERAL) ensure -- from READABLE_STRING_GENERAL consistent: Result = as_lower.case_insensitive_hash_code character_32_item (i: INTEGER_32): CHARACTER_32 -- Character at position i. -- (from STRING_8) require -- from READABLE_STRING_GENERAL valid_index: valid_index (i) False_constant: STRING_8 = "false" -- Constant string "false" -- (from READABLE_STRING_GENERAL) fuzzy_index (other: READABLE_STRING_GENERAL; start: INTEGER_32; fuzz: INTEGER_32): INTEGER_32 -- Position of first occurrence of other at or after start -- with 0..fuzz mismatches between the string and other. -- 0 if there are no fuzzy matches -- (from READABLE_STRING_8) require -- from READABLE_STRING_GENERAL other_exists: other /= Void other_not_empty: not other.is_empty start_large_enough: start >= 1 start_small_enough: start <= count acceptable_fuzzy: fuzz <= other.count generating_type: TYPE [detachable UC_STRING] -- 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 hash_code: INTEGER_32 -- Hash code -- (ELKS 2001 STRING) require -- from HASHABLE True ensure -- from HASHABLE good_hash_value: Result >= 0 index_of (c: CHARACTER_8; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of character c -- at or after start_index; 0 if none -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 start_large_enough: start_index >= 1 start_small_enough: start_index <= count + 1 ensure -- from READABLE_STRING_8 valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).has (c) found_if_present: substring (start_index, count).has (c) implies item (Result) = c none_before: substring (start_index, count).has (c) implies not substring (start_index, Result - 1).has (c) character_32_index_of (c: like character_32_item; start_index: INTEGER_32): INTEGER_32 -- Position of first occurrence of c at or after start_index; -- 0 if none. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL start_large_enough: start_index >= 1 start_small_enough: start_index <= count + 1 ensure -- from READABLE_STRING_GENERAL valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).character_32_has (c) found_if_present: substring (start_index, count).character_32_has (c) implies character_32_item (Result) = c none_before: substring (start_index, count).character_32_has (c) implies not substring (start_index, Result - 1).character_32_has (c) index_of_item_code (a_code: INTEGER_32; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of unicode character with -- code a_code at or after start_index; 0 if none require valid_start_index: start_index >= 1 and start_index <= count + 1 valid_code: Unicode.valid_code (a_code) ensure valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).has_item_code (a_code) found_if_present: substring (start_index, count).has_item_code (a_code) implies item_code (Result) = a_code none_before: substring (start_index, count).has_item_code (a_code) implies not substring (start_index, Result - 1).has_item_code (a_code) index_of_unicode (c: UC_CHARACTER; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of c at or after start_index; -- 0 if none require c_not_void: c /= Void valid_start_index: start_index >= 1 and start_index <= count + 1 ensure valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).has_unicode (c) found_if_present: substring (start_index, count).has_unicode (c) implies item_code (Result) = c.code none_before: substring (start_index, count).has_unicode (c) implies not substring (start_index, Result - 1).has_unicode (c) Integer_: KL_INTEGER_ROUTINES -- Routines that ought to be in class INTEGER -- (from KL_IMPORTED_INTEGER_ROUTINES) ensure -- from KL_IMPORTED_INTEGER_ROUTINES instance_free: class integer_routines_not_void: Result /= Void item (i: INTEGER_32): CHARACTER_8 -- Character at index i; -- '%U' if the unicode character at index -- i cannot fit into a CHARACTER -- (Extended from ELKS 2001 STRING) -- Note: Use item_code instead of this routine when Current -- can contain characters which may not fit into a CHARACTER. ensure then code_small_enough: item_code (i) <= Platform.Maximum_character_code implies Result.code = item_code (i) overflow: item_code (i) > Platform.Maximum_character_code implies Result = '%U' item_code (i: INTEGER_32): INTEGER_32 -- Code of character at index i require -- from READABLE_STRING_8 index_small_enough: i <= count index_large_enough: i > 0 ensure then item_code_not_negative: Result >= 0 valid_item_code: Unicode.valid_code (Result) last_index_of (c: CHARACTER_8; start_index_from_end: INTEGER_32): INTEGER_32 -- Position of last occurrence of c, -- 0 if none. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 start_index_small_enough: start_index_from_end <= count start_index_large_enough: start_index_from_end >= 1 ensure -- from READABLE_STRING_8 valid_result: 0 <= Result and Result <= start_index_from_end zero_if_absent: (Result = 0) = not substring (1, start_index_from_end).has (c) found_if_present: substring (1, start_index_from_end).has (c) implies item (Result) = c none_after: substring (1, start_index_from_end).has (c) implies not substring (Result + 1, start_index_from_end).has (c) character_32_last_index_of (c: like character_32_item; start_index_from_end: INTEGER_32): INTEGER_32 -- Position of last occurrence of c. -- 0 if none. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL start_index_small_enough: start_index_from_end <= count start_index_large_enough: start_index_from_end >= 1 ensure -- from READABLE_STRING_GENERAL valid_result: 0 <= Result and Result <= start_index_from_end zero_if_absent: (Result = 0) = not substring (1, start_index_from_end).character_32_has (c) found_if_present: substring (1, start_index_from_end).character_32_has (c) implies character_32_item (Result) = c none_after: substring (1, start_index_from_end).character_32_has (c) implies not substring (Result + 1, start_index_from_end).character_32_has (c) last_index_of_code (c: like code; start_index_from_end: INTEGER_32): INTEGER_32 -- Position of last occurrence of c. -- 0 if none. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL start_index_small_enough: start_index_from_end <= count start_index_large_enough: start_index_from_end >= 1 ensure -- from READABLE_STRING_GENERAL valid_result: 0 <= Result and Result <= start_index_from_end zero_if_absent: (Result = 0) = not substring (1, start_index_from_end).has_code (c) found_if_present: substring (1, start_index_from_end).has_code (c) implies code (Result) = c none_after: substring (1, start_index_from_end).has_code (c) implies not substring (Result + 1, start_index_from_end).has_code (c) new_cursor: STRING_8_ITERATION_CURSOR -- Fresh cursor associated with current structure -- (from READABLE_STRING_8) require -- from ITERABLE True ensure -- from ITERABLE result_attached: Result /= Void new_empty_string (suggested_capacity: INTEGER_32): like Current -- New empty string with same dynamic type as Current require non_negative_suggested_capacity: suggested_capacity >= 0 ensure new_string_not_void: Result /= Void same_type: Any_.same_types (Result, Current) new_string_empty: Result.count = 0 byte_count_set: Result.byte_count = 0 byte_capacity_set: Result.byte_capacity >= suggested_capacity Platform: KL_PLATFORM -- Platform-dependent properties -- (from KL_SHARED_PLATFORM) ensure -- from KL_SHARED_PLATFORM instance_free: class platform_not_void: Result /= Void plus alias "+" (other: READABLE_STRING_8): like Current -- New object which is a clone of Current extended -- by the characters of other -- (ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL argument_not_void: other /= Void compatible_strings: Is_string_8 implies other.Is_valid_as_string_8 ensure -- from READABLE_STRING_GENERAL plus_not_void: Result /= Void new_count: Result.count = count + other.count initial: Elks_checking implies Result.substring (1, count) ~ Current final: Elks_checking implies Result.substring (count + 1, count + other.count).same_string_general (other) ensure then final_unicode: Result.substring (count + 1, count + other.count).same_unicode_string (other) prefixed_string (other: STRING_8): like Current -- New object which is a clone of Current preceded -- by the characters of other require other_not_void: other /= Void ensure prefixed_string_not_void: Result /= Void prefixed_string_count: Result.count = other.count + count initial: Result.substring (1, other.count).same_unicode_string (other) final: Result.substring (other.count + 1, Result.count).is_equal (Current) string: STRING_8 -- New STRING having the same character sequence as Current -- where characters which do not fit in a CHARACTER are -- replaced by a '%U' -- (Extended from ELKS 2001 STRING) ensure -- from READABLE_STRING_8 string_not_void: Result /= Void string_type: Result.same_type (create {STRING_8}.make_empty) first_item: count > 0 implies Result.item (1) = item (1) recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).string string_representation: STRING_8 -- Similar to string but only create a new object if Current is not of dynamic type STRING_8. -- (from READABLE_STRING_8) ensure -- from READABLE_STRING_8 result_not_void: Result /= Void correct_type: Result.same_type (create {STRING_8}.make_empty) first_item: count > 0 implies Result.item (1) = item (1) recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).string substring (start_index, end_index: INTEGER_32): like Current -- New object containing all characters -- from start_index to end_index inclusive -- (ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL True ensure -- from READABLE_STRING_GENERAL substring_not_void: Result /= Void substring_count: Result.count = end_index - start_index + 1 or Result.count = 0 first_code: Result.count > 0 implies Result.character_32_item (1) = character_32_item (start_index) recurse: Result.count > 0 implies Result.substring (2, Result.count) ~ substring (start_index + 1, end_index) ensure then first_unicode_item: Result.count > 0 implies Result.item_code (1) = item_code (start_index) substring_index (other: STRING_8; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of other at or after start_index; -- 0 if none. other and Current are considered with their -- characters which do not fit in a CHARACTER replaced by a '%U' -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void valid_start_index: start_index >= 1 and start_index <= count + 1 ensure -- from READABLE_STRING_GENERAL valid_result: Result = 0 or else (start_index <= Result and Result <= count - other.count + 1) zero_if_absent: (Result = 0) = not substring (start_index, count).has_substring (other) at_this_index: Result >= start_index implies other.same_string_general (substring (Result, Result + other.count - 1)) none_before: Result > start_index implies not substring (start_index, Result + other.count - 2).has_substring (other) substring_index_in_bounds (other: READABLE_STRING_GENERAL; start_pos, end_pos: INTEGER_32): INTEGER_32 -- Position of first occurrence of other at or after start_pos -- and to or before end_pos; -- 0 if none. -- (from READABLE_STRING_8) require -- from READABLE_STRING_GENERAL other_nonvoid: other /= Void other_notempty: not other.is_empty start_pos_large_enough: start_pos >= 1 start_pos_small_enough: start_pos <= count end_pos_large_enough: end_pos >= start_pos end_pos_small_enough: end_pos <= count ensure -- from READABLE_STRING_GENERAL correct_place: Result > 0 implies other.same_string (substring (Result, Result + other.count - 1)) True_constant: STRING_8 = "true" -- Constant string "true" -- (from READABLE_STRING_GENERAL) Unicode: UC_UNICODE_ROUTINES -- Unicode routines -- (from UC_IMPORTED_UNICODE_ROUTINES) ensure -- from UC_IMPORTED_UNICODE_ROUTINES instance_free: class unicode_not_void: Result /= Void unicode_item (i: INTEGER_32): UC_CHARACTER -- Unicode character at index i; -- Return a new object at each call require valid_index: valid_index (i) ensure item_not_void: Result /= Void code_set: Result.code = item_code (i) unicode_substring_index (other: READABLE_STRING_GENERAL; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of other at or after start_index; -- 0 if none require other_not_void: other /= Void valid_start_index: start_index >= 1 and start_index <= count + 1 ensure valid_result: Result = 0 or else (start_index <= Result and Result <= count - other.count + 1) zero_if_absent: (Result = 0) = not substring (start_index, count).has_unicode_substring (other) at_this_index: Result >= start_index implies substring (Result, Result + other.count - 1).same_unicode_string (other) none_before: Result > start_index implies not substring (start_index, Result + other.count - 2).has_unicode_substring (other) Utf16: UC_UTF16_ROUTINES -- UTF-16 encoding routines -- (from UC_IMPORTED_UTF16_ROUTINES) ensure -- from UC_IMPORTED_UTF16_ROUTINES instance_free: class utf16_not_void: Result /= Void Utf32: UC_UTF32_ROUTINES -- UTF-32 encoding routines -- (from UC_IMPORTED_UTF32_ROUTINES) ensure -- from UC_IMPORTED_UTF32_ROUTINES instance_free: class utf32_not_void: Result /= Void Utf8: UC_UTF8_ROUTINES -- UTF-8 encoding routines -- (from UC_IMPORTED_UTF8_ROUTINES) ensure -- from UC_IMPORTED_UTF8_ROUTINES instance_free: class utf8_not_void: Result /= Void feature -- Measurement additional_space: INTEGER_32 -- Proposed number of additional items -- (from RESIZABLE) ensure -- from RESIZABLE at_least_one: Result >= 1 byte_capacity: INTEGER_32 -- Maximum number of bytes that can be put in -- internal storage require -- from READABLE_STRING_GENERAL True require -- from BOUNDED True ensure -- from READABLE_STRING_GENERAL capacity_non_negative: Result >= 0 ensure -- from BOUNDED capacity_non_negative: Result >= 0 byte_count: INTEGER_32 -- Number of bytes in internal storage code_occurrences (a_code: INTEGER_32): INTEGER_32 -- Number of times unicode character of code -- a_code appears in the string require valid_code: Unicode.valid_code (a_code) ensure zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then item_code (1) /= a_code) implies Result = substring (2, count).code_occurrences (a_code) recurse_if_found_at_first_position: (count > 0 and then item_code (1) = a_code) implies Result = 1 + substring (2, count).code_occurrences (a_code) count: INTEGER_32 -- Number of characters -- (ELKS 2001 STRING) Growth_percentage: INTEGER_32 = 50 -- Percentage by which structure will grow automatically -- (from RESIZABLE) Lower: INTEGER_32 = 1 -- Minimum index. -- (from READABLE_STRING_8) Minimal_increase: INTEGER_32 = 5 -- Minimal number of additional items -- (from RESIZABLE) occurrences (c: CHARACTER_8): INTEGER_32 -- Number of times character c appears in the string -- (ELKS 2001 STRING) require -- from BAG True require -- from READABLE_STRING_8 True ensure -- from BAG non_negative_occurrences: Result >= 0 ensure then -- from READABLE_STRING_8 zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then item (1) /= c) implies Result = substring (2, count).occurrences (c) recurse_if_found_at_first_position: (count > 0 and then item (1) = c) implies Result = 1 + substring (2, count).occurrences (c) character_32_occurrences (c: CHARACTER_32): INTEGER_32 -- Number of times c appears in the string -- (from READABLE_STRING_GENERAL) ensure then -- from READABLE_STRING_GENERAL zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then character_32_item (1) /= c) implies Result = substring (2, count).character_32_occurrences (c) recurse_if_found_at_first_position: (count > 0 and then character_32_item (1) = c) implies Result = 1 + substring (2, count).character_32_occurrences (c) unicode_occurrences (c: UC_CHARACTER): INTEGER_32 -- Number of times c appears in the string require c_not_void: c /= Void ensure zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then item_code (1) /= c.code) implies Result = substring (2, count).unicode_occurrences (c) recurse_if_found_at_first_position: (count > 0 and then item_code (1) = c.code) implies Result = 1 + substring (2, count).unicode_occurrences (c) 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) ends_with_general (s: READABLE_STRING_GENERAL): BOOLEAN -- Does string finish with s? -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL argument_not_void: s /= Void ensure -- from READABLE_STRING_GENERAL definition: Result = s.same_string (substring (count - s.count + 1, count)) 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)) is_case_insensitive_equal_general (other: READABLE_STRING_GENERAL): BOOLEAN -- Is string made of same character sequence as other regardless of casing -- (possibly with a different capacity)? -- (from READABLE_STRING_GENERAL) ensure -- from READABLE_STRING_GENERAL symmetric: Result implies other.is_case_insensitive_equal (Current) consistent: attached {UC_STRING} other as l_other implies (standard_is_equal (l_other) implies Result) valid_result: as_lower ~ other.as_lower implies Result frozen is_deep_equal (other: UC_STRING): 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: like Current): BOOLEAN -- Is other attached to an object considered equal -- to current object? -- (Extended from ELKS 2001 STRING) ensure then unicode_definition: Result = (Any_.same_types (Current, other) and then count = other.count and then (count > 0 implies (item_code (1) = other.item_code (1) and substring (2, count).is_equal (other.substring (2, count))))) old_is_equal (other: UC_STRING): BOOLEAN -- Is string made of same character sequence as other -- (possibly with a different capacity)? -- (from READABLE_STRING_8) require -- from ANY other_not_void: other /= Void ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result ensure then -- from COMPARABLE trichotomy: Result = (not (Current < other) and not (other < Current)) is_greater alias ">" (other: UC_STRING): BOOLEAN -- Is current object greater than other? -- (from COMPARABLE) require -- from PART_COMPARABLE other_exists: other /= Void ensure then -- from COMPARABLE definition: Result = (other < Current) is_greater_equal alias ">=" (other: UC_STRING): BOOLEAN -- Is current object greater than or equal to other? -- (from COMPARABLE) require -- from PART_COMPARABLE other_exists: other /= Void ensure then -- from COMPARABLE definition: Result = (other <= Current) is_less alias "<" (other: like Current): BOOLEAN -- Is string lexicographically lower than other? -- (Extended from ELKS 2001 STRING, inherited from COMPARABLE) ensure then unicode_definition: Result = (count = 0 and other.count > 0 or count > 0 and then other.count > 0 and then (item_code (1) < other.item_code (1) or item_code (1) = other.item_code (1) and substring (2, count) < other.substring (2, other.count))) old_infix_less (other: UC_STRING): BOOLEAN -- Is string lexicographically lower than other? -- (from READABLE_STRING_8) require -- from PART_COMPARABLE other_exists: other /= Void ensure then -- from COMPARABLE asymmetric: Result implies not (other < Current) is_less_equal alias "<=" (other: UC_STRING): BOOLEAN -- Is current object less than or equal to other? -- (from COMPARABLE) require -- from PART_COMPARABLE other_exists: other /= Void ensure then -- from COMPARABLE definition: Result = ((Current < other) or (Current ~ other)) max (other: UC_STRING): UC_STRING -- The greater of current object and other -- (from COMPARABLE) require -- from COMPARABLE other_exists: other /= Void ensure -- from COMPARABLE current_if_not_smaller: Current >= other implies Result = Current other_if_smaller: Current < other implies Result = other min (other: UC_STRING): UC_STRING -- The smaller of current object and other -- (from COMPARABLE) require -- from COMPARABLE other_exists: other /= Void ensure -- from COMPARABLE current_if_not_greater: Current <= other implies Result = Current other_if_greater: Current > other implies Result = other same_caseless_characters (other: READABLE_STRING_8; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- caseless identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) ensure -- from READABLE_STRING_8 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).is_case_insensitive_equal (other.substring (start_pos, end_pos)) same_caseless_characters_general (other: READABLE_STRING_GENERAL; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- caseless identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) ensure -- from READABLE_STRING_GENERAL same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).is_case_insensitive_equal_general (other.substring (start_pos, end_pos)) same_characters (other: READABLE_STRING_8; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) ensure -- from READABLE_STRING_8 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).same_string (other.substring (start_pos, end_pos)) same_characters_general (other: READABLE_STRING_GENERAL; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) ensure -- from READABLE_STRING_GENERAL same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).same_string_general (other.substring (start_pos, end_pos)) same_string (other: READABLE_STRING_8): BOOLEAN -- Do Current and other have the same character sequence? -- Current is considered with its characters which do not -- fit in a CHARACTER replaced by a '%U'. -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_8 other_not_void: other /= Void ensure -- from READABLE_STRING_8 definition: Result = (string ~ other.string) same_string_general (other: READABLE_STRING_GENERAL): BOOLEAN -- Do Current and other have the same character sequence? -- Current is considered with its characters which do not -- fit in a CHARACTER replaced by a '%U'. -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void same_unicode_string (other: READABLE_STRING_GENERAL): BOOLEAN -- Do Current and other have the same unicode character sequence? require other_not_void: other /= Void ensure definition: Result = (count = other.count and then (count > 0 implies (code (1) = other.code (1) and (count >= 2 implies substring (2, count).same_unicode_string (other.substring (2, count)))))) 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 (other: UC_STRING): 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) starts_with_general (s: READABLE_STRING_GENERAL): BOOLEAN -- Does string begin with s? -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL argument_not_void: s /= Void ensure -- from READABLE_STRING_GENERAL definition: Result = s.same_string (substring (1, s.count)) three_way_comparison (other: like Current): INTEGER_32 -- If current object equal to other, 0; -- if smaller, -1; if greater, 1 -- (ELKS 2001 STRING, inherited from COMPARABLE) -- Note: there is a bug in the specification of the -- contracts of three_way_comparison inherited -- from COMPARABLE. This routine cannot satisfy -- its postconditions if other is not of the -- same type as Current because the postcondition -- uses is_equal and is_equal has a postcondition -- inherited from ANY which says if it returns true -- then other has the same type as Current. require -- from COMPARABLE other_exists: other /= Void ensure -- from COMPARABLE equal_zero: (Result = 0) = (Current ~ other) smaller_negative: (Result = -1) = (Current < other) greater_positive: (Result = 1) = (Current > other) three_way_unicode_comparison (other: STRING_8): INTEGER_32 -- If current object equal to other, 0; -- if smaller, -1; if greater, 1 -- Note: there is a bug in the specification of the -- contracts of three_way_comparison inherited -- from COMPARABLE. This routine cannot satisfy -- its postconditions if other is not of the -- same type as Current because the postcondition -- uses is_equal and is_equal has a postcondition -- inherited from ANY which says if it returns true -- then other has the same type as Current. -- three_way_unicode_comparison solves this problem -- and make the comparison polymorphically safe by -- changing the signature from 'like Current' to -- 'STRING' and by using same_unicode_string instead -- of is_equal in its postcondition. require other_not_void: other /= Void ensure equal_zero: (Result = 0) = same_unicode_string (other) feature -- Status report Changeable_comparison_criterion: BOOLEAN = False -- May object_comparison be changed? -- (Answer: yes by default.) -- (from STRING_8) 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 ends_with (s: READABLE_STRING_8): BOOLEAN -- Does string finish with s? -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 argument_not_void: s /= Void ensure -- from READABLE_STRING_8 definition: Result = s.same_string (substring (count - s.count + 1, count)) Extendible: BOOLEAN = True -- May new items be added? (Answer: yes.) -- (from STRING_8) full: BOOLEAN -- Is structure full? -- (from BOUNDED) character_32_has (c: like character_32_item): BOOLEAN -- Does string include c? -- (from READABLE_STRING_GENERAL) ensure then -- from READABLE_STRING_GENERAL false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then character_32_item (1) = c implies Result recurse: (count > 0 and then character_32_item (1) /= c) implies (Result = substring (2, count).character_32_has (c)) has (c: CHARACTER_8): BOOLEAN -- Does Current contain character c? -- (ELKS 2001 STRING) require -- from CONTAINER True require -- from READABLE_STRING_8 True ensure -- from CONTAINER not_found_in_empty: Result implies not old_is_empty ensure -- from READABLE_STRING_8 false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then item (1) = c implies Result recurse: (count > 0 and then item (1) /= c) implies (Result = substring (2, count).has (c)) has_item_code (a_code: INTEGER_32): BOOLEAN -- Does Current contain the unicode character of code a_code? require valid_code: Unicode.valid_code (a_code) ensure false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then item_code (1) = a_code implies Result recurse: (count > 0 and then item_code (1) /= a_code) implies (Result = substring (2, count).has_item_code (a_code)) has_substring (other: STRING_8): BOOLEAN -- Does Current contain other? -- other and Current are considered with their characters -- which do not fit in a CHARACTER replaced by a '%U'. -- (Extented from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void ensure -- from READABLE_STRING_GENERAL false_if_too_small: count < other.count implies not Result true_if_initial: (count >= other.count and then other.same_string_general (substring (1, other.count))) implies Result recurse: (count >= other.count and then not other.same_string_general (substring (1, other.count))) implies (Result = substring (2, count).has_substring (other)) has_unicode (c: UC_CHARACTER): BOOLEAN -- Does Current contain c? require c_not_void: c /= Void ensure false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then item_code (1) = c.code implies Result recurse: (count > 0 and then item_code (1) /= c.code) implies (Result = substring (2, count).has_unicode (c)) has_unicode_substring (other: READABLE_STRING_GENERAL): BOOLEAN -- Does Current contain other? require other_not_void: other /= Void ensure false_if_too_small: count < other.count implies not Result true_if_initial: (count >= other.count and then substring (1, other.count).same_unicode_string (other)) implies Result recurse: (count >= other.count and then not substring (1, other.count).same_unicode_string (other)) implies (Result = substring (2, count).has_unicode_substring (other)) is_ascii: BOOLEAN -- Does string contain only ASCII characters? ensure empty: count = 0 implies Result recurse: count > 0 implies Result = (unicode_item (1).is_ascii and substring (2, count).is_ascii) is_boolean: BOOLEAN -- Does Current represent a BOOLEAN? -- (from READABLE_STRING_8) require -- from READABLE_STRING_GENERAL True ensure -- from READABLE_STRING_GENERAL is_boolean: Result = (True_constant.same_string_general (as_lower) or False_constant.same_string_general (as_lower)) is_closable: BOOLEAN -- Can current output stream be closed? -- (from KI_OUTPUT_STREAM) ensure -- from KI_OUTPUT_STREAM is_open: Result implies is_open_write is_double: BOOLEAN -- Does Current represent a REAL_64? -- Was declared in READABLE_STRING_GENERAL as synonym of is_real_64. -- (from READABLE_STRING_GENERAL) is_empty: BOOLEAN -- Is string empty? -- (ELKS 2001 STRING) old_is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) require -- from CONTAINER True require -- from READABLE_STRING_GENERAL True is_hashable: BOOLEAN -- May current object be hashed? -- (True by default.) -- (from HASHABLE) is_immutable: BOOLEAN -- Can the character sequence of Current be not changed? -- (from READABLE_STRING_GENERAL) is_inserted (v: CHARACTER_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) is_integer: BOOLEAN -- Does Current represent an INTEGER_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_integer_32. -- (from READABLE_STRING_GENERAL) is_integer_16: BOOLEAN -- Does Current represent an INTEGER_16? -- (from READABLE_STRING_GENERAL) is_integer_32: BOOLEAN -- Does Current represent an INTEGER_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_integer. -- (from READABLE_STRING_GENERAL) is_integer_64: BOOLEAN -- Does Current represent an INTEGER_64? -- (from READABLE_STRING_GENERAL) is_integer_8: BOOLEAN -- Does Current represent an INTEGER_8? -- (from READABLE_STRING_GENERAL) is_natural: BOOLEAN -- Does Current represent a NATURAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_natural_32. -- (from READABLE_STRING_GENERAL) is_natural_16: BOOLEAN -- Does Current represent a NATURAL_16? -- (from READABLE_STRING_GENERAL) is_natural_32: BOOLEAN -- Does Current represent a NATURAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_natural. -- (from READABLE_STRING_GENERAL) is_natural_64: BOOLEAN -- Does Current represent a NATURAL_64? -- (from READABLE_STRING_GENERAL) is_natural_8: BOOLEAN -- Does Current represent a NATURAL_8? -- (from READABLE_STRING_GENERAL) is_number_sequence: BOOLEAN -- Does Current represent a number sequence? -- (from READABLE_STRING_GENERAL) is_real: BOOLEAN -- Does Current represent a REAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_real_32. -- (from READABLE_STRING_GENERAL) is_real_32: BOOLEAN -- Does Current represent a REAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_real. -- (from READABLE_STRING_GENERAL) is_real_64: BOOLEAN -- Does Current represent a REAL_64? -- Was declared in READABLE_STRING_GENERAL as synonym of is_double. -- (from READABLE_STRING_GENERAL) is_real_sequence: BOOLEAN -- Does Current represent a real sequence? -- (from READABLE_STRING_GENERAL) Is_string_32: BOOLEAN = False -- Is Current a sequence of CHARACTER_32? -- (from READABLE_STRING_8) Is_string_8: BOOLEAN = True -- Is Current a sequence of CHARACTER_8? -- (from READABLE_STRING_8) is_substring_whitespace (start_index, end_index: INTEGER_32): BOOLEAN -- Is substring between start_index and end_index containing only whitespace characters? -- (from READABLE_STRING_8) require -- from READABLE_STRING_GENERAL start_index_big_enough: 1 <= start_index end_index_small_enough: end_index <= count consistent_indexes: start_index - 1 <= end_index Is_valid_as_string_8: BOOLEAN = True -- Is Current convertible to a sequence of CHARACTER_8 without information loss? -- (from READABLE_STRING_8) is_whitespace: BOOLEAN -- Is structure containing only whitespace characters? -- (from READABLE_STRING_GENERAL) object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) prunable: BOOLEAN -- May items be removed? (Answer: yes.) -- (from STRING_8) resizable: BOOLEAN -- May capacity be changed? (Answer: yes.) -- (from RESIZABLE) 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)) starts_with (s: READABLE_STRING_8): BOOLEAN -- Does string begin with s? -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 argument_not_void: s /= Void ensure -- from READABLE_STRING_8 definition: Result = s.same_string (substring (1, s.count)) valid_index (i: INTEGER_32): BOOLEAN -- Is i within the bounds of the string? -- (from READABLE_STRING_GENERAL) require -- from READABLE_INDEXABLE True require -- from TABLE True require -- from TO_SPECIAL True ensure -- from READABLE_INDEXABLE only_if_in_index_set: Result implies (Lower <= i and i <= count) ensure -- from READABLE_STRING_GENERAL definition: Result = (1 <= i and i <= count) 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 -- Element change adjust -- Remove leading and/or trailing whitespace. -- (from STRING_GENERAL) ensure -- from STRING_GENERAL valid_count: count <= old count new_count_left: not old_is_empty implies not character_32_item (1).is_space new_count_right: not old_is_empty implies not character_32_item (count).is_space kept: Elks_checking implies (old twin).has_substring (Current) only_spaces_removed_before: Elks_checking implies (old twin).is_substring_whitespace (1, (old twin).substring_index (Current, 1) - 1) only_spaces_removed_after: Elks_checking implies (old twin).is_substring_whitespace ((old twin).substring_index (Current, 1) + count, old count) append (a_string: READABLE_STRING_8) -- Append a copy of a_string at end. -- (ELKS 2001 STRING) require -- from STRING_8 argument_not_void: a_string /= Void ensure -- from STRING_8 new_count: count = old count + old a_string.count appended: Elks_checking implies same_string (old (Current + a_string)) append_boolean (b: BOOLEAN) -- Append the string representation of b at end. -- (from STRING_8) append_character (c: CHARACTER_8) -- Append character c at end. -- (ELKS 2001 STRING) require -- from KI_OUTPUT_STREAM is_open_write: is_open_write require -- from STRING_8 True ensure then -- from STRING_8 item_inserted: item (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) ensure then unicode_appended: item_code (count) = c.code append_double (d: REAL_64) -- Append the string representation of d at end. -- (from STRING_8) append_integer (i: INTEGER_32) -- Append the string representation of i at end. -- (from STRING_8) append_integer_16 (i: INTEGER_16) -- Append the string representation of i at end. -- (from STRING_8) append_integer_64 (i: INTEGER_64) -- Append the string representation of i at end. -- (from STRING_8) append_integer_8 (i: INTEGER_8) -- Append the string representation of i at end. -- (from STRING_8) append_item_code (a_code: INTEGER_32) -- Append unicode character of code a_code at end. require valid_item_code: Unicode.valid_code (a_code) ensure new_count: count = old count + 1 appended: item_code (count) = a_code stable_before: substring (1, count - 1).is_equal (old cloned_string) append_natural_16 (i: NATURAL_16) -- Append the string representation of i at end. -- (from STRING_8) append_natural_32 (i: NATURAL_32) -- Append the string representation of i at end. -- (from STRING_8) append_natural_64 (i: NATURAL_64) -- Append the string representation of i at end. -- (from STRING_8) append_natural_8 (i: NATURAL_8) -- Append the string representation of i at end. -- (from STRING_8) append_real (r: REAL_32) -- Append the string representation of r at end. -- (from STRING_8) append_string (s: detachable READABLE_STRING_8) -- Append a copy of s at end. ensure -- from STRING_8 appended: s /= Void implies (Elks_checking implies Current ~ (old twin + old s.twin)) append_string_general (s: READABLE_STRING_GENERAL) -- Append a copy of s at end. require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 ensure -- from STRING_GENERAL new_count: count = old count + old s.count appended: Elks_checking implies same_string_general (old (to_string_32 + s)) append_substring (s: READABLE_STRING_8; start_index, end_index: INTEGER_32) -- Append characters of s.substring (start_index, end_index) at end. -- (from STRING_8) require -- from STRING_8 argument_not_void: s /= Void start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 ensure -- from STRING_8 new_count: count = old count + (end_index - start_index + 1) appended: Elks_checking implies same_string (old (Current + s.substring (start_index, end_index))) append_substring_general (s: READABLE_STRING_GENERAL; start_index, end_index: INTEGER_32) -- Append characters of s.substring (start_index, end_index) at end. -- (from STRING_GENERAL) require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 ensure -- from STRING_GENERAL new_count: count = old count + end_index - start_index + 1 appended: Elks_checking implies same_string_general (old (to_string_32 + s.substring (start_index, end_index))) append_unicode_character (c: UC_CHARACTER) -- Append unicode character c at end. require c_not_void: c /= Void ensure new_count: count = old count + 1 appended: item_code (count) = c.code stable_before: substring (1, count - 1).is_equal (old cloned_string) append_utf16 (s: STRING_8) -- Append UTF-16 encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16: Utf16.valid_utf16 (s) append_utf16be (s: STRING_8) -- Append UTF-16BE encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16be: Utf16.valid_utf16be (s) append_utf16le (s: STRING_8) -- Append UTF-16LE encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16le: Utf16.valid_utf16le (s) append_utf8 (s: STRING_8) -- Append UTF-8 encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf8: Utf8.valid_utf8 (s) extend (c: CHARACTER_8) -- Append c at end. -- Was declared in STRING_8 as synonym of append_character. -- (from STRING_8) require -- from COLLECTION extendible: Extendible ensure -- from COLLECTION item_inserted: is_inserted (c) ensure then -- from STRING_8 item_inserted: item (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) fill (other: CONTAINER [CHARACTER_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 fill_blank -- Fill with capacity blank characters. -- (from STRING_8) ensure -- from STRING_8 filled: full same_size: (count = byte_capacity) and (byte_capacity = old byte_capacity) fill_character (c: CHARACTER_8) -- Fill with capacity characters all equal to c. -- (from READABLE_STRING_8) ensure -- from READABLE_STRING_8 filled: count = byte_capacity same_size: byte_capacity = old byte_capacity fill_with (c: CHARACTER_8) -- Replace every character with character c. -- (ELKS 2001 STRING) require -- from STRING_8 True ensure -- from STRING_8 same_count: (count = old count) and (byte_capacity = old byte_capacity) filled: Elks_checking implies occurrences (c) = count ensure then all_code: code_occurrences (c.code) = count fill_with_code (a_code: INTEGER_32) -- Replace every character with unicode character of code a_code. require valid_code: Unicode.valid_code (a_code) ensure same_count: old count = count filled: code_occurrences (a_code) = count fill_with_unicode (c: UC_CHARACTER) -- Replace every character with unicode character c. require c_not_void: c /= Void ensure same_count: old count = count filled: unicode_occurrences (c) = count gobo_append_substring (a_string: STRING_8; s, e: INTEGER_32) -- Append substring of a_string between indexes -- s and e at end of current string. require a_string_not_void: a_string /= Void s_large_enough: s >= 1 e_small_enough: e <= a_string.count valid_interval: s <= e + 1 ensure then appended: is_equal (old cloned_string + old a_string.substring (s, e)) insert_character (c: CHARACTER_8; i: INTEGER_32) -- Insert character c at index i, shifting -- characters between ranks i and count rightwards. -- (ELKS 2001 STRING) require -- from STRING_8 valid_insertion_index: 1 <= i and i <= count + 1 ensure -- from STRING_8 one_more_character: count = old count + 1 inserted: item (i) = c stable_before_i: Elks_checking implies substring (1, i - 1) ~ (old substring (1, i - 1)) stable_after_i: Elks_checking implies substring (i + 1, count) ~ (old substring (i, count)) ensure then code_inserted: item_code (i) = c.code insert_code (a_code: INTEGER_32; i: INTEGER_32) -- Insert unicode character of code a_code -- at index i, shifting characters between -- ranks i and count rightwards. require valid_code: Unicode.valid_code (a_code) valid_insertion_index: 1 <= i and i <= count + 1 ensure one_more_character: count = old count + 1 inserted: item_code (i) = a_code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i, count)) insert_string (a_string: READABLE_STRING_8; i: INTEGER_32) -- Insert a_string at index i, shifting characters between ranks -- i and count rightwards. -- (ELKS 2001 STRING) require -- from STRING_8 string_exists: a_string /= Void valid_insertion_index: 1 <= i and i <= count + 1 require else string_not_void: a_string /= Void valid_insertion_index: 1 <= i and i <= count + 1 ensure -- from STRING_8 inserted: Elks_checking implies (Current ~ (old substring (1, i - 1) + old (a_string.twin) + old substring (i, count))) insert_unicode_character (c: UC_CHARACTER; i: INTEGER_32) -- Insert unicode character c at index i, shifting -- characters between ranks i and count rightwards. require c_not_void: c /= Void valid_insertion_index: 1 <= i and i <= count + 1 ensure one_more_character: count = old count + 1 inserted: item_code (i) = c.code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i, count)) precede (c: CHARACTER_8) -- Add c at front. -- Was declared in STRING_8 as synonym of prepend_character. -- (from STRING_8) ensure -- from STRING_8 new_count: count = old count + 1 prepend (s: READABLE_STRING_8) -- Prepend a copy of s at front. require -- from STRING_8 argument_not_void: s /= Void ensure -- from STRING_8 new_count: count = old (count + s.count) inserted: Elks_checking implies same_string (old (s + Current)) prepend_boolean (b: BOOLEAN) -- Prepend the string representation of b at front. -- (from STRING_8) prepend_character (c: CHARACTER_8) -- Add c at front. -- Was declared in STRING_8 as synonym of precede. -- (from STRING_8) ensure -- from STRING_8 new_count: count = old count + 1 prepend_double (d: REAL_64) -- Prepend the string representation of d at front. -- (from STRING_8) prepend_integer (i: INTEGER_32) -- Prepend the string representation of i at front. -- (from STRING_8) prepend_real (r: REAL_32) -- Prepend the string representation of r at front. -- (from STRING_8) prepend_string (s: detachable STRING_8) -- Prepend a copy of s, if not void, at front. prepend_string_general (s: READABLE_STRING_GENERAL) -- Prepend characters of s at front. -- (from STRING_8) require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 ensure -- from STRING_GENERAL new_count: count = old (count + s.count) inserted: Elks_checking implies same_string_general (old (s.to_string_32 + Current)) prepend_substring (s: READABLE_STRING_8; start_index, end_index: INTEGER_32) -- Prepend characters of s.substring (start_index, end_index) at front. -- (from STRING_8) require -- from STRING_8 argument_not_void: s /= Void start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 ensure -- from STRING_8 new_count: count = old count + end_index - start_index + 1 inserted: Elks_checking implies same_string (old (s.substring (start_index, end_index) + Current)) prepend_substring_general (s: READABLE_STRING_GENERAL; start_index, end_index: INTEGER_32) -- Prepend characters of s.substring (start_index, end_index) at front. -- (from STRING_GENERAL) require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 ensure -- from STRING_GENERAL new_count: count = old count + end_index - start_index + 1 inserted: Elks_checking implies same_string_general (old (s.substring (start_index, end_index).to_string_32 + Current)) put (c: CHARACTER_8; i: INTEGER_32) -- Replace unicode character at index i by character c. -- (ELKS 2001 STRING) ensure then unicode_replaced: item_code (i) = c.code put_item_code (a_code: INTEGER_32; i: INTEGER_32) -- Replace unicode character at index i -- by unicode character of code a_code. require valid_index: valid_index (i) valid_item_code: Unicode.valid_code (a_code) ensure stable_count: count = old count replaced: item_code (i) = a_code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i + 1, count)) put_string (a_string: STRING_8) -- Write a_string to output stream. require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write a_string_not_void: a_string /= Void put_substring (a_string: STRING_8; s, e: INTEGER_32) -- Write substring of a_string between indexes -- s and e to output stream. require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write a_string_not_void: a_string /= Void s_large_enough: s >= 1 e_small_enough: e <= a_string.count valid_interval: s <= e + 1 put_unicode (c: UC_CHARACTER; i: INTEGER_32) -- Replace unicode character at index i by c. require valid_index: valid_index (i) c_not_void: c /= Void ensure stable_count: count = old count replaced: item_code (i) = c.code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i + 1, count)) replace_blank -- Replace all current characters with blanks. -- (from STRING_8) ensure -- from STRING_8 same_size: (count = old count) and (byte_capacity = old byte_capacity) all_blank: Elks_checking implies occurrences (' ') = count replace_substring (a_string: STRING_8; start_index, end_index: INTEGER_32) -- Replace the substring from start_index to end_index, -- inclusive, with a_string. -- (ELKS 2001 STRING) require -- from STRING_8 string_not_void: a_string /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningfull_interval: start_index <= end_index + 1 ensure -- from STRING_8 new_count: count = old count + old a_string.count - end_index + start_index - 1 replaced: Elks_checking implies (Current ~ (old (substring (1, start_index - 1) + a_string + substring (end_index + 1, count)))) replace_substring_all (original, new: like Current) -- Replace every occurrence of original with new. require -- from STRING_8 original_exists: original /= Void new_exists: new /= Void original_not_empty: not original.old_is_empty replace_substring_by_string (a_string: STRING_8; start_index, end_index: INTEGER_32) -- Replace the substring from start_index to end_index, -- inclusive, with a_string. require a_string_not_void: a_string /= Void set (t: READABLE_STRING_8; n1, n2: INTEGER_32) -- Set current string to substring of t from indices n1 -- to n2, or to empty string if no such substring. -- (from STRING_8) require -- from STRING_8 argument_not_void: t /= Void ensure -- from STRING_8 is_substring: same_string (t.substring (n1, n2)) subcopy (other: READABLE_STRING_8; start_pos, end_pos, index_pos: INTEGER_32) -- Copy characters of other within bounds start_pos and -- end_pos to current string starting at index index_pos. -- (from STRING_8) require -- from STRING_8 other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) enough_space: (count - index_pos) >= (end_pos - start_pos) ensure -- from STRING_8 same_count: count = old count copied: Elks_checking implies (Current ~ (old substring (1, index_pos - 1) + old other.substring (start_pos, end_pos) + old substring (index_pos + (end_pos - start_pos + 1), count))) feature -- Removal keep_head (n: INTEGER_32) -- Remove all the characters except for the first n; -- if n > count, do nothing. -- (ELKS 2001 STRING) require -- from STRING_GENERAL non_negative_argument: n >= 0 ensure -- from STRING_GENERAL new_count: count = n.min (old count) kept: Elks_checking implies Current ~ (old substring (1, n.min (count))) keep_tail (n: INTEGER_32) -- Remove all the characters except for the last n; -- if n > count, do nothing. -- (ELKS 2001 STRING) require -- from STRING_GENERAL non_negative_argument: n >= 0 ensure -- from STRING_GENERAL new_count: count = n.min (old count) kept: Elks_checking implies Current ~ (old substring (count - n.min (count) + 1, count)) prune (c: CHARACTER_8) -- Remove first occurrence of c, if any. -- (from STRING_8) require -- from COLLECTION prunable: prunable require else -- from STRING_8 True prune_all (c: CHARACTER_8) -- Remove all occurrences of c. -- (from STRING_8) require -- from COLLECTION prunable: prunable require else -- from STRING_8 True ensure -- from COLLECTION no_more_occurrences: not has (c) ensure then -- from STRING_8 changed_count: count = (old count) - (old occurrences (c)) prune_all_leading (c: CHARACTER_8) -- Remove all leading occurrences of c. -- (from STRING_8) prune_all_trailing (c: CHARACTER_8) -- Remove all trailing occurrences of c. -- (from STRING_8) remove (i: INTEGER_32) -- Remove i-th character, shifting characters between -- ranks i + 1 and count leftwards. -- (ELKS 2001 STRING) require -- from STRING_GENERAL valid_index: valid_index (i) ensure -- from STRING_GENERAL new_count: count = old count - 1 removed: Elks_checking implies to_string_32 ~ (old substring (1, i - 1).to_string_32 + old substring (i + 1, count).to_string_32) remove_head (n: INTEGER_32) -- Remove the first n characters; -- if n > count, remove all. -- (ELKS 2001 STRING) require -- from STRING_GENERAL n_non_negative: n >= 0 ensure -- from STRING_GENERAL removed: Elks_checking implies Current ~ (old substring (n.min (count) + 1, count)) remove_substring (start_index, end_index: INTEGER_32) -- Remove all characters from start_index -- to end_index inclusive. -- (ELKS 2001 STRING) require -- from STRING_GENERAL valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningful_interval: start_index <= end_index + 1 ensure -- from STRING_GENERAL removed: Elks_checking implies Current ~ (old substring (1, start_index - 1) + old substring (end_index + 1, count)) remove_tail (n: INTEGER_32) -- Remove the last n characters; -- if n > count, remove all. -- (ELKS 2001 STRING) require -- from STRING_GENERAL n_non_negative: n >= 0 ensure -- from STRING_GENERAL removed: Elks_checking implies Current ~ (old substring (1, count - n.min (count))) wipe_out -- Remove all characters. -- (ELKS 2001 STRING) feature -- Resizing adapt_size -- Adapt the size to accommodate count characters. -- (from STRING_8) automatic_grow -- Change the capacity to accommodate at least -- Growth_percentage more items. -- (from RESIZABLE) require -- from RESIZABLE resizable: resizable ensure -- from RESIZABLE increased_capacity: byte_capacity >= old byte_capacity + old additional_space grow (newsize: INTEGER_32) -- Ensure that the capacity is at least newsize. -- (from STRING_8) require -- from RESIZABLE resizable: resizable ensure -- from RESIZABLE new_capacity: byte_capacity >= newsize resize (newsize: INTEGER_32) -- Rearrange string so that it can accommodate -- at least newsize characters. -- (from STRING_8) require -- from STRING_GENERAL new_size_large_enough: newsize >= count ensure -- from STRING_GENERAL same_count: count = old count capacity_large_enough: byte_capacity >= newsize same_content: Elks_checking implies same_string_general (old twin) trim -- Decrease capacity to the minimum value. -- Apply to reduce allocated storage. -- (from STRING_8) require -- from RESIZABLE True ensure -- from RESIZABLE same_count: count = old count minimal_capacity: byte_capacity = count ensure then -- from STRING_8 same_string: same_string (old twin) feature -- Transformation correct_mismatch -- Attempt to correct object mismatch during retrieve using Mismatch_information. -- (from STRING_8) feature -- Conversion as_lower: like Current -- New object with all letters in lower case -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL True ensure -- from READABLE_STRING_GENERAL as_lower_attached: Result /= Void length: Result.count = count anchor: count > 0 implies Result.character_32_item (1) = character_32_item (1).as_lower recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).as_lower ensure then unicode_anchor: count > 0 implies Result.unicode_item (1).is_equal (unicode_item (1).as_lower) unicode_recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_lower) as_string: STRING_8 -- STRING version of current string; -- Return the UTF8 representation if it is encoded -- with UTF8, the UTF16 representation if it is -- encoded with UTF16, etc. ensure as_string_not_void: Result /= Void string_type: Any_.same_types (Result, "") as_string_32: STRING_32 -- Convert Current as a STRING_32. -- Was declared in READABLE_STRING_GENERAL as synonym of to_string_32. -- (from READABLE_STRING_GENERAL) ensure -- from READABLE_STRING_GENERAL as_string_32_not_void: Result /= Void identity: (conforms_to (create {STRING_32}.make_empty) and Result = Current) or (not conforms_to (create {STRING_32}.make_empty) and Result /= Current) as_string_8: STRING_8 -- Convert Current as a STRING_8. If a code of Current is -- not a valid code for a STRING_8 it is replaced with the null -- character. -- (from READABLE_STRING_GENERAL) ensure -- from READABLE_STRING_GENERAL as_string_8_not_void: Result /= Void identity: (conforms_to ("") and Result = Current) or (not conforms_to ("") and Result /= Current) as_upper: like Current -- New object with all letters in upper case -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL True ensure -- from READABLE_STRING_GENERAL as_upper_attached: Result /= Void length: Result.count = count anchor: count > 0 implies Result.character_32_item (1) = character_32_item (1).as_upper recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).as_upper ensure then unicode_anchor: count > 0 implies Result.unicode_item (1).is_equal (unicode_item (1).as_upper) unicode_recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_upper) center_justify -- Center justify Current using count as width. -- (from STRING_8) character_justify (pivot: CHARACTER_8; position: INTEGER_32) -- Justify a string based on a pivot -- and the position it needs to be in -- the final string. -- This will grow the string if necessary -- to get the pivot in the correct place. -- (from STRING_8) require -- from STRING_8 valid_position: position <= byte_capacity positive_position: position >= 1 pivot_not_space: pivot /= ' ' not_empty: not old_is_empty left_justify -- Left justify Current using count as witdth. -- (from STRING_8) linear_representation: LINEAR [CHARACTER_8] -- Representation as a linear structure -- (from STRING_8) mirrored: UC_STRING -- Mirror image of string; -- Result for "Hello world" is "dlrow olleH". -- (from STRING_8) ensure -- from READABLE_STRING_8 same_count: Result.count = count right_justify -- Right justify Current using count as width. -- (from STRING_8) ensure -- from STRING_8 same_count: count = old count split (a_separator: CHARACTER_32): LIST [UC_STRING] -- Split on a_separator. -- (from READABLE_STRING_GENERAL) ensure -- from READABLE_STRING_GENERAL Result /= Void to_boolean: BOOLEAN -- Boolean value; -- "True" yields True, "False" yields False -- (case-insensitive) -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_boolean: is_boolean ensure -- from READABLE_STRING_GENERAL to_boolean: (Result = as_lower.same_string_general (True_constant)) or (not Result = as_lower.same_string_general (False_constant)) frozen to_c: ANY -- A reference to a C form of current string. -- Useful only for interfacing with C software. -- (from STRING_8) require -- from STRING_8 not_is_dotnet: not {PLATFORM}.is_dotnet frozen to_cil: SYSTEM_STRING -- Create an instance of SYSTEM_STRING using characters -- of Current between indices 1 and count. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_dotnet: {PLATFORM}.is_dotnet ensure -- from READABLE_STRING_GENERAL to_cil_not_void: Result /= Void to_double: REAL_64 -- "Double" value; -- for example, when applied to "123.0", will yield 123.0 (double) -- Was declared in READABLE_STRING_GENERAL as synonym of to_real_64. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_double: is_double to_integer: INTEGER_32 -- 32-bit integer value -- Was declared in READABLE_STRING_GENERAL as synonym of to_integer_32. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer: is_integer_32 to_integer_16: INTEGER_16 -- 16-bit integer value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer_16: is_integer_16 to_integer_32: INTEGER_32 -- 32-bit integer value -- Was declared in READABLE_STRING_GENERAL as synonym of to_integer. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer: is_integer_32 to_integer_64: INTEGER_64 -- 64-bit integer value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer_64: is_integer_64 to_integer_8: INTEGER_8 -- 8-bit integer value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer_8: is_integer_8 to_lower -- Convert all letters to lower case. -- (ELKS 2001 STRING) ensure -- from STRING_8 length_and_content: Elks_checking implies Current ~ (old as_lower) to_natural: NATURAL_32 -- 32-bit natural value -- Was declared in READABLE_STRING_GENERAL as synonym of to_natural_32. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural: is_natural_32 to_natural_16: NATURAL_16 -- 16-bit natural value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural_16: is_natural_16 to_natural_32: NATURAL_32 -- 32-bit natural value -- Was declared in READABLE_STRING_GENERAL as synonym of to_natural. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural: is_natural_32 to_natural_64: NATURAL_64 -- 64-bit natural value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural_64: is_natural_64 to_natural_8: NATURAL_8 -- 8-bit natural value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural_8: is_natural_8 to_real: REAL_32 -- Real value; -- for example, when applied to "123.0", will yield 123.0 -- Was declared in READABLE_STRING_GENERAL as synonym of to_real_32. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_real: is_real to_real_32: REAL_32 -- Real value; -- for example, when applied to "123.0", will yield 123.0 -- Was declared in READABLE_STRING_GENERAL as synonym of to_real. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_real: is_real to_real_64: REAL_64 -- "Double" value; -- for example, when applied to "123.0", will yield 123.0 (double) -- Was declared in READABLE_STRING_GENERAL as synonym of to_double. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_double: is_double to_string_8: STRING_8 -- Convert Current as a STRING_8. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_valid_as_string_8: Is_valid_as_string_8 ensure -- from READABLE_STRING_GENERAL as_string_8_not_void: Result /= Void identity: (conforms_to ("") and Result = Current) or (not conforms_to ("") and Result /= Current) to_upper -- Convert all letters to upper case. -- (ELKS 2001 STRING) ensure -- from STRING_8 length_and_content: Elks_checking implies Current ~ (old as_upper) to_utf16_be: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-16BE representation of current string ensure to_utf16_be_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf16: Utf16.valid_utf16 (Result) to_utf16_le: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-16LE representation of current string ensure to_utf16_le_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf16: Utf16.valid_utf16 (Utf16.Bom_le + Result) to_utf32_be: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-32BE representation of current string ensure to_utf32_be_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf32: Utf32.valid_utf32 (Result) to_utf32_le: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-32LE representation of current string ensure to_utf32_le_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf32: Utf32.valid_utf32 (Utf32.Bom_le + Result) to_utf8: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-8 representation of current string ensure to_utf8_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf8: Utf8.valid_utf8 (Result) feature -- Duplication cloned_string: like Current -- New object equal to Current ensure twin_not_void: Result /= Void is_equal: Result.is_equal (Current) copy (other: like Current) -- Reinitialize by copying the characters of other. -- (This is also used by clone.) -- (ELKS 2001 STRING) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) ensure -- from ANY is_equal: Current ~ other ensure then -- from READABLE_STRING_8 new_result_count: count = other.count frozen deep_copy (other: UC_STRING) -- 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: UC_STRING -- New object structure recursively duplicated from Current. -- (from ANY) ensure -- from ANY deep_twin_not_void: Result /= Void deep_equal: deep_equal (Current, Result) head (n: INTEGER_32): UC_STRING -- Prefix, retaining first n characters (or as many as available). -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL non_negative_argument: n >= 0 ensure -- from READABLE_STRING_GENERAL same_count: count = old count new_count: Result.count = n.min (count) multiply (n: INTEGER_32) -- Duplicate a string within itself -- ("hello").multiply(3) => "hellohellohello" -- (from STRING_8) require -- from STRING_8 meaningful_multiplier: n >= 1 frozen standard_copy (other: UC_STRING) -- 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: UC_STRING -- 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) tail (n: INTEGER_32): UC_STRING -- Suffix, retaining last n characters (or as many as available). -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL non_negative_argument: n >= 0 ensure -- from READABLE_STRING_GENERAL same_count: count = old count new_count: Result.count = n.min (count) frozen twin: UC_STRING -- 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 close -- Try to close output stream if it is closable. Set -- is_open_write to false if operation was successful. -- (from KI_OUTPUT_STREAM) require -- from KI_OUTPUT_STREAM is_closable: is_closable frozen default: detachable UC_STRING -- 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 -- Implementation current_string: STRING_8 -- Current string feature -- Access: Cursor new_character_32_cursor: STRING_ITERATION_CURSOR -- Fresh cursor for this string that iterates over code points (see code) -- exposed as CHARACTER_32. -- (from READABLE_STRING_GENERAL) feature -- Correction Mismatch_information: MISMATCH_INFORMATION -- Original attribute values of mismatched object -- (from MISMATCH_CORRECTOR) feature -- Output append_stream (an_input_stream: KI_INPUT_STREAM [CHARACTER_8]) -- Read items of an_input_stream until the end -- of input is reached, and write these items to -- current output stream. -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_OUTPUT_STREAM is_open_write: is_open_write an_input_stream_not_void: an_input_stream /= Void an_input_stream_open_read: an_input_stream.is_open_read ensure -- from KI_OUTPUT_STREAM end_of_input: an_input_stream.end_of_input debug_output: STRING_8 -- String that should be displayed in debugger to represent Current. ensure -- from DEBUG_OUTPUT result_not_void: Result /= Void Io: STD_FILES -- Handle to standard file setup -- (from ANY) ensure -- from ANY instance_free: class io_not_void: Result /= Void out: STRING_8 -- New STRING containing terse printable representation -- of current object; Non-ascii characters are represented -- with the %/code/ convention. -- (ELKS 2001 STRING) require -- from ANY True ensure -- from ANY out_not_void: Result /= Void ensure then -- from READABLE_STRING_8 out_not_void: Result /= Void same_items: same_type ("") implies Result.same_string (Current) print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) ensure -- from ANY instance_free: class put_boolean (b: BOOLEAN) -- Write "True" to output stream if -- b is true, "False" otherwise. -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_integer (i: INTEGER_32) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_integer_16 (i: INTEGER_16) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_integer_32 (i: INTEGER_32) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_integer_64 (i: INTEGER_64) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_integer_8 (i: INTEGER_8) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_line (a_string: STRING_8) -- Write a_string to output stream -- followed by a line separator. -- (from KI_TEXT_OUTPUT_STREAM) require -- from KI_TEXT_OUTPUT_STREAM is_open_write: is_open_write a_string_not_void: a_string /= Void put_natural_16 (i: NATURAL_16) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_natural_32 (i: NATURAL_32) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_natural_64 (i: NATURAL_64) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_natural_8 (i: NATURAL_8) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write put_new_line -- Write a line separator to output stream. -- (from KI_TEXT_OUTPUT_STREAM) require -- from KI_TEXT_OUTPUT_STREAM is_open_write: is_open_write 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 -- Output stream Eol: STRING_8 = "%N" -- Line separator flush -- Do nothing (operation does not apply to string). require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write is_open_write: BOOLEAN -- Can characters be written to output stream? Name: STRING_8 = "UC_STRING" -- Name of output stream 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 -- Traversal byte_index (i: INTEGER_32): INTEGER_32 -- Byte index of character at index i require valid_index: valid_index (i) ensure byte_index_large_enough: Result >= 1 byte_index_small_enough: Result <= byte_count is_encoded_first_byte: is_encoded_first_byte (Result) character_item_at_byte_index (i: INTEGER_32): CHARACTER_8 -- Character at byte_index i; -- '%U' is the unicode character at byte index -- i cannot fit into a CHARACTER require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) ensure code_small_enough: item_code_at_byte_index (i) <= Platform.Maximum_character_code implies Result.code = item_code_at_byte_index (i) overflow: item_code_at_byte_index (i) > Platform.Maximum_character_code implies Result = '%U' is_encoded_first_byte (i: INTEGER_32): BOOLEAN -- Is byte at index i the first byte of an encoded unicode character? require i_large_enough: i >= 1 i_small_enough: i <= byte_count item_code_at_byte_index (i: INTEGER_32): INTEGER_32 -- Code of character at byte index i require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) ensure valid_item_code: Unicode.valid_code (Result) next_byte_index (i: INTEGER_32): INTEGER_32 -- Byte index of unicode character after character -- at byte index i; Return 'byte_count + 1' if -- character at byte index i is the last character -- in the string require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) ensure next_byte_index_large_enough: Result > i next_byte_index_small_enough: Result <= byte_count + 1 shifted_byte_index (i: INTEGER_32; n: INTEGER_32): INTEGER_32 -- Byte index of unicode character n positions after -- character at byte index i; Return 'byte_count + 1' -- if no such character in the string require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) n_positive: n >= 0 ensure next_byte_index_large_enough: Result >= i next_byte_index_small_enough: Result <= byte_count + 1 invariant non_negative_byte_count: byte_count >= 0 byte_count_small_enough: byte_count <= byte_capacity count_small_enough: count <= byte_count -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from STRING_8 extendible: Extendible compare_character: not object_comparison -- from READABLE_STRING_8 area_not_void: area /= Void -- from COMPARABLE irreflexive_comparison: not (Current < Current) -- from READABLE_INDEXABLE consistent_boundaries: Lower <= count or else Lower = count + 1 -- from STRING_GENERAL mutable: not is_immutable -- from RESIZABLE increase_by_at_least_one: Minimal_increase >= 1 -- from BOUNDED valid_count: count <= byte_capacity full_definition: full = (count = byte_capacity) -- from FINITE empty_definition: old_is_empty = (count = 0) end -- class UC_STRING
Generated by ISE EiffelStudio