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