Class STRING
Visual Eiffel 3.2 beta
indexing
title : "Sequences of characters, accessible through integer",
"indices in a contiguous range.";
cluster : "%VE_Lib%\Kernel";
project : "Eiffel Kernel Library";
copyright : "Object Tools, 1996-1997";
original : 26,Apr,96;
version : 1.0;
last_change :
25,Jul,96, Alexis, "invariant clause was updated - assertions the ",
"same to one from GENERAL was removed ";
key : ELKS;
done_at : "Object Tools (info@object-tools.com)";
extrnl_name : "string.e"
-----------------------------------------------------------------------------
class STRING
-----------------------------------------------------------------------------
inherit
------------------------------------------------------------------ COMPARABLE
COMPARABLE
redefine
is_equal, copy, out, compare
end
-------------------------------------------------------------------- HASHABLE
HASHABLE
redefine
is_equal, copy, out
end
-----------------------------------------------------------------------------
creation {ANY}
make, make_from_string, adapt
-----------------------------------------------------------------------------
feature -- Creation
------------------------------------------------------------------------ make
frozen make (n : INTEGER) is
-- Allocate space for at least 'n' characters
require
non_negative_size : n >= 0
external "CWC"
alias "_STR_make"
ensure
empty_string : count = n
end; -- make
------------------------------------------------------------ make_from_string
make_from_string (s : STRING) is
-- 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
do
if Current /= s then
make (s.count);
c_string_copy (s);
end; -- if
end; -- make_from_string
-----------------------------------------------------------------------------
feature -- Initialization
---------------------------------------------------------------------- from_c
from_c (c_string : POINTER) is
-- 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
external "CWC"
alias "_STR_from_c"
end; -- from_c
---------------------------------------------------------------------- remake
frozen remake (n : INTEGER) is
-- Allocate space for at least 'n' characters
require
non_negative_size : n >= 0
external "CWC"
alias "_STR_make"
ensure
empty_string : count = n
end; -- remake
-----------------------------------------------------------------------------
feature -- Access
------------------------------------------------------------------------- has
has (c : CHARACTER) : BOOLEAN is
-- Does string include 'c' ?
do
Result := occurrences (c) > 0;
ensure
not_found_in_empty : Result implies not empty
end; -- has
------------------------------------------------------------------- hash_code
hash_code : INTEGER is
-- Hash code value
-- (From HASHABLE)
local
i : INTEGER;
n : INTEGER;
h : BIT 32;
g : BIT 32;
do
from
n := count;
until
i = n
loop
i := i + 1;
h.from_integer ((h ^ -4).to_integer + item (i).code);
g := h and 11110000000000000000000000000000B;
if g /= 00000000000000000000000000000000B then
h := h xor (g ^ 24);
end; -- if
h := h and not g;
end; -- loop
Result := h.to_integer.abs;
end; -- hash_code
-------------------------------------------------------------------- index_of
index_of (c : CHARACTER; start : INTEGER) : INTEGER is
-- Position of first occurrence of 'c' at or after 'start'; 0 if none
require
good_key : valid_index (start)
local
i : INTEGER;
do
from
i := start;
until
i > count
loop
if c = item (i) then
Result := i;
i := count;
end; -- if
i := i + 1;
end; -- loop
ensure
non_negative_result : Result >= 0;
at_this_position : Result > 0 implies item (Result) = c;
--none_before : For every i in start..Result, item (i) /= c;
--zero_iff_absent :
-- (Result = 0) = For every i in 1..count, item (i) /= c
end; -- index_of
------------------------------------------------------------- infix "@", item
infix "@", item (i : INTEGER) : CHARACTER is
-- Character at position 'i'
require
good_key : valid_index (i)
external "CWC"
alias "_STR_item"
end; -- infix "@", item
------------------------------------------------------------------- item_code
item_code (i : INTEGER) : INTEGER is
-- Numeric code of character at position 'i'
require
good_key : valid_index (i)
do
Result := item (i).code;
end; -- item_code
------------------------------------------------------------- substring_index
substring_index (other : STRING; start : INTEGER) : INTEGER is
-- Position of first occurrence of 'other' at or after 'start';
-- 0 if none
require
other_non_void : other /= Void;
other_not_empty : not other.empty;
good_key : valid_index (start)
external "CWC"
alias "_STR_substring_index"
end; -- substring_index
-----------------------------------------------------------------------------
feature {NONE} -- Implementation
------------------------------------------------------------------------ area
frozen area : POINTER;
-- in fact it's pointer to string's data
-- (for internal use only)
-----------------------------------------------------------------------------
feature -- Measurement
----------------------------------------------------------------------- count
count : INTEGER;
-- Actual number of characters making up to string
----------------------------------------------------------------- occurrences
occurrences (c : CHARACTER) : INTEGER is
-- Number of times 'c' appears in the string
local
i : INTEGER;
do
from
until
i = count
loop
i := i + 1;
if c = item (i) then
Result := Result + 1;
end; -- if
end; -- loop
ensure
non_negative_occurrences : Result >= 0
end; -- occurrences
-----------------------------------------------------------------------------
feature -- Comparison
-------------------------------------------------------------------- is_equal
is_equal (other : like Current) : BOOLEAN is
-- Is string made of same character sequence as 'other' ?
-- (Redefined from GENERAL)
do
if count = other.count then
Result := compare (other) = 0;
end; -- if
end; -- is_equal
------------------------------------------------------------------- infix "<"
infix "<" (other : like Current) : BOOLEAN is
-- Is string lexicographically lower than 'other' ?
-- (False if 'other' is void)
-- (From COMPARABLE)
do
Result := compare (other) < 0;
end; -- infix "<"
--------------------------------------------------------------------- same_as
same_as (other: STRING): BOOLEAN is
-- Is string made of same character sequence as other?
-- Case insensitive comparison.
require
other_exists: other /= Void
local
current_str: STRING
other_str: STRING
do
current_str := clone (Current)
current_str.to_lower
other_str := clone (other)
other_str.to_lower
Result := current_str.is_equal (other_str)
end; -- same_as
-----------------------------------------------------------------------------
feature -- Status report
----------------------------------------------------------------------- empty
empty : BOOLEAN is
-- Is string empty ?
do
Result := count = 0;
end; -- empty
----------------------------------------------------------------- valid_index
valid_index (i : INTEGER) : BOOLEAN is
-- Is 'i' within the bounds of the string ?
do
Result := i > 0 and i <= count;
end; -- valid_index
-----------------------------------------------------------------------------
feature -- Element change
-------------------------------------------------------------- append_boolean
append_boolean (b : BOOLEAN) is
-- Append the string representation of 'b' at end
external "CWC"
alias "_STR_append_boolean"
end; -- append_boolean
------------------------------------------------------------ append_character
append_character (c : CHARACTER) is
-- Append 'c' at end
external "CWC"
alias "_STR_append_character"
ensure
item_inserted : item (count) = c;
one_more_occurence : occurrences (c) = old (occurrences (c)) + 1
end; -- append_character
--------------------------------------------------------------- append_double
append_double (d : DOUBLE) is
-- Append the string representation of 'd' at end
external "CWC"
alias "_STR_append_double"
end; -- append_double
-------------------------------------------------------------- append_integer
append_integer (i : INTEGER) is
-- Append the string representation of 'i' at end
external "CWC"
alias "_STR_append_integer"
end; -- append_integer
----------------------------------------------------------------- append_real
append_real (r : REAL) is
-- Append the string representation of 'r' at end
external "CWC"
alias "_STR_append_real"
end; -- append_real
--------------------------------------------------------------- append_string
append_string (s : STRING) is
-- Append a copy of 's', if not void, at end
external "CWC"
alias "_STR_append_string"
ensure
new_count : (s = Void implies count = old count) and
(s /= Void implies
( ( count = s.count + old count ) or else
( s = Current and then count = 2 * old count ) )
)
--appended : For every i in 1..s.count,
-- item (old count + i) = s.item (i)
end; -- append_string
------------------------------------------------------------------------ fill
fill (c : CHARACTER) is
-- Replace every character with 'c'
external "CWC"
alias "_STR_fill"
end; -- fill
------------------------------------------------------------------ fill_blank
fill_blank is
-- Fill with blanks
do
fill (' ');
ensure
--allblank : For every i in 1..count, item (i) = Blank
end; -- fill_blank
------------------------------------------------------------------------ head
head (n : INTEGER) is
-- Remove all characters except for the first 'n';
-- do nothing if n >= count
require
non_negative_argument : n >= 0
external "CWC"
alias "_STR_head"
ensure
new_count : count = n.min (old count)
--first_kept : For every i in 1..n, item (i) = old item (i)
end; -- head
---------------------------------------------------------------------- insert
insert (s : like Current; i : INTEGER) is
-- Add 's' to the left of position 'i'
require
string_exists : s /= Void;
good_key : valid_index (i)
local
j, k, n : INTEGER;
do
if Current = s then
insert (clone (s), i);
else
from
j := i;
n := s.count;
until
k = n
loop
k := k + 1;
insert_character (s.item (k), j);
j := j + 1;
end; -- loop
end; -- if
ensure
new_count : count = old (count + s.count)
end; -- insert
------------------------------------------------------------ insert_character
insert_character (c : CHARACTER; i : INTEGER) is
-- Add 'c' to the left of position 'i'
require
good_key : valid_index (i)
external "CWC"
alias "_STR_insert_character"
ensure
new_count : count = old count + 1
end; -- insert_character
----------------------------------------------------------------- left_adjust
left_adjust is
-- Remove leading white space
local
i, max_blank_index : INTEGER;
is_non_blank : BOOLEAN;
do
from
until
is_non_blank or else (i = count)
loop
i := i + 1;
if item (i).code <= (' ').code then
max_blank_index := i;
else
is_non_blank := True;
end; -- if
end; -- loop
if max_blank_index > 0 then
tail (count - max_blank_index);
end; -- if
ensure
new_count : (count /= 0) implies (item (1).code > (' ').code)
end; -- left_adjust
--------------------------------------------------------------------- precede
precede (ch : CHARACTER) is
-- Add 'ch' at front
external "CWC"
alias "_STR_precede"
ensure
new_count : count = old count + 1
end; -- precede
--------------------------------------------------------------------- prepend
prepend (s : STRING) is
-- Prepend a copy of 's' at front
require
argument_not_void : s /= Void
external "CWC"
alias "_STR_prepend"
ensure
new_count : count = old (count + s.count)
end; -- prepend
------------------------------------------------------------------------- put
put (c : CHARACTER; i : INTEGER) is
-- Replace character at position 'i' by 'c'
require
good_key : valid_index (i)
external "CWC"
alias "_STR_put"
ensure
insertion_done : item (i) = c
end; -- put
-------------------------------------------- replace_substring, put_substring
replace_substring, put_substring (
s : like Current; start_pos, end_pos : INTEGER
) is
-- 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
local
res : STRING;
do
if start_pos <= 1 then
res := "";
else
res := substring (1, start_pos - 1);
end; -- if
res.append (s);
if end_pos < count then
res.append (substring (end_pos + 1, count));
end; -- if
make_from_string (res);
ensure
new_count : count = old (count + s.count) - end_pos + start_pos - 1
end; -- replace_substring, put_substring
---------------------------------------------------------------- right_adjust
right_adjust is
-- Remove trailing white space
local
c : CHARACTER;
i, last_non_blank_index : INTEGER;
is_non_blank : BOOLEAN;
do
from
i := count;
until
is_non_blank or else (i < 1)
loop
c := item (i);
if c /= ' ' and c /= '%T' then
is_non_blank := True;
last_non_blank_index := i;
end; -- if
i := i - 1;
end; -- loop
head (last_non_blank_index);
ensure
new_count : (count /= 0) implies (item (count) /= ' ')
end; -- right_adjust
------------------------------------------------------------------------- set
set (t : like Current; n1, n2 : INTEGER) is
-- 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
meaningful_origin: 1 <= n1
meaningful_interval: n1 <= n2
meaningful_end: n2 <= t.count
do
if (n1 >= 1) and (n1 <= n2) and (n2 <= t.count) then
copy (t.substring (n1, n2));
else
wipe_out;
end; -- if
ensure
is_substring : is_equal (old clone (t.substring (n1, n2)))
end; -- set
------------------------------------------------------------------------ tail
tail (n : INTEGER) is
-- Remove all characters except for the last 'n'
require
non_negative_element : n >= 0
do
from
until
n >= count
loop
remove (1);
end; -- loop
ensure
new_count : count = n.min (old count)
end; -- tail
-----------------------------------------------------------------------------
feature -- Removal
----------------------------------------------------------------------- prune
prune (c : CHARACTER) is
-- Remove first occurrence of 'c', if any
local
i : INTEGER;
do
if count /= 0 then
i := index_of (c, 1);
if i /= 0 then
remove (i);
end; -- if
end; -- if
end; -- prune
------------------------------------------------------------------- prune_all
prune_all (c : CHARACTER) is
-- Remove all occurrences of 'c'
local
i : INTEGER;
do
from
i := 1;
until
i > count
loop
i := index_of (c, i);
if i = 0 then
i := count + 1;
else
remove (i);
end; -- if
end; -- loop
ensure
changed_count : count = (old count) - (old occurrences (c));
--removed : For every 'i' in 1..count, item (i) /= c;
no_more_occurrences : not has (c)
end; -- prune_all
---------------------------------------------------------------------- remove
remove (i : INTEGER) is
-- Remove 'i-th' character
require
good_key : valid_index (i)
external "CWC"
alias "_STR_remove"
ensure
new_count : count = old count - 1
end; -- remove
-------------------------------------------------------------------- wipe_out
wipe_out is
-- Remove all characters
do
remake (0);
ensure
empty_string : count = 0;
wiped_out : empty
end; -- wipe_out
-----------------------------------------------------------------------------
feature -- Resizing
---------------------------------------------------------------------- resize
resize (newsize : INTEGER) is
-- Rearrange string so that it can accommodate
-- at least 'newsize' characters.
-- Do not lose any previously entered characters
require
new_size_non_negative : newsize >= 0
local
s : STRING;
do
if newsize > count then
!!s.make (newsize - count);
append_string (s);
elseif newsize < count then
head (newsize);
end; -- if
end; -- resize
-----------------------------------------------------------------------------
feature -- Conversion
---------------------------------------------------------------------- mirror
mirror is
-- Reverse the order of characters.
-- "Hello world" -> "dlrow olleH"
local
tmp : CHARACTER;
i, j : INTEGER;
do
from
i := 1;
j := count;
until
i >= j
loop
tmp := item (i);
put (item (j), i);
put (tmp, j);
i := i + 1;
j := j - 1;
end; -- loop
ensure
same_count : count = old count;
--reversed : For every 'i' in 1..count, item (i) = old item (count+1-i)
end; -- mirror
-------------------------------------------------------------------- mirrored
mirrored : like Current is
-- Mirror image of string;
-- result for "Hello world" is "dlrow olleH"
do
Result := clone( Current );
Result.mirror;
ensure
same_count : Result.count = count;
--reversed : For every 'i' in 1..count, Result.item (i) = item (count+1-i)
end; -- mirrored
------------------------------------------------------------------ to_boolean
to_boolean : BOOLEAN is
-- Boolean value;
-- "true" yields 'true', "false" yields 'false' (case-insensitive)
local
s : STRING;
do
s := clone (Current);
s.right_adjust;
s.left_adjust;
s.to_lower;
Result := s.is_equal ("true");
end; -- to_boolean
----------------------------------------------- to_external, to_c, to_pointer
to_external, to_c, to_pointer : POINTER is
-- A pointer to a C from of current string.
-- Useful only for interfacing with C software
external "CWC"
alias "_STR_to_external"
end; -- to_external, to_c, to_pointer
------------------------------------------------------------------- to_double
to_double : DOUBLE is
-- Double value;
-- for example, when applied to "123.0", will yield 123.0 (double)
external "CWC"
alias "_STR_to_double"
end; -- to_double
------------------------------------------------------------------ to_integer
to_integer : INTEGER is
-- Integer value;
-- for example, when applied to "123", will yield 123
external "CWC"
alias "_STR_to_integer"
end; -- to_integer
-------------------------------------------------------------------- to_lower
to_lower is
-- Convert to lower case
external "CWC"
alias "_STR_to_lower"
end; -- to_lower
--------------------------------------------------------------------- to_real
to_real : REAL is
-- Real value;
-- for example, when applied to "123.0", will yield 123.0
external "CWC"
alias "_STR_to_real"
end; -- to_real
-------------------------------------------------------------------- to_upper
to_upper is
-- Convert to upper case
external "CWC"
alias "_STR_to_upper"
end; -- to_upper
-----------------------------------------------------------------------------
feature -- Duplication
------------------------------------------------------------------------ copy
copy (other : like Current) is
-- Reinitialize by copying the characters of 'other'.
-- (This is also used by 'clone'.)
-- (From GENERAL)
do
c_string_copy (other);
ensure then
new_result_count : count = other.count;
--same_characters : For every i in 1..count, item (i) = other.item (i)
end; -- copy
------------------------------------------------------------------- substring
substring (n1, n2 : INTEGER) : like Current is
-- Copy of substring containing all characters at indices
-- between 'n1' and 'n2'
require
meaningful_origin : 1 <= n1;
meaningful_interval : n1 <= n2;
meaningful_end : n2 <= count
do
!!Result.make (n2 - n1 + 1);
Result.c_string_fill_from_external (Current, n1, n2);
ensure
new_result_count : Result.count = n2 - n1 + 1
--original_characters : For every i in 1..n2 - n1,
-- Result.item (i) = item (n1 + i - 1)
end; -- substring
------------------------------------------------------------------- infix "+"
infix "+" (other: like Current): like Current is
-- Create a new object which is the concatenation of Current and `other'
require
non_void_other: other /= Void
do
Result := clone (Current)
Result.append_string (other)
ensure
non_void_result: Result /= Void
result_count: Result.count = count + other.count
definition:
Result.substring (1, count).is_equal (Current) and then
Result.substring (count + 1, Result.count).is_equal (other)
end; -- infix "+"
-----------------------------------------------------------------------------
feature -- Output
------------------------------------------------------------------------- out
out : STRING is
-- Printable representation
-- (From GENERAL)
do
Result := clone (Current);
ensure then
result_not_void : Result /= Void
end; -- out
-----------------------------------------------------------------------------
feature -- Eiffel/S 1.3 compatibility
----------------------------------------------------------------------- adapt
adapt (other : STRING) is
-- Initialize Current's text from string 's'
obsolete "Eiffel/S 1.3 compatibility"
require
not_void_other: other /= Void
do
make_from_string (other);
end; -- adapt
---------------------------------------------------------------------- append
append (other : STRING) is
-- Append 'other' to Current
obsolete "Eiffel/S 1.3 compatibility"
require
not_void_other: other /= Void
external "CWC"
alias "_STR_append_string"
end; -- append
------------------------------------------------------------------- fill_with
fill_with (c : CHARACTER) is
-- Fill entire string with character 'c'
obsolete "Eiffel/S 1.3 compatibility"
external "CWC"
alias "_STR_fill"
end; -- fill_with
---------------------------------------------------------------------- extend
extend (ch : CHARACTER) is
-- Append 'ch' to string
obsolete "Eiffel/S 1.3 compatibility"
external "CWC"
alias "_STR_extend"
end; -- extend
--------------------------------------------------------------------- compare
compare (other : like Current) : INTEGER is
obsolete "Eiffel/S 1.3 compatibility"
require else
not_void_other: other /= Void
external "CWC"
alias "_STR_compare"
end; -- compare
-----------------------------------------------------------------------------
feature {NONE} -- Implementation
--------------------------------------------------------------- c_string_copy
c_string_copy (other : like Current) is
external "CWC"
alias "_STR_copy"
end; -- c_string_copy
-----------------------------------------------------------------------------
feature {STRING} -- Implementation
------------------------------------------------- c_string_fill_from_external
c_string_fill_from_external (other:STRING; from_index, to_index:INTEGER) is
external "CWC"
alias "_STR_from_external"
end; -- c_string_fill_from_external
-----------------------------------------------------------------------------
invariant
empty_definition : empty = (count = 0);
non_negative_count : count >= 0
-----------------------------------------------------------------------------
end -- class STRING