| work in progress | string |
Here's a cut at STRING. The starting point was the Elks 2000 proposal from Dominique, Manu, and Olivier. That version was quite well done with many features completely or nearly completely specified. (The inclusion of a concatenation operator, "+" is particularly important and useful.) I've tried to be even more complete and to use compilable specs whenever possible. In a few cases I've recommended some additional features as I think they may be useful in their own right as well as helping with the spec. I particular, "has_substring" seems like a natural.
In each case I've tried to mark the changes I made from the original. I've also tried to be clear where I'm not sure how to write the spec.
I _think_ the only really controversial issue here is that of `capacity'. I've pretty much punted on that issue for now.
Enjoy,
-- Jim McKim
indexing
description: "Resizable sequences of characters, accessible through %
%integer indices in a contiguous range. If not empty, first element%
%is at index 1."
Basic specifiers: count, item
Auxiliary specifiers (1): valid_index, substring, is_equal, "<" Auxiliary specifiers (2): has, has_substring, same_as, "+" Auxiliary specifiers (3): occurrences
class interface STRING creation make (n: INTEGER) -- Allocate space for at least n characters. require non_negative_size: n >= 0 ensure empty_string: count = 0 correctly_allocated_size: capacity >= n
[Same problems with `capacity' as in ARRAY. Just kill it and provide a `make_empty' routine? Include `requested_capacity'? Leave as is?]
make_from_external (ptr: POINTER) -- Set Current with a copy of the content of ptr. -- Assume ptr is a null-terminated memory area containing -- only characters. -- The extra null character is not part of the Eiffel string require ptr_exists: ptr /= 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 count_set: count = s.count
[Can't claim is_equal (s) here, 'cause descendant won't be of type STRING. Can we say for_all i, 1..count (item (i) = s.item (i))? Can we say anything?]
feature -- Initialization make (n: INTEGER) -- Allocate space for at least n characters. require non_negative_size: n >= 0 ensure empty_string: count = 0 correctly_allocated_size: capacity >= n
make_from_external (ptr: POINTER) -- Set Current with a copy of the content of ptr. -- Assume ptr is a null-terminated memory area containing -- only characters. -- The extra null character is not part of the Eiffel string require ptr_exists: ptr /= 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 count_set: count = s.count
feature - Access
first: CHARACTER -- First character of Current. require not_empty_string: count > 0 ensure definition: Result = item (1)
[Changed precondition to reduce dependencies, changed tag of postcondition]
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))
[Complete spec.]
has_substring (other : STRING ) : BOOLEAN -- Does Current contain `other'? require other_not_void: other /= Void other_not_empty: other.count > 0 ensure false_if_too_small: count < other.count implies not Result true_if_initial: (count >= other.count and then other.is_equal (substring (1, other.count)) implies Result recurse: (count >= other.count and then not other.is_equal (substring (1, other.count)) implies (Result = substring (2, count).has_substring (other))
[New routine. Parallel to `has'. Makes corresponding `index' routines easier to describe. Useful in its own right?]
hash_code: INTEGER -- Hash code value -- (From HASHABLE.) ensure good_hash_value: Result >= 0 -- Vendor dependent hashing function
[Added comment]
index_from (c: CHARACTER; start_index: INTEGER): INTEGER
-- Index of first occurrence of c at or after start_index;
-- 0 if none.
require
valid_start_index: valid_index (start_index)
ensure
valid_result:
Result >= 0 or (start_index <= Result and Result <= count)
zero_if_absent: (Result = 0) = not has (c)
found_if_present: has (c) implies item (Result) = c
none_before: has (c) implies
not substring (start_index, Result - 1).has (c)
[Compilable version, perhaps simpler.]
index_of (c: CHARACTER): INTEGER
-- Index of first occurrence of c;
-- 0 if none.
ensure
valid_result: Result >= 0 and Result <= count
zero_if_absent: (Result = 0) = not has (c)
found_if_present: has (c) implies item (Result) = c
none_before: has (c) implies
not substring (1, Result - 1).has (c)
[Removed dependency on `index_from', not necessarily a good thing, as
this version is more complex.]
item (i: INTEGER): CHARACTER
-- Character at index i
-- Basic specifier
require
good_key: valid_index (i)
infix "@": CHARACTER
-- Character at index i
require
good_key: valid_index (i)
ensure
definition: Result = item (i)
[Split `item' and `@' in order to define one in terms of the other.]
last: CHARACTER
-- Last character of Current.
require
not_empty_string: count > 0
ensure
definition: Result = item (count)
[Changed precondition to reduce dependencies, changed tag of postcondition]
reverse_index_from (c: CHARACTER; last_index: INTEGER): INTEGER -- Index of first occurrence of c at or before last_index; -- 0 if none. require valid_last_index: valid_index (last_index) ensure valid_result: Result >= 0 and Result <= last_index zero_if_absent: (Result = 0) = not has (c) present_implies_found: has (c) implies item (Result) = c none_after: has (c) implies not substring (Result + 1, last_index).has (c)
[Compilable, perhaps simpler]
reverse_index_of (c: CHARACTER): INTEGER -- Index of last occurrence of c; -- 0 if none. ensure valid_result: Result >= 0 and Result <= count zero_if_absent: (Result = 0) = not has (c) present_implies_found: has (c) implies item (Result) = c none_after: has (c) implies not substring (Result + 1, count).has (c)
[Removed dependency on `index_from', not necessarily a good thing, as this version is more complex.]
reverse_string_index_from (other: STRING; last_index: INTEGER): INTEGER
-- Index of first occurrence of `other' at or before
-- `last_index'; 0 if none.
require
other_not_void: other /= Void
other_not_empty: other.count > 0
valid_last_index: valid_index (last_index)
ensure
valid_result: Result >= 0 and Result <= last_index
zero_if_absent: (Result = 0) =
not substring (1, count.min (last_index + other.count-1).has_substring (other)
enough_room: Result > 0 implies
(Result + other.count-1 <= count)
at_this_index: Result > 0 implies
other.is_equal (substring (Result, Result + other.count - 1))
none_after:
not substring (Result + 1, count.min (last_index + other.count - 1).has_substring (other))
[Added not_void precondition. Used has_substring to simplify and make compilable.]
reverse_string_index_of (other: STRING): INTEGER -- Index of last occurrence of other; -- 0 if none. require other_not_void: other /= Void other_not_empty: other.count > 0 ensure valid_result: Result >= 0 and Result <= count zero_if_absent: (Result = 0) = not has_substring (other) enough_room: Result > 0 implies Result + other.count - 1 <= count at_this_index: Result > 0 implies other.is_equal (substring (Result, Result + other.count - 1)) none_after: not substring (Result + 1, count).has_substring (other))
[Removed dependency on reverse_string_index_from. Adds complexity though.]
string_index_from (other: STRING; start_index: INTEGER): INTEGER
-- Index of first occurrence of other at or after start;
-- 0 if none.
require
other_not_void: other /= Void
other_not_empty: other.count > 0
valid_start_index: valid_index (start_index)
ensure
valid_result: Result = 0 or else
(start_index <= Result and Result <= count)
zero_if_absent: (Result = 0) =
not substring (start_index, count).has_substring (other)
enough_room: Result >= start_index implies
Result + other.count - 1 <= count
at_this_index: Result >= start_index implies
other.is_equal (substring (Result, Result + other.count - 1))
none_before: Result >= start_index implies
not substring (start_index, Result + other.count - 2).has_substring (other))
[Used has_substring to simplify and make compilable.]
string_index_of (other: STRING): INTEGER -- Index of first occurrence of other; -- 0 if none. require other_not_void: other /= Void other_not_empty: other.count > 0 ensure valid_index: 0 <= Result and Result <= count zero_if_absent: (Result = 0) = not has_substring (other) enough_room: Result > 0 implies Result + other.count - 1 < count at_index: Result > 0 implies other.is_equal (substring (Result, Result + other.count - 1)) none_before: Result > 0 implies not substring (1, Result + other.count - 2).has_substring (other))
[Removed dependency on string_index_from, paying some cost in complexity.]
feature -- Measurement
count: INTEGER
-- Current number of characters making up the string
-- Basic specifier
capacity: INTEGER
-- Number of characters that Current can currently contain
-- in the internal storage area.
-- Automatically updated when resizing is needed. Useful
-- for fine tuning.
ensure
large_enough: Result >= count -- nondeterministic
[Added postcondition]
occurrences (c: CHARACTER): INTEGER
-- Number of times c appears in the string
ensure
zero_if_empty: count = 0 implies Result = 0
simple_recurse: (count > 0 and then item (1) /= c) implies
Result = substring (2, count).occurrences
Recurse_and_add: (count > 0 and then item (1) = c) implies
Result = 1 + substring (2, count).occurrences
[Complete spec.]
feature - Comparison
is_equal (other: like Current): BOOLEAN
-- Is string made of same character sequence as other?
-- (Redefined from GENERAL.)
require
other_not_void: other /= Void
ensure
definition: Result = (count = other.count and then
(count > 0 implies (item (1) = other.item (1) and
substring (2, count).is_equal (other.substring (2, count)))
[Added postcondition]
infix "<" (other: like Current): BOOLEAN
-- Is string lexicographically lower than other?
-- (False if other is void)
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
asymmetric: Result implies not (other < Current)
ensure then
definition: Result = (count = 0 and other.count > 0) or else
(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, count))))
[Completed spec.]
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)
same_as (other: STRING): BOOLEAN
-- Is string made of same character sequence as other?
-- Case insensitive comparison.
require
other_exists: other /= Void
ensure
definition:
Result = (count = other.count and then (count > 0 implies
(item (1).upper = other.item (1).upper and
substring (2, count).same_as (other.substring (2, count))))
[Completed spec, note that this assumes CHARACTER has a feature `upper' or equivalent.]
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
is_empty: BOOLEAN
-- Is string empty?
ensure
definition: Result = (count = 0)
valid_index (index: INTEGER): BOOLEAN
-- Is `index' within the bounds of the string?
ensure
definition: Result = (1 <= index and index <= count)
[Changed comment `i' to `index']
is_boolean: BOOLEAN
-- Is Current representing a boolean ("true" or "false" with no
-- case consideration)?
ensure
definition: Result = (same_as ("TRUE") or same_as ("FALSE"))
[Added postcondition.]
is_double: BOOLEAN
-- Can Current be read as a DOUBLE?
false_if_empty: count = 0 implies not Result
[gulp. Not sure what all the possibilities are here.]
is_integer: BOOLEAN
-- Can Current be read as an INTEGER?
false_if_empty: count = 0 implies not Result
false_if_bad_start:
count > 0 and not item (1).is_digit implies not Result
true_anchor: count = 1 and item (1).is_digit implies Result
recurse: count > 0 and item (1).is_digit implies
Result = substring (2, count).is_integer
[Added postcondition. Assumes no leading or trailing white space is allowed.]
is_real: BOOLEAN
-- Can Current be read as a REAL?
false_if_empty: count = 0 implies not Result
[gulp. Not sure what all the possibilities are here.]
feature -- Element change
add, insert (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
inserted:
is_equal (old substring (1, i - 1) + c.out + old substring (i, count)
[Completed and simplified postcondition. Needed, given `put'?]
add_first, precede (c: CHARACTER)
-- Prepend c at beginning.
ensure
inserted: is_equal (c.out + old clone (Current))
[Completed and simplified postcondition]
add_last, append_character, extend (c: CHARACTER)
-- Append c at end.
ensure
inserted: is_equal (old clone (Current) + c.out)
[Completed and simplified postcondition]
append, append_string (s: STRING)
-- Append a copy of s at end.
require
other_exists: s /= Void
ensure
appended: is_equal (old clone (Current) + old clone (s))
[Completed and simplified postcondition.]
append_boolean (b: BOOLEAN)
-- Append the string representation of b at end.
ensure
appended: is_equal (old clone (Current) + b.out)
[Completed and simplified postcondition.]
append_double (d: DOUBLE)
-- Append the string representation of d at end.
ensure
appended: is_equal (old clone (Current) + d.out)
[Completed and simplified postcondition.]
append_integer (i: INTEGER)
-- Append the string representation of i at end.
ensure
appended: is_equal (old clone (Current) + i.out)
[Completed and simplified postcondition.]
append_real (r: REAL)
-- Append the string representation of r at end.
ensure
appended: is_equal (old clone (Current) + r.out)
[Completed and simplified postcondition.]
fill (c: CHARACTER)
-- Replace every character with c.
ensure
same_count: old count = count
filled: occurrences(c) = count
head (n: INTEGER)
-- Remove all characters except for the first n;
-- do nothing if n >= count.
require
non_negative_argument: n >= 0
ensure
first_kept: is_equal (old substring (1, n.min (count)))
[Should have a verb name. Completed and simplified postcondition.]
insert_string (s: like Current; i: INTEGER)
-- Insert s at index i, shifting characters between ranks
-- i and count rightwards.
require
string_exists: 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))
[Completed and simplified postcondition.]
left_adjust
-- Remove leading white space.
ensure
shorter: count <= old count
first_not_white_space: not is_empty implies
("%T%R%N ").index_of (first) = 0
[Warning! _Long_ comment coming. (That second clause is really quite clever!) I've never been sure why this feature isn't called `remove_leading_white_space'. Anyway, I don't see a way to give a complete, compilable spec without some help. I can give a complete spec as a comment. Something like
-- there_exists k, 1..old count
((old clone(Current)).is_equal(old substring(1, k) + Current) and
for_all i, 1..k (("%T%R%N ").index_of (old item (i)) > 0)) and
(k = old count or else (("%T%R%N ").index_of (old item (k + 1) = 0)))
Whew!
The help I would need to write a compilable spec is a feature like
first_dark_index : INTEGER
-- Index of first character that is not white space, count + 1
-- if no such character.
ensure
empty_case: count = 0 implies Result = 1
dark_anchor:
count > 0 and then ("%T%R%N ").index_of (item (1)) = 0 implies Result = 1
recurse:
count > 0 and then ("%T%R%N ").index_of (item (1)) > 0 implies
Result = 1 + substring (2, count).first_dark_index
Now the postcondition for `left_adjust' is just one line
(old clone (Current)).is_equal (old substring(1, first_dark_index-1) + Current)
Trouble is, I'm not convinced `first_dark_index' is independently useful enough to be in the kernel.]
put (c: CHARACTER; i: INTEGER)
-- Replace character at index i by c.
require
good_key: valid_index (i)
ensure
inserted:
is_equal (old substring (1, i - 1) + c.out + old substring (i, count))
[Completed postcondition.]
right_adjust
-- Remove trailing white space.
ensure
shorter: count <= old count
last_not_white_space: not is_empty implies
("%T%R%N ").index_of (last) = 0
[Similar comments to `left_adjust'.]
subcopy (other: like Current; start_pos, end_pos, from_index: INTEGER) is
-- Copy characters of other within bounds start_pos and
-- end_pos to current string starting at index from_index.
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
valid_from_index: valid_index (from_index)
enough_space: valid_index (from_index + end_pos - start_pos)
ensure
copied: is_equal (old substring (1, from_index - 1) +
old other.substring (start_pos, end_pos) +
old substring (from_index + end_pos - start_pos + 1, old count))
[Completed postcondition.]
tail (n: INTEGER)
-- Remove all characters except for the last n;
-- do nothing if n >= count.
require
non_negative_argument: n >= 0
ensure
last_kept:
is_equal (old substring (count - n.min (count) + 1, count))
[Should have a verb name. Completed and simplified postcondition.]
feature -- Removal
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)
[Completed postcondition.]
wipe_out
-- Remove all characters.
ensure
empty_string: count = 0
[Removed `same_capacity' from postcondition as not sure what to do about `capacity' in general yet. Removed `same_lower', I think it was just a slip that it was there in the first place.]
feature -- Conversion
to_boolean: BOOLEAN
-- Boolean value;
-- "true" yields true, "false" yields false
-- (case-insensitive)
require
is_boolean: is_boolean
ensure
converted: Result = same_as ("TRUE")
[The comment doesn't say anything about removing white space, but ISE's
implementation does. If that's what we want then maybe those `dark_index'
features aren't so crazy. We could use
converted: Result = substring (first_dark_index, last_dark_index).same_as ("TRUE")
to_double: DOUBLE
-- Double value; for example, when applied to "123.0",
-- will yield 123.0 (double)
require
is_double: is_integer or is_real or is_double
[Not sure what to do for postcondition here. Help!]
to_external: POINTER
-- Address of the storage area containing the actual
-- sequence of characters,
-- to be passed to some external (non-Eiffel) routine.
-- Keep in mind that this storage area is subject to garbage
-- collection.
to_integer: INTEGER
-- Integer value;
-- for example, when applied to "123", will yield 123
require
is_integer: is_integer
[Not sure what to do for postcondition here. Help!]
to_lower
-- Convert to lower case.
ensure
same_count: count = old count
converted:
-- for_all i, 1..count (item (i) = old item (i).lower)
[I don't see a compilable version without a query version of this (lower?), but at least the comment is pretty simple in this case.]
to_real: REAL
-- Real value;
-- for example, when applied to "123.0", will yield 123.0
require
is_real: is_integer or is_real
[Not sure what to do for postcondition here. Help!]
to_upper
-- Convert to upper case.
ensure
same_count: count = old count
converted:
-- for_all i, 1..count (item (i) = old item (i).upper)
[Same issues as with `to_lower'.]
feature -- Duplication
copy (other: like Current)
-- Reinitialize by copying the characters of other.
-- (From GENERAL.)
ensure
new_result_count: count = other.count
-- same_characters: For every i in 1..count,
-- item (i) = other.item (i)
[I didn't change this, but there's no need for any new postconditions, is there? The postcondition from GENERAL is `is_equal (other)' which covers both of these.]
infix "+" (other: STRING): like Current
-- Create a new object which is the concatenation of Current and other.
require
other_exists: other /= Void
ensure
result_count: Result.count = count + other.count
initial: Result.substring (1..count).is_equal (Current)
final:
Result.substring (count + 1, count + other.count).is_equal (other)
[Completed postcondition]
substring (start_index, end_index: INTEGER): like Current
-- Create a substring containing all characters from start_index
-- to end_index included.
require
valid_start_index: 1 <= start_index
valid_end_index: end_index <= count
meaningful_interval: start_index <= end_index + 1
ensure
result_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))
[Major changes in precondition to allow various empty cases. Completed postcondition.]
feature -- Output
out: STRING
-- Printable representation
-- (From GENERAL.)
ensure
result_not_void: Result /= Void
duplicated_result: Result /= Current and Result.is_equal (Current)
feature -- Optimization
adjust_capacity (n: INTEGER)
-- Rearrange string so that it can accommodate
-- at least n characters.
-- Do not lose any previously entered character.
require
no_item_lost: n >= count
ensure
enough_capacity: capacity >= n
invariant non_negative_count: count >= 0 capacity_big_enough: capacity >= count end
Copyright (c) 1995, Nonprofit International Consortium for Eiffel
Last Updated: 01 September 1999