Automatic generation produced by ISE Eiffel
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: 2014-03-19 07:36:10 -0700 (Wed, 19 Mar 2014) $" revision: "$Revision: 94633 $" deferred class interface STRING_GENERAL convert as_string_32: {READABLE_STRING_32, STRING_32}, to_cil: {SYSTEM_STRING} feature -- Settings 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)) feature -- Element change 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 (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)) 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))) 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)) 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)) 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) 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-2014, 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 Eiffel --
For more details: www.eiffel.com