Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

kernel.spec.ise

Class KL_STRING_ROUTINES


Direct ancestors

KL_SHARED_PLATFORM, KL_IMPORTED_CHARACTER_ROUTINES, KL_IMPORTED_ANY_ROUTINES, UC_IMPORTED_UNICODE_ROUTINES

Features

Invariants

indexing

description

Routines that ought to be in class STRING

remark

Unless otherwise specified in their preconditions, %
%the features of this class can deal with UC_STRING %
%whenever a STRING is expected.

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 1999-2005, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/06/04 19:43:26 $

revision

$Revision: 1.29 $

class

KL_STRING_ROUTINES

inherit

KL_SHARED_PLATFORM
KL_IMPORTED_CHARACTER_ROUTINES
KL_IMPORTED_ANY_ROUTINES
UC_IMPORTED_UNICODE_ROUTINES

feature -- Initialization

make (n: INTEGER): STRING

-- Create an empty string. Try to allocate space
-- for at least n characters.
-- (ELKS 2001 STRING)

obsolete

[040930] Use 'create Result.make (n)' instead.

require
non_negative_n: n >= 0
ensure
string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
empty_string: Result.count = 0
make_buffer (n: INTEGER): STRING

-- Create a new string containing n characters.
-- (Not in ELKS 2001 STRING)

require
non_negative_n: n >= 0
ensure
string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
count_set: Result.count = n
make_empty: STRING

-- Create empty string.
-- (ELKS 2001 STRING)

obsolete

[041001] Use 'create Result.make_empty' instead.

ensure
string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
empty: Result.count = 0
make_filled (c: CHARACTER; n: INTEGER): STRING

-- Create string of length n filled with c.
-- (ELKS 2001 STRING)

obsolete

[041001] Use 'create Result.make_filled (c, n)' instead.

require
valid_count: n >= 0
ensure
string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
count_set: Result.count = n
filled: Result.occurrences (c) = Result.count
make_from_string (s: STRING): STRING

-- Initialize from the character sequence of s.
-- s is considered with its characters which do not fit
-- in a CHARACTER replaced by a '%U'.
-- (ELKS 2001 STRING)
-- Note: Use this routine instead of 'STRING.make_from_string (s)'
-- when s is of dynamic type other than STRING (e.g. UC_STRING)
-- because the class STRING provided with the Eiffel compilers
-- is not necessarily aware of the implementation of UC_STRING
-- and this may lead to run-time errors or crashes.

require
s_not_void: s /= Void
ensure
string_not_void: Result /= Void
new_string: Result /= s
string_type: ANY_.same_types (Result,
)
initialized: elks_same_string (Result, s)

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
character_: KL_CHARACTER_ROUTINES

-- Routines that ought to be in class CHARACTER

-- (From KL_IMPORTED_CHARACTER_ROUTINES)

ensure
character_routines_not_void: Result /= Void
platform: KL_PLATFORM

-- Platform-dependent properties

-- (From KL_SHARED_PLATFORM)

ensure
platform_not_void: Result /= Void
case_insensitive_hash_code (a_string: STRING): INTEGER

-- Hash code value of a_string which doesn't
-- take case sensitivity into account
-- (Not in ELKS 2001 STRING)

require
a_string_not_void: a_string /= Void
ensure
hash_code_positive: Result >= 0
concat (a_string, other: STRING): STRING

-- New object which contains the characters of a_string
-- followed by the characters of other; If other is
-- of dynamic type UC_STRING or one of its descendants and
-- a_string is not, then the dynamic type of the result
-- is the same as the dynamic type of other. Otherwise
-- the result is similar to 'a_string + other';
-- Note: Use this routine instead of 'a_string + other' or
-- 'a_string.append_string (other)' when a_string
-- can be of dynamic type STRING and other of dynamic
-- type other than STRING such as UC_STRING, because class
-- STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may
-- lead to run-time errors or crashes.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
ensure
concat_not_void: Result /= Void
concat_count: Result.count = a_string.count + other.count
initial: same_string (Result.substring (1, a_string.count), a_string)
final: same_string (Result.substring (a_string.count + 1, Result.count), other)
new_empty_string (a_string: STRING; n: INTEGER): STRING

