| ELKS 2001 STRING Class |
  |
indexing
description: "Sequences of characters, accessible through %
%integer indices in a contiguous range starting %
%from one."
class interface
STRING
creation
make_empty
-- Create empty string.
ensure
empty: count = 0
make_filled (c: CHARACTER; n: INTEGER)
-- Create string of length n filled with c.
require
valid_count: n >= 0
ensure
count_set: count = n
filled: occurrences (c) = count
make (suggested_capacity: INTEGER)
-- Create empty string, or remove all characters from
-- existing string.
require
non_negative_suggested_capacity: suggested_capacity >= 0
ensure
empty_string: count = 0
make_from_string (s: STRING)
-- Initialize from the character sequence of s.
require
s_not_void: s /= Void
ensure
initialized: same_string (s)
feature -- Initialization
make (suggested_capacity: INTEGER)
-- Create empty string, or remove all characters from
-- existing string.
require
non_negative_suggested_capacity: suggested_capacity >= 0
ensure
empty_string: count = 0
from_c (c_string: POINTER)
-- Set the current STRING from a copy of the
-- zero-byte-terminated memory starting at `c_string'.
require
c_string_exists: c_string /= default_pointer
ensure
no_zero_byte: not has ('%/0/')
characters: -- for all i in 1..count, item(i) equals the
-- ASCII character at address c_string+i-1
correct_count: -- the ASCII character at address
-- c_string+count is NUL
make_from_string (s: STRING)
-- Initialize from the character sequence of s.
require
s_not_void: s /= Void
ensure
initialized: same_string (s)
feature -- Basic specifiers
count: INTEGER
-- Number of characters
item (i: INTEGER): CHARACTER
-- Character at index i
require
valid_index: valid_index (i)
feature -- Access
hash_code: INTEGER
-- Hash code value (vendor dependent hashing function)
-- (From HASHABLE.)
ensure
good_hash_value: Result >= 0
index_of (c: CHARACTER; start_index: INTEGER): INTEGER
-- Index of first occurrence of c at or after start_index;
-- 0 if none
require
valid_start_index: start_index >= 1 and 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)
string: STRING
-- New STRING having the same character sequence as Current
ensure
string_not_void: Result /= Void
string_type: Result.same_type ("")
first_item: count > 0 implies Result.item (1) = item (1)
recurse: count > 1 implies
Result.substring (2, count).is_equal (substring (2, count).string)
substring (start_index, end_index: INTEGER): like Current
-- New object containing 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
substring_not_void: Result /= Void
substring_count: Result.count = end_index - start_index + 1
first_item: Result.count > 0 implies Result.item (1) = item (start_index)
recurse: Result.count > 0 implies
Result.substring (2, Result.count).is_equal
(substring (start_index + 1, end_index))
substring_index (other: STRING; start_index: INTEGER): INTEGER
-- Index of first occurrence of other at or after start_index;
-- 0 if none
require
other_not_void: other /= Void
valid_start_index: start_index >= 1 and start_index <= count + 1
ensure
valid_result: Result = 0 or else
(start_index <= Result and Result <= count - other.count + 1)
zero_if_absent: (Result = 0) =
not substring (start_index, count).has_substring (other)
at_this_index: Result >= start_index implies
other.same_string (substring (Result, Result + other.count - 1))
none_before: Result > start_index implies
not substring (start_index, Result + other.count - 2).has_substring (other)
infix "@" (i: INTEGER): CHARACTER
-- Character at index i
require
valid_index: valid_index (i)
ensure
definition: Result = item (i)
feature -- Measurement
occurrences (c: CHARACTER): INTEGER
-- Number of times c appears in the string
ensure
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)
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object considered equal
-- to current object?
-- (Redefined from GENERAL.)
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_equal (Current)
definition: Result = (same_type (other) and then
count = other.count and then
(count > 0 implies (item (1) = other.item (1) and
substring (2, count).is_equal (other.substring (2, count)))))
same_string (other: STRING): BOOLEAN
-- Do Current and other have the same character sequence?
require
other_not_void: other /= Void
ensure
definition: Result = string.is_equal (other.string)
infix "<" (other: STRING): BOOLEAN
-- Is string lexicographically lower than other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
asymmetric: Result implies not (other < Current)
definition: Result = (count = 0 and other.count > 0 or
count > 0 and then other.count > 0 and then
(item (1) < other.item (1) or
item (1) = other.item (1) and
substring (2, count) < other.substring (2, other.count)))
infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal to other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (Current < other or is_equal (other))
infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or equal to other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (other <= Current)
infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (other < Current)
max (other: like Current): like Current
-- The greater of current object and other
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
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
other_exists: other /= Void
ensure
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
other_exists: other /= Void
ensure
equal_zero: (Result = 0) = is_equal (other)
smaller: (Result = -1) = Current < other
greater_positive: (Result = 1) = Current > other
feature -- Status report
has (c: CHARACTER): BOOLEAN
-- Does Current contain 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))
has_substring (other: STRING): BOOLEAN
-- Does Current contain other?
require
other_not_void: other /= Void
ensure
false_if_too_small: count < other.count implies not Result
true_if_initial: (count >= other.count and then
other.same_string (substring (1, other.count)))
implies Result
recurse: (count >= other.count and then
not other.same_string (substring (1, other.count))) implies
(Result = substring (2, count).has_substring (other))
is_boolean: BOOLEAN
-- Does Current represent a BOOLEAN?
ensure
is_boolean: Result = (same_string ("true") or same_string ("false"))
is_double: BOOLEAN
-- Does Current represent a DOUBLE?
ensure
syntax_and_range:
-- Result is true if and only if the following two
-- conditions are satisfied:
--
-- 1. In the following BNF grammar, the value of
-- Current can be produced by "Real_literal":
--
-- Real_literal = Mantissa [Exponent_part]
-- Exponent_part = "E" Exponent
-- | "e" Exponent
-- Exponent = Integer_literal
-- Mantissa = Decimal_literal
-- Decimal_literal = Integer_literal ["." Integer]
-- Integer_literal = [Sign] Integer
-- Sign = "+" | "-"
-- Integer = Digit | Digit Integer
-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
--
-- 2. The numerical value represented by Current
-- is within the range that can be represented
-- by an instance of type DOUBLE.
is_empty: BOOLEAN
-- Is string empty?
ensure
definition: Result = (count = 0)
is_integer: BOOLEAN
-- Does Current represent an INTEGER?
ensure
syntax_and_range:
-- Result is true if and only if the following two
-- conditions are satisfied:
--
-- 1. In the following BNF grammar, the value of
-- Current can be produced by "Integer_literal":
--
-- Integer_literal = [Sign] Integer
-- Sign = "+" | "-"
-- Integer = Digit | Digit Integer
-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
--
-- 2. The integer value represented by Current
-- is within the (inclusive) range
-- minimum_integer..maximum_integer
-- where `minimum_integer' and `maximum_integer'
-- are the constants defined in class PLATFORM.
is_real: BOOLEAN
-- Does Current represent a REAL?
ensure
syntax_and_range:
-- Result is true if and only if the following two
-- conditions are satisfied:
--
-- 1. In the following BNF grammar, the value of
-- Current can be produced by "Real_literal":
--
-- Real_literal = Mantissa [Exponent_part]
-- Exponent_part = "E" Exponent
-- | "e" Exponent
-- Exponent = Integer_literal
-- Mantissa = Decimal_literal
-- Decimal_literal = Integer_literal ["." Integer]
-- Integer_literal = [Sign] Integer
-- Sign = "+" | "-"
-- Integer = Digit | Digit Integer
-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
--
-- 2. The numerical value represented by Current
-- is within the range that can be represented
-- by an instance of type REAL.
valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the string?
ensure
definition: Result = (1 <= i and i <= count)
feature -- Element change
append_character (c: CHARACTER)
-- Append c at end.
ensure
new_count: count = old count + 1
appended: item (count) = c
stable_before: substring (1, count - 1).is_equal (old clone (Current))
append_string (s: STRING)
-- Append a copy of s at end.
require
s_not_void: s /= Void
ensure
appended: is_equal (old clone (Current) + old clone (s))
fill_with (c: CHARACTER)
-- Replace every character with c.
ensure
same_count: old count = count
filled: occurrences (c) = count
insert_character (c: CHARACTER; i: INTEGER)
-- 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: substring (1, i - 1).is_equal (old substring (1, i - 1))
stable_after_i: substring (i + 1, count).is_equal (old substring (i, count))
insert_string (s: STRING; i: INTEGER)
-- Insert s at index i, shifting characters between ranks
-- i and count rightwards.
require
string_not_void: s /= Void
valid_insertion_index: 1 <= i and i <= count + 1
ensure
inserted: is_equal (old substring (1, i - 1)
+ old clone (s) + old substring (i, count))
put (c: CHARACTER; i: INTEGER)
-- Replace character at index i by c.
require
valid_index: valid_index (i)
ensure
stable_count: count = old count
replaced: item (i) = c
stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1))
stable_after_i: substring (i + 1, count).is_equal (old substring (i + 1, count))
replace_substring (s: STRING; start_index, end_index: INTEGER)
-- Replace the substring from start_index to end_index,
-- inclusive, with s.
require
string_not_void: s /= Void
valid_start_index: 1 <= start_index
valid_end_index: end_index <= count
meaningful_interval: start_index <= end_index + 1
ensure
replaced: is_equal (old (substring (1, start_index - 1) +
s + substring (end_index + 1, count)))
feature -- Removal
keep_head (n: INTEGER)
-- Remove all the characters except for the first n;
-- if n > count, do nothing.
require
n_non_negative: n >= 0
ensure
kept: is_equal (old substring (1, n.min (count)))
keep_tail (n: INTEGER)
-- Remove all the characters except for the last n;
-- if n > count, do nothing.
require
n_non_negative: n >= 0
ensure
kept: is_equal (old substring (count - n.min (count) + 1, count))
remove (i: INTEGER)
-- Remove i-th character, shifting characters between
-- ranks i + 1 and count leftwards.
require
valid_removal_index: valid_index (i)
ensure
removed: is_equal (old substring (1, i - 1) +
old substring (i + 1, count))
remove_head (n: INTEGER)
-- Remove the first n characters;
-- if n > count, remove all.
require
n_non_negative: n >= 0
ensure
removed: is_equal (old substring (n.min (count) + 1, count))
remove_substring (start_index, end_index: INTEGER)
-- 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: is_equal (old (substring (1, start_index - 1) +
old (substring (end_index + 1, count))
remove_tail (n: INTEGER)
-- Remove the last n characters;
-- if n > count, remove all.
require
n_non_negative: n >= 0
ensure
removed: is_equal (old substring (1, count - n.min (count)))
wipe_out
-- Remove all characters.
ensure
empty_string: count = 0
feature -- Conversion
as_lower: like Current
-- New object with all letters in lower case
ensure
length: Result.count = count
anchor: count > 0 implies Result.item (1) = item (1).as_lower
recurse: count > 1 implies
Result.substring (2, count).is_equal (substring (2, count).as_lower)
as_upper: like Current
-- New object with all letters in upper case
ensure
length: Result.count = count
anchor: count > 0 implies Result.item (1) = item (1).as_upper
recurse: count > 1 implies
Result.substring (2, count).is_equal (substring (2, count).as_upper)
to_boolean: BOOLEAN
-- Boolean value;
-- "true" yields true, "false" yields false
require
represents_a_boolean: is_boolean
ensure
to_boolean: Result = same_string ("true")
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
represents_an_integer: is_integer
ensure
single_digit: count = 1 implies
Result = ("0123456789").index_of (item (1), 1) - 1
minus_sign_followed_by_single_digit:
count = 2 and item (1) = '-' implies
Result = - substring (2, 2).to_integer
plus_sign_followed_by_single_digit:
count = 2 and item (1) = '+' implies
Result = substring (2, 2).to_integer
recurse_to_reduce_length:
count > 2 or count = 2 and not (("+-").has (item (1))) implies
Result // 10 = substring (1, count - 1).to_integer and
(Result \\ 10).abs = substring (count, count).to_integer
to_lower
-- Convert all letters to lower case.
ensure
length_and_content: is_equal (old as_lower)
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 all letters to upper case.
ensure
length_and_content: is_equal (old as_upper)
feature -- Duplication
copy (other: like Current)
-- Reinitialize by copying the characters of other.
-- (This is also used by clone.)
-- (From GENERAL.)
require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)
infix "+" (other: STRING): like Current
-- New object which is a clone of `Current' extended
-- by the characters of `other'.
require
other_exists: other /= Void
ensure
result_not_void: Result /= Void
result_count: Result.count = count + other.count
initial: Result.substring (1, count).is_equal (Current)
final: Result.substring (count + 1, count + other.count).same_string (other)
feature -- Output
out: STRING
-- New STRING containing terse printable representation
-- of current object
-- (From GENERAL.)
ensure
out_not_void: Result /= Void
same_items: same_type ("") implies Result.same_string (Current)
invariant
irreflexive_comparison: not (Current < Current)
-- (From COMPARABLE.)
non_negative_count: count >= 0
end
-- The correctness of this specification is based on the following
-- assumptions:
--
-- 1. No feature of STRING calls a command on any of its arguments.
--
-- 2. No query of STRING changes the value of any basic specifier.
--
-- 3. No feature of STRING shares internal structures in any way
-- that could lead to behaviour not deducible from this
-- specification.
--
-- 4. The phrase "new STRING" in a header comment means a
-- newly-created STRING to which there is no reference other than
-- from `Result'.
--
-- 5. The phrase "new object" in a header comment means a
-- newly-created object of type "like Current" to which
-- there is no reference other than from `Result'.
Copyright © 2001, Nonprofit
International Consortium for Eiffel
Last Updated: 28 December 2001
|
  |