Automatic generation produced by ISE Eiffel
indexing description: "[ Sequences of characters, accessible through integer indices in a contiguous range. ]" status: "See notice at end of class" date: "$Date: 2001-11-16 20:32:23 +0000 (Fri, 16 Nov 2001) $" revision: "$Revision: 51435 $" class interface STRING create make (n: INTEGER) -- Allocate space for at least n characters. require non_negative_size: n >= 0 ensure empty_string: count = 0 area_allocated: capacity >= n make_from_string (s: STRING) -- Initialize from the characters of s. -- (Useful in proper descendants of class STRING, -- to initialize a string-like object from a manifest string.) require string_exists: s /= void ensure shared_implementation: shared_with (s) make_from_c (c_string: POINTER) -- Initialize from contents of c_string, -- a string created by some external C function require c_string_exists: c_string /= default_pointer feature -- Initialization adapt (s: STRING): like Current -- Object of a type conforming to the type of s, -- initialized with attributes from s from_c (c_string: POINTER) -- Reset contents of string from contents of c_string, -- a string created by some external C function. require c_string_exists: c_string /= default_pointer ensure no_zero_byte: not has ('%U') from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER) -- Reset contents of string from substring of c_string, -- a string created by some external 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 make_from_c (c_string: POINTER) -- Initialize from contents of c_string, -- a string created by some external C function require c_string_exists: c_string /= default_pointer make_from_string (s: STRING) -- Initialize from the characters of s. -- (Useful in proper descendants of class STRING, -- to initialize a string-like object from a manifest string.) require string_exists: s /= void ensure shared_implementation: shared_with (s) feature -- Access area: SPECIAL [CHARACTER] -- Special data zone -- (from TO_SPECIAL) False_constant: STRING is "false" -- Constant string "false" fuzzy_index (other: STRING; start: INTEGER; fuzz: INTEGER): INTEGER -- 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 require 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 has (c: CHARACTER): BOOLEAN -- Does string include c? ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty hash_code: INTEGER -- Hash code value ensure -- from HASHABLE good_hash_value: Result >= 0 index_of (c: CHARACTER; start: INTEGER): INTEGER -- Position of first occurrence of c at or after start; -- 0 if none. require start_large_enough: start >= 1 start_small_enough: start <= count + 1 ensure correct_place: Result > 0 implies item (Result) = c item (i: INTEGER): CHARACTER -- Character at position i -- Was declared in STRING as synonym of @. require -- from TABLE valid_key: valid_index (k) item_code (i: INTEGER): INTEGER -- Numeric code of character at position i require index_small_enough: i <= count index_large_enough: i > 0 last_index_of (c: CHARACTER; start_index_from_end: INTEGER): INTEGER -- Position of last occurence 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 correct_place: Result > 0 implies item (Result) = c shared_with (other: like Current): BOOLEAN -- Does string share the text of other? substring_index (other: STRING; start: INTEGER): INTEGER -- Position of first occurrence of other at or after start; -- 0 if none. require other_nonvoid: other /= void other_notempty: not other.is_empty start_large_enough: start >= 1 start_small_enough: start <= count ensure correct_place: Result > 0 implies substring (Result, Result + other.count - 1).is_equal (other) True_constant: STRING is "true" -- Constant string "true" infix "@" (i: INTEGER): CHARACTER -- Character at position i -- Was declared in STRING as synonym of item. require -- from TABLE valid_key: valid_index (k) feature -- Measurement additional_space: INTEGER -- Proposed number of additional items -- (from RESIZABLE) ensure -- from RESIZABLE at_least_one: Result >= 1 capacity: INTEGER -- Allocated space count: INTEGER -- Actual number of characters making up the string Growth_percentage: INTEGER is 50 -- Percentage by which structure will grow automatically -- (from RESIZABLE) index_set: INTEGER_INTERVAL -- Range of acceptable indexes ensure -- from INDEXABLE not_void: Result /= void ensure then Result.count = count Minimal_increase: INTEGER is 5 -- Minimal number of additional items -- (from RESIZABLE) occurrences (c: CHARACTER): INTEGER -- Number of times c appears in the string ensure -- from BAG non_negative_occurrences: Result >= 0 feature -- Comparison is_equal (other: like Current): BOOLEAN -- Is string made of same character sequence as other -- (possibly with a different capacity)? require -- from ANY other_not_void: other /= void ensure -- from ANY symmetric: Result implies other.is_equal (Current) consistent: standard_is_equal (other) implies Result ensure then -- from COMPARABLE trichotomy: Result = (not (Current < other) and not (other < Current)) max (other: like Current): like Current -- 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: like Current): like Current -- 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 three_way_comparison (other: like Current): INTEGER -- If current object equal to other, 0; -- if smaller, -1; if greater, 1 -- (from COMPARABLE) require -- from COMPARABLE other_exists: other /= void ensure -- from COMPARABLE equal_zero: (Result = 0) = is_equal (other) smaller_negative: (Result = - 1) = (Current < other) greater_positive: (Result = 1) = (Current > other) infix "<" (other: like Current): BOOLEAN -- Is string lexicographically lower than other? require -- from PART_COMPARABLE other_exists: other /= void ensure then -- from COMPARABLE asymmetric: Result implies not (other < Current) infix "<=" (other: like Current): 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 is_equal (other)) infix ">" (other: like Current): 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) infix ">=" (other: like Current): 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) feature -- Status report Changeable_comparison_criterion: BOOLEAN is False Extendible: BOOLEAN is True -- May new items be added? (Answer: yes.) full: BOOLEAN -- Is structure full? -- (from BOUNDED) is_boolean: BOOLEAN -- Does Current represent a BOOLEAN? is_double: BOOLEAN -- Does Current represent a DOUBLE? is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) is_hashable: BOOLEAN -- May current object be hashed? -- (True if it is not its type's default.) -- (from HASHABLE) ensure -- from HASHABLE ok_if_not_default: Result implies (Current /= default) is_inserted (v: CHARACTER): 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? is_real: BOOLEAN -- Does Current represent a REAL? 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.) resizable: BOOLEAN -- May capacity be changed? (Answer: yes.) -- (from RESIZABLE) valid_index (i: INTEGER): BOOLEAN -- Is i within the bounds of the string? ensure then -- from INDEXABLE only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper)) 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 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 ensure -- from CONTAINER reference_comparison: not object_comparison feature -- Element change append (s: STRING) -- Append a copy of s at end. require argument_not_void: s /= void ensure new_count: count = old count + old s.count append_boolean (b: BOOLEAN) -- Append the string representation of b at end. append_character (c: CHARACTER) -- Append c at end. -- Was declared in STRING as synonym of extend. ensure then item_inserted: item (count) = c new_count: count = old count + 1 append_double (d: DOUBLE) -- Append the string representation of d at end. append_integer (i: INTEGER) -- Append the string representation of i at end. append_real (r: REAL) -- Append the string representation of r at end. append_string (s: STRING) -- Append a copy of s, if not void, at end. copy (other: like Current) -- Reinitialize by copying the characters of other. -- (This is also used by clone.) require -- from ANY other_not_void: other /= void type_identity: same_type (other) ensure -- from ANY is_equal: is_equal (other) ensure then new_result_count: count = other.count extend (c: CHARACTER) -- Append c at end. -- Was declared in STRING as synonym of append_character. require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: is_inserted (v) ensure then -- from BAG one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1 ensure then item_inserted: item (count) = c new_count: count = old count + 1 fill (other: CONTAINER [CHARACTER]) -- 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 fill_blank -- Fill with capacity blank characters. ensure filled: full same_size: (count = capacity) and (capacity = old capacity) fill_character (c: CHARACTER) -- Fill with capacity characters all equal to c. ensure filled: full same_size: (count = capacity) and (capacity = old capacity) head (n: INTEGER) -- 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) insert (s: STRING; i: INTEGER) -- Add s to the left of position i in current string. require string_exists: s /= void index_small_enough: i <= count index_large_enough: i > 0 ensure new_count: count = old count + s.count left_adjust -- Remove leading whitespace. ensure new_count: (count /= 0) implies ((item (1) /= ' ') and (item (1) /= '%T') and (item (1) /= '%R') and (item (1) /= '%N')) precede (c: CHARACTER) -- Add c at front. ensure new_count: count = old count + 1 prepend (s: STRING) -- Prepend a copy of s at front. require argument_not_void: s /= void ensure new_count: count = old count + s.count prepend_boolean (b: BOOLEAN) -- Prepend the string representation of b at front. prepend_character (c: CHARACTER) -- Prepend the string representation of c at front. prepend_double (d: DOUBLE) -- Prepend the string representation of d at front. prepend_integer (i: INTEGER) -- Prepend the string representation of i at front. prepend_real (r: REAL) -- Prepend the string representation of r at front. prepend_string (s: STRING) -- Prepend a copy of s, if not void, at front. put (c: CHARACTER; i: INTEGER) -- Replace character at position i by c. require -- from TABLE valid_key: valid_index (k) ensure then -- from INDEXABLE insertion_done: item (k) = v replace_blank -- Replace all current characters with blanks. ensure same_size: (count = old count) and (capacity = old capacity) replace_character (c: CHARACTER) -- Replace all current characters with characters all equal to c. ensure same_size: (count = old count) and (capacity = old capacity) replace_substring (s: like Current; start_pos, end_pos: INTEGER) -- Copy the characters of s to positions -- start_pos .. end_pos. require string_exists: s /= void index_small_enough: end_pos <= count order_respected: start_pos <= end_pos index_large_enough: start_pos > 0 ensure new_count: count = old count + s.count - end_pos + start_pos - 1 replace_substring_all (original, new: like Current) -- Replace every occurence of original with new. require original_exists: original /= void new_exists: new /= void original_not_empty: not original.is_empty right_adjust -- Remove trailing whitespace. ensure new_count: (count /= 0) implies ((item (count) /= ' ') and (item (count) /= '%T') and (item (count) /= '%R') and (item (count) /= '%N')) set (t: like Current; n1, n2: INTEGER) -- 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: is_equal (t.substring (n1, n2)) share (other: like Current) -- 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 subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER) -- 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) tail (n: INTEGER) -- 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) infix "+" (s: STRING): STRING -- Append a copy of 's' at the end of a copy of Current, -- Then return the Result. require argument_not_void: s /= void ensure result_exists: Result /= void new_count: Result.count = count + s.count feature -- Removal clear_all -- Reset all characters. ensure is_empty: count = 0 same_capacity: capacity = old capacity prune (c: CHARACTER) -- Remove first occurrence of c, if any. require -- from COLLECTION prunable: prunable require else True prune_all (c: CHARACTER) -- Remove all occurrences of c. require -- from COLLECTION prunable require else True ensure -- from COLLECTION no_more_occurrences: not has (v) ensure then changed_count: count = (old count) - (old occurrences (c)) prune_all_leading (c: CHARACTER) -- Remove all leading occurrences of c. prune_all_trailing (c: CHARACTER) -- Remove all trailing occurrences of c. remove (i: INTEGER) -- Remove i-th character. require index_small_enough: i <= count index_large_enough: i > 0 ensure new_count: count = old count - 1 wipe_out -- Remove all characters. require -- from COLLECTION prunable ensure -- from COLLECTION wiped_out: is_empty ensure then is_empty: count = 0 empty_capacity: capacity = 0 feature -- Resizing adapt_size -- Adapt the size to accommodate count characters. automatic_grow -- Change the capacity to accommodate at least -- Growth_percentage more items. -- (from RESIZABLE) ensure -- from RESIZABLE increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100 grow (newsize: INTEGER) -- Ensure that the capacity is at least newsize. require -- from RESIZABLE True require else new_size_non_negative: newsize >= 0 ensure -- from RESIZABLE new_capacity: capacity >= i resize (newsize: INTEGER) -- Rearrange string so that it can accommodate -- at least newsize characters. -- Do not lose any previously entered character. require new_size_non_negative: newsize >= 0 feature -- Conversion center_justify -- Center justify the string using -- the capacity as the width character_justify (pivot: CHARACTER; position: INTEGER) -- 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 /= ' ' not_empty: not is_empty left_justify -- Left justify the string using -- the capacity as the width linear_representation: LINEAR [CHARACTER] -- Representation as a linear structure mirror -- Reverse the order of characters. -- "Hello world" -> "dlrow olleH". ensure same_count: count = old count mirrored: like Current -- Mirror image of string; -- result for "Hello world" is "dlrow olleH". ensure same_count: Result.count = count right_justify -- Right justify the string using -- the capacity as the width split (a_separator: CHARACTER): LINEAR [STRING] -- Split on a_separator. -- Ignore separators in quotes. ensure Result /= void to_boolean: BOOLEAN -- Boolean value; -- "True" yields True, "False" yields False -- (case-insensitive) require is_boolean: is_boolean frozen to_c: ANY -- A reference to a C form of current string. -- Useful only for interfacing with C software. to_double: DOUBLE -- "Double" value; -- for example, when applied to "123.0", will yield 123.0 (double) require represents_a_double: is_double to_integer: INTEGER -- Integer value; -- for example, when applied to "123", will yield 123 require is_integer: is_integer to_lower -- Convert to lower case. to_real: REAL -- Real value; -- for example, when applied to "123.0", will yield 123.0 require represents_a_real: is_real to_upper -- Convert to upper case. feature -- Duplication multiply (n: INTEGER) -- Duplicate a string within itself -- ("hello").multiply(3) => "hellohellohello" require meaningful_multiplier: n >= 1 substring (n1, n2: INTEGER): like Current -- Copy of substring containing all characters at indices -- between n1 and n2 ensure new_result_count: Result.count = n2 - n1 + 1 or Result.count = 0 feature -- Output out: like Current -- Printable representation invariant extendible: extendible compare_character: not object_comparison index_set_has_same_count: index_set.count = count -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from INDEXABLE index_set_not_void: index_set /= void -- from RESIZABLE increase_by_at_least_one: minimal_increase >= 1 -- from BOUNDED valid_count: count <= capacity full_definition: full = (count = capacity) -- from FINITE empty_definition: is_empty = (count = 0) non_negative_count: count >= 0 -- from COMPARABLE irreflexive_comparison: not (Current < Current) indexing library: "[ EiffelBase: Library of reusable components for Eiffel. ]" status: "[ Copyright 1986-2001 Interactive Software Engineering (ISE). For ISE customers the original versions are an ISE product covered by the ISE Eiffel license and support agreements. ]" license: "[ EiffelBase may now be used by anyone as FREE SOFTWARE to develop any product, public-domain or commercial, without payment to ISE, under the terms of the ISE Free Eiffel Library License (IFELL) at http://eiffel.com/products/base/license.html. ]" source: "[ Interactive Software Engineering Inc. ISE Building 360 Storke Road, Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Electronic mail <info@eiffel.com> Customer support http://support.eiffel.com ]" info: "[ For latest info see award-winning pages: http://eiffel.com ]" end -- class STRING -- Generated by ISE Eiffel --
For more details: www.eiffel.com