-- New empty string with same dynamic type as a_string;
-- Try to allocate space for at least n characters.
-- (Not in ELKS 2001 STRING)

require
a_string_not_void: a_string /= Void
non_negative_n: n >= 0
ensure
new_string_not_void: Result /= Void
same_type: ANY_.same_types (Result, a_string)
new_string_empty: Result.count = 0
string (a_string: STRING): STRING

-- New STRING having the same character sequence as a_string
-- where characters which do not fit in a CHARACTER are
-- replaced by a '%U'
-- (Extended from ELKS 2001 STRING)

obsolete

[041001] Use 'a_string.string' instead.

require
a_string_not_void: a_string /= Void
ensure
string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
first_item: a_string.count > 0 implies Result.item (1) = a_string.item (1)
recurse: a_string.count > 1 implies Result.substring (2, a_string.count).is_equal (a_string.substring (2, a_string.count).string)
substring (a_string: STRING; start_index, end_index: INTEGER): STRING

-- New object containing all characters of a_string
-- from start_index to end_index inclusive
-- (ELKS 2001 STRING)

obsolete

[040922] Use a_string.substring (start_index, end_index) instead.

require
a_string_not_void: a_string /= Void
valid_start_index: 1 <= start_index
valid_end_index: end_index <= a_string.count
meaningful_interval: start_index <= end_index + 1
ensure
substring_not_void: Result /= Void
substring_same_type: ANY_.same_types (Result, a_string)
substring_count: Result.count = end_index - start_index + 1
first_item: Result.count > 0 implies Result.item (1) = a_string.item (start_index)
substring_index (a_string, other: STRING; start_index: INTEGER): INTEGER

-- Index of first occurrence of other at or after start_index in
-- a_string; 0 if none. a_string and other are considered with
-- their characters which do not fit in a CHARACTER replaced by a '%U'.
-- (ELKS 2001 STRING)
-- Note: Use this feature instead of 'a_string.substring_index (other,
-- start_index)' when a_string can be of dynamic type STRING and
-- other of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may lead to
-- run-time errors or crashes.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
valid_start_index: start_index >= 1 and start_index <= a_string.count + 1
ensure
valid_result: Result = 0 or else (start_index <= Result and Result <= a_string.count - other.count + 1)
zero_if_absent: (Result = 0) = not has_substring (a_string.substring (start_index, a_string.count), other)
at_this_index: Result >= start_index implies elks_same_string (other, a_string.substring (Result, Result + other.count - 1))
none_before: Result > start_index implies nothas_substring (a_string.substring (start_index, Result + other.count - 2), other)
unicode: UC_UNICODE_ROUTINES

-- Unicode routines

-- (From UC_IMPORTED_UNICODE_ROUTINES)

ensure
unicode_not_void: Result /= Void

feature -- Comparison

elks_same_string (a_string, other: STRING): BOOLEAN

-- Do a_string and other have the same character sequence?
-- a_string and other are considered with their characters
-- which do not fit in a CHARACTER replaced by a '%U'.
-- (Extended from ELKS 2001 STRING)
-- Note: Use this feature instead of 'a_string.same_string
-- (other)' when a_string can be of dynamic type STRING and
-- other of dynamic type other than STRING such as UC_STRING,
-- because class STRING provided by the Eiffel compilers is
-- not necessarily aware of the implementation of UC_STRING
-- and this may lead to run-time errors or crashes.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
ensure
definition: Result = a_string.string.is_equal (other.string)
same_case_insensitive (s1, s2: STRING): BOOLEAN

-- Are s1 and s2 made up of the same
-- characters (case insensitive)?
-- (Not in ELKS 2001 STRING)

require
s1_not_void: s1 /= Void
s2_not_void: s2 /= Void
same_string (a_string, other: STRING): BOOLEAN

-- Do a_string and other have the same unicode character sequence?
-- (Not in ELKS 2001 STRING)
-- Note: the difference with elks_same_string is that here the
-- implementation uses STRING.item_code instead of STRING.item
-- and hence characters which have different codes are not
-- considered equal even if they do not fit into a CHARACTER.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
ensure
definition: Result = (a_string.count = other.count and then(a_string.count > 0 implies (a_string.item_code (1) = other.item_code (1) and(a_string.count >= 2 implies same_string (a_string.substring (2, a_string.count), other.substring (2, a_string.count))))))
elks_same_string: Result implies elks_same_string (a_string, other)
same_unicode_string (a_string, other: STRING): BOOLEAN

