note description: "Common ancestors to all STRING classes." library: "Free implementation of ELKS library" status: "See notice at end of class." legal: "See notice at end of class." date: "$Date: 2020-05-12 20:58:01 +0000 (Tue, 12 May 2020) $" revision: "$Revision: 104181 $" deferred class interface STRING_GENERAL convert as_string_32: {READABLE_STRING_32, STRING_32}, to_cil: {SYSTEM_STRING} feature -- Element change put_code (v: like code; i: INTEGER_32) -- Put code v at position i. require valid_code: valid_code (v) valid_index: valid_index (i) ensure inserted: code (i) = v stable_count: count = old count 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 + 1, count)) append_code (c: like code) -- Append c at end. require valid_code: valid_code (c) ensure then item_inserted: code (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) append_integer_8 (i: INTEGER_8) -- Append the string representation of i at end. append_integer_16 (i: INTEGER_16) -- Append the string representation of i at end. append_integer (i: INTEGER_32) -- Append the string representation of i at end. append_integer_64 (i: INTEGER_64) -- Append the string representation of i at end. append_natural_8 (i: NATURAL_8) -- Append the string representation of i at end. append_natural_16 (i: NATURAL_16) -- Append the string representation of i at end. append_natural_32 (i: NATURAL_32) -- Append the string representation of i at end. append_real (r: REAL_32) -- Append the string representation of r at end. append_double (d: REAL_64) -- Append the string representation of d at end. append_boolean (b: BOOLEAN) -- Append the string representation of b at end. append (s: READABLE_STRING_GENERAL) -- Append characters of s at end. require argument_not_void: s /= Void compatible_strings: is_string_8 implies s.is_valid_as_string_8 ensure new_count: count = old count + old s.count appended: Elks_checking implies same_string (old (to_string_32 + s.as_string_32)) append_substring (s: READABLE_STRING_GENERAL; start_index, end_index: INTEGER_32) -- Append characters of s.substring (start_index, end_index) at end. require 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 new_count: count = old count + end_index - start_index + 1 appended: Elks_checking implies same_string (old (to_string_32 + s.substring (start_index, end_index).as_string_32)) prepend (s: READABLE_STRING_GENERAL) -- Prepend characters of s at front. require argument_not_void: s /= Void compatible_strings: is_string_8 implies s.is_valid_as_string_8 ensure new_count: count = old (count + s.count) inserted: Elks_checking implies same_string (old (s.to_string_32 + Current.as_string_32)) prepend_substring (s: READABLE_STRING_GENERAL; start_index, end_index: INTEGER_32) -- Prepend characters of s.substring (start_index, end_index) at front. require 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 new_count: count = old count + end_index - start_index + 1 inserted: Elks_checking implies same_string (old (s.substring (start_index, end_index).to_string_32 + Current.as_string_32)) prepend_integer (i: INTEGER_32) -- Prepend the string representation of i at front. prepend_double (d: REAL_64) -- Prepend the string representation of d at front. prepend_real (r: REAL_32) -- Prepend the string representation of r at front. prepend_boolean (b: BOOLEAN) -- Prepend the string representation of b at front. keep_head (n: INTEGER_32) -- Remove all characters except for the first n; -- do nothing if n >= count. require non_negative_argument: n >= 0 ensure 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 characters except for the last n; -- do nothing if n >= count. require non_negative_argument: n >= 0 ensure new_count: count = n.min (old count) kept: Elks_checking implies Current ~ (old substring (count - n.min (count) + 1, count)) left_adjust -- Remove leading whitespace. ensure valid_count: count <= old count new_count: not is_empty implies not item (1).is_space kept: Elks_checking implies Current ~ (old twin).substring (old count - count + 1, old count) only_spaces_removed_before: Elks_checking implies (old twin).is_substring_whitespace (1, (old twin).substring_index (Current, 1) - 1) right_adjust -- Remove trailing whitespace. ensure valid_count: count <= old count new_count: not is_empty implies not item (count).is_space kept: Elks_checking implies Current ~ (old twin).substring (1, count) only_spaces_removed_after: Elks_checking implies (old twin).is_substring_whitespace ((old twin).substring_index (Current, 1) + count, old count) adjust -- Remove leading and/or trailing whitespace. ensure valid_count: count <= old count new_count_left: not is_empty implies not item (1).is_space new_count_right: not is_empty implies not 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) feature -- Removal remove (i: INTEGER_32) -- Remove i-th character. require valid_index: valid_index (i) ensure 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 first n characters; -- if n > count, remove all. require n_non_negative: n >= 0 ensure 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. require valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningful_interval: start_index <= end_index + 1 ensure removed: Elks_checking implies Current.as_string_32 ~ (old substring (1, start_index - 1).as_string_32 + old substring (end_index + 1, count).as_string_32) remove_tail (n: INTEGER_32) -- Remove last n characters; -- if n > count, remove all. require n_non_negative: n >= 0 ensure removed: Elks_checking implies Current ~ (old substring (1, count - n.min (count))) wipe_out -- Remove all characters. ensure is_empty: count = 0 same_capacity: capacity = old capacity feature -- Resizing resize (newsize: INTEGER_32) -- Rearrange string so that it can accommodate -- at least newsize characters. -- Do not lose any previously entered character. require new_size_large_enough: newsize >= count ensure same_count: count = old count capacity_large_enough: capacity >= newsize same_content: Elks_checking implies same_string (old twin) invariant mutable: not is_immutable note copyright: "Copyright (c) 1984-2020, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class STRING_GENERAL
Generated by ISE EiffelStudio