Automatic generation produced by ISE Eiffel
note description: "[ Sequences of 32-bit characters, accessible through integer indices in a contiguous range. ]" library: "Free implementation of ELKS library" status: "See notice at end of class." legal: "See notice at end of class." date: "$Date: 2016-04-13 06:29:38 -0700 (Wed, 13 Apr 2016) $" revision: "$Revision: 98619 $" class interface STRING_32 create make, make_empty, make_filled, make_from_string, make_from_string_general, make_from_c, make_from_c_pointer, make_from_cil, make_from_separate convert to_cil: {SYSTEM_STRING}, make_from_cil ({SYSTEM_STRING}), as_string_8: {READABLE_STRING_8, STRING_8} feature -- Initialization make_from_string_general (s: READABLE_STRING_GENERAL) -- Initialize from the characters of `s'. make_from_cil (a_system_string: detachable SYSTEM_STRING) -- Initialize Current with `a_system_string'. from_c (c_string: POINTER) -- Reset contents of string from contents of `c_string', -- a string created by some C function. require c_string_exists: c_string /= default_pointer ensure no_zero_byte: not has ('%U'.to_character_32) from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32) -- Reset contents of string from substring of `c_string', -- a string created by some C function. require c_string_exists: c_string /= default_pointer start_position_big_enough: start_pos >= 1 end_position_big_enough: start_pos <= end_pos + 1 ensure valid_count: count = end_pos - start_pos + 1 adapt (s: STRING_32): like Current -- Object of a type conforming to the type of `s', -- initialized with attributes from `s' ensure adapt_not_void: Result /= Void shared_implementation: Result.shared_with (s) feature -- Access item alias "[]" (i: INTEGER_32): CHARACTER_32 assign put -- Character at position `i' -- Was declared in STRING_32 as synonym of at. at alias "@" (i: INTEGER_32): CHARACTER_32 assign put -- Character at position `i' -- Was declared in STRING_32 as synonym of item. code (i: INTEGER_32): NATURAL_32 -- Character at position `i' area: SPECIAL [CHARACTER_32] -- Storage for characters feature -- Status report Extendible: BOOLEAN = True -- May new items be added? (Answer: yes.) prunable: BOOLEAN -- May items be removed? (Answer: yes.) Changeable_comparison_criterion: BOOLEAN = False -- May object_comparison be changed? -- (Answer: yes by default.) feature -- Element change set (t: READABLE_STRING_32; n1, n2: INTEGER_32) -- Set current string to substring of `t' from indices `n1' -- to `n2', or to empty string if no such substring. require argument_not_void: t /= Void ensure is_substring: same_string (t.substring (n1, n2)) subcopy (other: READABLE_STRING_32; 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'. require 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 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))) replace_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32) -- Replace characters from `start_index' to `end_index' with `s'. require string_not_void: s /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningfull_interval: start_index <= end_index + 1 ensure new_count: count = old count + old s.count - end_index + start_index - 1 replaced: Elks_checking implies (Current ~ (old (substring (1, start_index - 1) + s + substring (end_index + 1, count)))) replace_substring_all (original, new: READABLE_STRING_32) -- Replace every occurrence of `original' with `new'. require original_exists: original /= Void new_exists: new /= Void original_not_empty: not original.is_empty replace_blank -- Replace all current characters with blanks. ensure same_size: (count = old count) and (capacity = old capacity) all_blank: Elks_checking implies occurrences (' '.to_character_32) = count fill_blank -- Fill with capacity blank characters. ensure filled: full same_size: (count = capacity) and (capacity = old capacity) fill_with (c: CHARACTER_32) -- Replace every character with `c'. ensure same_count: (count = old count) and (capacity = old capacity) filled: Elks_checking implies occurrences (c) = count keep_head (n: INTEGER_32) -- Remove all characters except for the first `n'; -- do nothing if `n' >= count. keep_tail (n: INTEGER_32) -- Remove all characters except for the last `n'; -- do nothing if `n' >= count. left_adjust -- Remove leading whitespace. right_adjust -- Remove trailing whitespace. share (other: STRING_32) -- Make current string share the text of `other'. -- Subsequent changes to the characters of current string -- will also affect `other', and conversely. require argument_not_void: other /= Void ensure shared_count: other.count = count shared_area: other.area = area put (c: CHARACTER_32; i: INTEGER_32) -- Replace character at position `i' by `c'. ensure then 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)) put_code (v: NATURAL_32; i: INTEGER_32) -- Replace character at position `i' by character of code `v'. prepend_string_general (s: READABLE_STRING_GENERAL) -- Prepend characters of `s' at front. precede (c: CHARACTER_32) -- Add `c' at front. -- Was declared in STRING_32 as synonym of prepend_character. ensure new_count: count = old count + 1 prepend_character (c: CHARACTER_32) -- Add `c' at front. -- Was declared in STRING_32 as synonym of precede. ensure new_count: count = old count + 1 prepend (s: READABLE_STRING_32) -- Prepend characters of `s' at front. require argument_not_void: s /= Void ensure new_count: count = old (count + s.count) inserted: Elks_checking implies same_string (old (s + Current)) prepend_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32) -- Prepend characters of `s.substring (start_index, end_index)' at front. require 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 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_boolean (b: BOOLEAN) -- Prepend the string representation of `b' at front. prepend_double (d: REAL_64) -- Prepend the string representation of `d' at front. prepend_integer (i: INTEGER_32) -- Prepend the string representation of `i' at front. prepend_real (r: REAL_32) -- Prepend the string representation of `r' at front. prepend_string (s: detachable READABLE_STRING_32) -- Prepend characters of `s', if not void, at front. append_string_general (s: READABLE_STRING_GENERAL) -- Append characters of `s' at end. append (s: READABLE_STRING_32) -- Append characters of `s' at end. require argument_not_void: s /= Void ensure new_count: count = old count + old s.count appended: Elks_checking implies same_string (old (Current + s)) append_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32) -- Append characters of `s.substring (start_index, end_index)' at end. require 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 new_count: count = old count + (end_index - start_index + 1) appended: Elks_checking implies same_string (old (Current + s.substring (start_index, end_index))) plus alias "+" (s: READABLE_STRING_GENERAL): like Current append_string (s: detachable READABLE_STRING_32) -- Append a copy of `s', if not void, at end. ensure appended: s /= Void implies (Elks_checking implies Current ~ (old twin + old s.twin)) append_integer (i: INTEGER_32) -- Append the string representation of `i' at end. 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_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_natural_64 (i: NATURAL_64) -- 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_character (c: CHARACTER_32) -- Append `c' at end. -- Was declared in STRING_32 as synonym of extend. ensure then item_inserted: item (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) extend (c: CHARACTER_32) -- Append `c' at end. -- Was declared in STRING_32 as synonym of append_character. ensure then item_inserted: item (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) append_boolean (b: BOOLEAN) -- Append the string representation of `b' at end. insert_string (s: READABLE_STRING_32; i: INTEGER_32) -- Insert `s' at index `i', shifting characters between ranks -- `i' and count rightwards. require string_exists: s /= Void valid_insertion_index: 1 <= i and i <= count + 1 ensure inserted: Elks_checking implies (Current ~ (old substring (1, i - 1) + old (s.twin) + old substring (i, count))) insert_character (c: CHARACTER_32; i: INTEGER_32) -- Insert `c' at index `i', shifting characters between ranks -- `i' and count rightwards. require valid_insertion_index: 1 <= i and i <= count + 1 ensure 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)) feature -- Removal remove (i: INTEGER_32) -- Remove `i'-th character. 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 ~ (old substring (1, start_index - 1) + old substring (end_index + 1, count)) 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))) prune (c: CHARACTER_32) -- Remove first occurrence of `c', if any. require else True prune_all (c: CHARACTER_32) -- Remove all occurrences of `c'. require else True ensure then changed_count: count = (old count) - (old occurrences (c)) prune_all_leading (c: CHARACTER_32) -- Remove all leading occurrences of `c'. prune_all_trailing (c: CHARACTER_32) -- Remove all trailing occurrences of `c'. wipe_out -- Remove all characters. ensure then is_empty: count = 0 same_capacity: capacity = old capacity feature -- Resizing adapt_size -- Adapt the size to accommodate count characters. resize (newsize: INTEGER_32) -- Rearrange string so that it can accommodate -- at least `newsize' characters. -- Do not lose any previously entered character. grow (newsize: INTEGER_32) -- Ensure that the capacity is at least `newsize'. trim -- Decrease capacity to the minimum value. -- Apply to reduce allocated storage. ensure then same_string: same_string (old twin) feature -- Conversion as_lower: like Current -- New object with all letters in lower case. as_upper: like Current -- New object with all letters in upper case left_justify -- Left justify Current using count as witdth. center_justify -- Center justify Current using count as width. right_justify -- Right justify Current using count as width. ensure same_count: count = old count character_justify (pivot: CHARACTER_32; 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. require valid_position: position <= capacity positive_position: position >= 1 pivot_not_space: pivot /= ' '.to_character_32 not_empty: not is_empty to_lower -- Convert to lower case. ensure length_and_content: Elks_checking implies Current ~ (old as_lower) to_upper -- Convert to upper case. ensure length_and_content: Elks_checking implies Current ~ (old as_upper) linear_representation: LINEAR [CHARACTER_32] -- Representation as a linear structure frozen to_c: ANY -- A reference to a C form of current string. -- Useful only for interfacing with C software. require not_is_dotnet: not {PLATFORM}.is_dotnet mirrored: like Current -- Mirror image of string; -- Result for "Hello world" is "dlrow olleH". mirror -- Reverse the order of characters. -- "Hello world" -> "dlrow olleH". ensure same_count: count = old count feature -- Duplication substring (start_index, end_index: INTEGER_32): like Current -- Copy of substring containing all characters at indices -- between `start_index' and `end_index' multiply (n: INTEGER_32) -- Duplicate a string within itself -- ("hello").multiply(3) => "hellohellohello" require meaningful_multiplier: n >= 1 feature -- Transformation correct_mismatch -- Attempt to correct object mismatch during retrieve using Mismatch_information. invariant extendible: Extendible compare_character: not object_comparison note copyright: "Copyright (c) 1984-2016, 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_32 -- Generated by ISE Eiffel --
For more details: www.eiffel.com