-- Do a_string and other have the same unicode character sequence?
-- Note: the difference with elks_same_string is that here the
-- implementation uses STRING.item_code instead of STRING.item
-- and hence characters which have different codes are not
-- considered equal even if they do not fit into a CHARACTER.

obsolete

[020722] Use same_string instead.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
ensure
definition: Result = (a_string.count = other.count and then(a_string.count > 0 implies (a_string.item_code (1) = other.item_code (1) and(a_string.count >= 2 implies same_string (a_string.substring (2, a_string.count), other.substring (2, a_string.count))))))
elks_same_string: Result implies elks_same_string (a_string, other)
three_way_case_insensitive_comparison (a_string, other: STRING): INTEGER

-- If a_string equal to other, 0; if smaller, -1; if greater, 1
-- (case insensitive comparison)
-- (Not in ELKS 2001 STRING)

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
three_way_comparison (a_string, other: STRING): INTEGER

-- If a_string equal to other, 0;
-- if smaller, -1; if greater, 1
-- (ELKS 2001 STRING)
-- Note: there is a bug in the specification of the
-- contracts of three_way_comparison from class
-- COMPARABLE. This routine cannot satisfy its
-- postconditions if other is not of the same type
-- as Current because the postcondition uses is_equal
-- and is_equal has a postcondition inherited from
-- ANY which says if it returns true then other has
-- the same type as Current. The current feature
-- three_way_comparison in class KL_STRING_ROTUINES
-- solves this problem and make the comparison
-- polymorphically safe by changing the signature
-- from 'like Current' to 'STRING' and by using
-- STRING_.same_string instead of is_equal in
-- its postcondition.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
ensure
equal_zero: (Result = 0) = same_string (a_string, other)

feature -- Status report

has_substring (a_string, other: STRING): BOOLEAN

-- Does a_string contain other? a_string and other
-- are considered with their characters which do not fit
-- in a CHARACTER replaced by a '%U'.
-- (Extended from ELKS 2001 STRING)
-- Note: Use this feature instead of 'a_string.has_substring
-- (other)' when a_string can be of dynamic type STRING and
-- other of dynamic type other than STRING such as UC_STRING,
-- because class STRING provided by the Eiffel compilers is
-- not necessarily aware of the implementation of UC_STRING
-- and this may lead to run-time errors or crashes.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
ensure
false_if_too_small: a_string.count < other.count implies not Result
true_if_initial: (a_string.count >= other.count and thenelks_same_string (other, a_string.substring (1, other.count))) implies Result
recurse: (a_string.count >= other.count and thennot elks_same_string (other, a_string.substring (1, other.count))) implies(Result = has_substring (a_string.substring (2, a_string.count), other))
is_hexadecimal (a_string: STRING): BOOLEAN

-- Is a string made up of digits or A-F or a-f?
-- (Not in ELKS 2001 STRING)

require
a_string_not_void: a_string /= Void
is_integer (a_string: STRING): BOOLEAN

-- Is a_string only made up of digits?

require
a_string_not_void: a_string /= Void

feature -- Element change

append_substring_to_string (a_string: STRING; other: STRING; s, e: INTEGER)

-- Append substring of other between indexes
-- s and e at end of a_string.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
same_type: ANY_.same_types (other, a_string)
s_large_enough: s >= 1
e_small_enough: e <= other.count
valid_interval: s <= e + 1
ensure
appended: a_string.is_equal (old cloned_string (a_string) + old other.substring (s, e))
appended_string (a_string, other: STRING): STRING

