Automatic generation produced by ISE Eiffel
note description: "[ Sequences of 8-bit characters, accessible through integer indices in a contiguous range. Read-only interface. ]" 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 $" deferred class interface READABLE_STRING_8 convert to_cil: {SYSTEM_STRING}, as_string_8: {STRING_8}, as_readable_string_32: {READABLE_STRING_32}, as_string_32: {STRING_32} feature -- Access item alias "[]" (i: INTEGER_32): CHARACTER_8 -- Character at position `i'. -- Was declared in READABLE_STRING_8 as synonym of at. at alias "@" (i: INTEGER_32): CHARACTER_8 -- Character at position `i'. -- Was declared in READABLE_STRING_8 as synonym of item. shared_with (other: READABLE_STRING_8): BOOLEAN -- Does string share the text of `other'? index_of (c: CHARACTER_8; start_index: INTEGER_32): INTEGER_32 -- Position of first occurrence of `c' at or after `start_index'; -- 0 if none. require start_large_enough: start_index >= 1 start_small_enough: 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 (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) last_index_of (c: CHARACTER_8; start_index_from_end: INTEGER_32): INTEGER_32 -- Position of last occurrence of `c', -- 0 if none. require start_index_small_enough: start_index_from_end <= count start_index_large_enough: start_index_from_end >= 1 ensure 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) 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. string: STRING_8 -- New STRING_8 having same character sequence as `Current'. ensure 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 ensure 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_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 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 new_cursor: STRING_8_ITERATION_CURSOR -- Fresh cursor associated with current structure feature -- Measurement capacity: INTEGER_32 -- Allocated space count: INTEGER_32 -- Actual number of characters making up the string occurrences (c: CHARACTER_8): INTEGER_32 -- Number of times `c' appears in the string ensure then 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) Lower: INTEGER_32 = 1 -- Minimum index. feature -- Comparison is_equal (other: like Current): BOOLEAN -- Is string made of same character sequence as `other' -- (possibly with a different capacity)? is_case_insensitive_equal (other: READABLE_STRING_8): BOOLEAN -- Is string made of same character sequence as `other' regardless of casing -- (possibly with a different capacity)? require other_not_void: other /= Void ensure symmetric: Result implies other.is_case_insensitive_equal (Current) consistent: attached {like Current} other as l_other implies (standard_is_equal (l_other) implies Result) valid_result: as_lower ~ other.as_lower implies Result 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'. 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) ensure same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).is_case_insensitive_equal (other.substring (start_pos, end_pos)) same_string (other: READABLE_STRING_8): BOOLEAN -- Do `Current' and `other' have same character sequence? require other_not_void: other /= Void ensure definition: Result = (string ~ other.string) 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'. 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) ensure same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).same_string (other.substring (start_pos, end_pos)) is_less alias "<" (other: like Current): BOOLEAN -- Is string lexicographically lower than `other'? feature -- Status report Is_string_8: BOOLEAN = True -- Is `Current' a sequence of CHARACTER_8? Is_string_32: BOOLEAN = False -- Is `Current' a sequence of CHARACTER_32? Is_valid_as_string_8: BOOLEAN = True -- Is `Current' convertible to a sequence of CHARACTER_8 without information loss? is_substring_whitespace (start_index, end_index: INTEGER_32): BOOLEAN -- Is substring between `start_index' and `end_index' containing only whitespace characters? has (c: CHARACTER_8): BOOLEAN -- Does string include `c'? ensure 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)) starts_with (s: READABLE_STRING_8): BOOLEAN -- Does string begin with `s'? require argument_not_void: s /= Void ensure definition: Result = s.same_string (substring (1, s.count)) ends_with (s: READABLE_STRING_8): BOOLEAN -- Does string finish with `s'? require argument_not_void: s /= Void ensure definition: Result = s.same_string (substring (count - s.count + 1, count)) valid_code (v: NATURAL_32): BOOLEAN -- Is `v' a valid code for a CHARACTER_32? is_boolean: BOOLEAN -- Does `Current' represent a BOOLEAN? feature -- Conversion mirrored: like Current -- Mirror image of string; -- Result for "Hello world" is "dlrow olleH". ensure same_count: Result.count = 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' feature -- Output out: STRING_8 -- Printable representation ensure then out_not_void: Result /= Void same_items: same_type ("") implies Result.same_string (Current) invariant area_not_void: area /= Void 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 READABLE_STRING_8 -- Generated by ISE Eiffel --
For more details: www.eiffel.com