-- If the dynamic type of other is UC_STRING or one of
-- its descendants and a_string is not, then return a
-- new object with the same dynamic type as other and
-- which contains the characters of a_string followed
-- by the characters of other. Otherwise append the
-- characters of other to a_string and return a_string.
-- Note: Use this routine instead of 'a_string.append_string (other)'
-- when a_string can be of dynamic type STRING and other
-- of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may
-- lead to run-time errors or crashes.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
ensure
append_not_void: Result /= Void
type_if_not_aliased: Result /= a_string implies ANY_.same_types (Result, other)
new_count: Result.count = old a_string.count + old other.count
initial: same_string (Result.substring (1, old a_string.count), old cloned_string (a_string))
final: same_string (Result.substring (old a_string.count + 1, Result.count), old cloned_string (other))
appended_substring (a_string, other: STRING; s, e: INTEGER): STRING

-- If the dynamic type of other is UC_STRING or one of
-- its descendants and a_string is not, then return a
-- new object with the same dynamic type as other and
-- which contains the characters of a_string followed by
-- the characters of other between indexes s and e.
-- Otherwise append the characters of other between s
-- and e to a_string and return a_string.
-- Note: Use this routine instead of 'a_string.append_string
-- (other.substring (s, e)' when a_string can be of dynamic
-- type STRING and other of dynamic type other than STRING
-- such as UC_STRING, because class STRING provided by the
-- Eiffel compilers is not necessarily aware of the
-- implementation of UC_STRING and this may lead to run-time
-- errors or crashes.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
s_large_enough: s >= 1
e_small_enough: e <= other.count
valid_interval: s <= e + 1
ensure
append_not_void: Result /= Void
type_if_not_aliased: Result /= a_string implies ANY_.same_types (Result, other)
new_count: Result.count = old a_string.count + e - s + 1
initial: same_string (Result.substring (1, old a_string.count), old cloned_string (a_string))
final: same_string (Result.substring (old a_string.count + 1, Result.count), old other.substring (s, e))
fill_with (a_string: STRING; c: CHARACTER)

-- Replace every character in a_string with c.
-- (ELKS 2001 STRING)

obsolete

[041002] Use 'a_string.fill_with (c)' instead.

require
a_string_not_void: a_string /= Void
ensure
same_count: old a_string.count = a_string.count
filled: a_string.occurrences (c) = a_string.count
insert_character (a_string: STRING; c: CHARACTER; i: INTEGER)

-- Insert c at index i in a_string, shifting characters
-- between ranks i and count rightwards.
-- (ELKS 2001 STRING)

obsolete

[041002] Use 'a_string.insert_character (c)' instead.

require
a_string_not_void: a_string /= Void
valid_insertion_index: 1 <= i and i <= a_string.count + 1
ensure
one_more_character: a_string.count = old a_string.count + 1
inserted: a_string.item (i) = c
stable_before_i: a_string.substring (1, i - 1).is_equal (old a_string.substring (1, i - 1))
stable_after_i: a_string.substring (i + 1, a_string.count).is_equal (old a_string.substring (i, a_string.count))
replaced_all_substrings (a_text, a_old, a_new: STRING): STRING

-- Copy of a_text for which each occurrence of a_old has been replaced
-- by a_new; a_text if no occurrence could be found

require
a_text_not_void: a_text /= Void
a_old_not_void: a_old /= Void
a_new_not_void: a_new /= Void
ensure
replaced_all_substrings_not_void: Result /= Void
replaced_first_substring (a_text: STRING; a_old, a_new: STRING): STRING

-- Copy of a_text for which first occurrence of a_old has been replaced
-- by a_new; a_text if no occurrence could be found

require
a_text_not_void: a_text /= Void
a_old_not_void: a_old /= Void
a_new_not_void: a_new /= Void
ensure
replaced_first_substring_not_void: Result /= Void
replaced_substring (a_string, other: STRING; start_index, end_index: INTEGER): STRING

-- If the dynamic type of other is UC_STRING or one of
-- its descendants and a_string is not, then return a
-- new object with the same dynamic type as other and
-- which contains the characters of a_string from which
-- the substring from start_index to end_index, inclusive,
-- has been replaced with other. Otherwise replace the
-- substring from start_index to end_index, inclusive,
-- in a_string with other and return a_string.
-- Note: Use this routine instead of 'a_string.replace_substring (other)'
-- when a_string can be of dynamic type STRING and other
-- of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may
-- lead to run-time errors or crashes.

require
a_string_not_void: a_string /= Void
other_not_void: other /= Void
valid_start_index: 1 <= start_index
valid_end_index: end_index <= a_string.count
meaningful_interval: start_index <= end_index + 1
ensure
replaced_substring_not_void: Result /= Void
replaced: same_string (Result, old (appended_string (appended_string (a_string.substring (1, start_index - 1), other), a_string.substring (end_index + 1, a_string.count))))

feature -- Removal

keep_head (a_string: STRING; n: INTEGER)

-- Remove all the characters of a_string except for the first n;
-- if n > a_string.count, do nothing.
-- (ELKS 2001 STRING)

obsolete

[041002] Use a_string.keep_head (n) instead.

require
a_string_not_void: a_string /= Void
n_non_negative: n >= 0
ensure
kept: a_string.is_equal (old a_string.substring (1, n.min (a_string.count)))
keep_tail (a_string: STRING; n: INTEGER)

-- Remove all the characters of a_string except for the last n;
-- if n > a_string.count, do nothing.
-- (ELKS 2001 STRING)

obsolete

[041002] Use a_string.keep_tail (n) instead.

require
a_string_not_void: a_string /= Void
n_non_negative: n >= 0
ensure
kept: a_string.is_equal (old a_string.substring (a_string.count - n.min (a_string.count) + 1, a_string.count))
left_adjust (a_string: STRING)

-- Remove leading whitespace from a_string.
-- (Not in ELKS 2001 STRING)
-- Note: SE 1.1 removes the following characters: ' ';
-- ISE 5.4 removes the following characters: ' ', '%T', '%R', '%N';
-- VE 4.1 removes the characters <= ' '.

require
a_string_not_void: a_string /= Void
ensure
left_adjusted: (a_string.count /= 0) implies((a_string.item_code (1) /= (' ').code) and(a_string.item_code (1) /= ('%T').code) and(a_string.item_code (1) /= ('%R').code) and(a_string.item_code (1) /= ('%N').code))
remove_head (a_string: STRING; n: INTEGER)

-- Remove the first n characters of a_string;
-- if n > a_string.count, remove all.
-- (ELKS 2001 STRING)

obsolete

[041002] Use a_string.remove_head (n) instead.

require
a_string_not_void: a_string /= Void
n_non_negative: n >= 0
ensure
removed: a_string.is_equal (old a_string.substring (n.min (a_string.count) + 1, a_string.count))
remove_substring (a_string: STRING; start_index, end_index: INTEGER)

-- Remove all characters of a_string from start_index
-- to end_index inclusive.
-- (ELKS 2001 STRING)

obsolete

[041002] Use a_string.remove_substring (start_index, end_index) instead.

require
a_string_not_void: a_string /= Void
valid_start_index: 1 <= start_index
valid_end_index: end_index <= a_string.count
meaningful_interval: start_index <= end_index + 1
ensure
removed: a_string.is_equal (old a_string.substring (1, start_index - 1) + old a_string.substring (end_index + 1, a_string.count))
remove_tail (a_string: STRING; n: INTEGER)

-- Remove the last n characters of a_string;
-- if n > a_string.count, remove all.
-- (ELKS 2001 STRING)

obsolete

[041002] Use a_string.remove_tail (n) instead.

require
a_string_not_void: a_string /= Void
n_non_negative: n >= 0
ensure
removed: a_string.is_equal (old a_string.substring (1, a_string.count - n.min (a_string.count)))
right_adjust (a_string: STRING)

-- Remove trailing whitespace from a_string.
-- (Not in ELKS 2001 STRING)
-- Note: SE 1.1 removes the following characters: ' ';
-- ISE 5.4 removes the following characters: ' ', '%T', '%R', '%N';
-- VE 4.1 removes the characters <= ' '.

require
a_string_not_void: a_string /= Void
ensure
right_adjusted: (a_string.count /= 0) implies((a_string.item_code (a_string.count) /= (' ').code) and(a_string.item_code (a_string.count) /= ('%T').code) and(a_string.item_code (a_string.count) /= ('%R').code) and(a_string.item_code (a_string.count) /= ('%N').code))
wipe_out (a_string: STRING)

-- Remove all characters in a_string.
-- Do not discard allocated memory (i.e. do not
-- change capacity) when allowed by the underlying
-- Eiffel compiler.
-- Note: currently only ISE and SE will not change
-- capacity, whereas VE will reset capacity to zero.

require
a_string_not_void: a_string /= Void
ensure
wiped_out: a_string.count = 0

feature -- Resizing

resize_buffer (a_string: STRING; n: INTEGER)

-- Resize a_string so that it contains n characters.
-- Do not lose any previously entered characters.

require
a_string_not_void: a_string /= Void
a_string_is_string: ANY_.same_types (a_string,
)
n_large_enough: n >= a_string.count
ensure
count_set: a_string.count = n

feature -- Conversion

as_lower (a_string: STRING): STRING

-- New object with all letters in lower case
-- (Extended from ELKS 2001 STRING)

obsolete

[041004] Use 'a_string.as_lower' instead.

require
a_string_not_void: a_string /= Void
ensure
as_lower_not_void: Result /= Void
as_lower_same_type: ANY_.same_types (Result, a_string)
length: Result.count = a_string.count
anchor: a_string.count > 0 implies Result.item (1) = CHARACTER_.as_lower (a_string.item (1))
recurse: a_string.count > 1 implies Result.substring (2, a_string.count).is_equal (a_string.substring (2, a_string.count).as_lower)
as_string (a_string: STRING): STRING

-- String version of a_string;
-- Return a_string if it is of dynamic type STRING,
-- return the UTF encoding version if it is a descendant
-- of UC_STRING, return 'string (a_string)' otherwise.

require
a_string_not_void: a_string /= Void
ensure
as_string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
aliasing: ANY_.same_types (a_string,
) implies Result = a_string
as_upper (a_string: STRING): STRING

-- New object with all letters in upper case
-- (Extended from ELKS 2001 STRING)

obsolete

[041004] Use 'a_string.as_upper' instead.

require
a_string_not_void: a_string /= Void
ensure
as_upper_not_void: Result /= Void
as_upper_same_type: ANY_.same_types (Result, a_string)
length: Result.count = a_string.count
anchor: a_string.count > 0 implies Result.item (1) = CHARACTER_.as_upper (a_string.item (1))
recurse: a_string.count > 1 implies Result.substring (2, a_string.count).is_equal (a_string.substring (2, a_string.count).as_upper)
hexadecimal_to_integer (a_string: STRING): INTEGER

-- Convert hexadecimal number string to integer;
-- (Not in ELKS 2001 STRING)
-- Note: Do not take overflow into account.

require
not_void: a_string /= Void
hexadecimal: is_hexadecimal (a_string)
to_lower (a_string: STRING): STRING

-- Lower case version of a_string
-- (Do not alter a_string.)

obsolete

[041004] Use 'a_string.as_lower' instead.

require
a_string_not_void: a_string /= Void
ensure
lower_string_not_void: Result /= Void
lower_string_same_type: ANY_.same_types (Result, a_string)
same_count: Result.count = a_string.count
anchor: a_string.count > 0 implies Result.item (1) = CHARACTER_.as_lower (a_string.item (1))
recurse: a_string.count > 1 implies Result.substring (2, a_string.count).is_equal (a_string.substring (2, a_string.count).as_lower)
to_upper (a_string: STRING): STRING

-- Upper case version of a_string
-- (Do not alter a_string.)

obsolete

[041004] Use 'a_string.as_upper' instead.

require
a_string_not_void: a_string /= Void
ensure
upper_string_not_void: Result /= Void
upper_string_same_type: ANY_.same_types (Result, a_string)
same_count: Result.count = a_string.count
anchor: a_string.count > 0 implies Result.item (1) = CHARACTER_.as_upper (a_string.item (1))
recurse: a_string.count > 1 implies Result.substring (2, a_string.count).is_equal (a_string.substring (2, a_string.count).as_upper)

feature -- Duplication

cloned_string (a_string: STRING): STRING

-- Clone of a_string

require
a_string_not_void: a_string /= Void
ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, a_string)
is_equal: Result.is_equal (a_string)

feature -- Obsolete

platform_: KL_PLATFORM

-- Platform-dependent properties

-- (From KL_SHARED_PLATFORM)

obsolete

[040101] Use Platform instead.

ensure
platform_not_void: Result /= Void

invariant


-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end