| work in progress | string |
- Strongly prefer to KEEP these features
- manus@eiffel.com
- Prefer to KEEP these features
- usander@online.de
- xavier@halstenbach.com
- ericb@gobosoft.com
- Prefer to REMOVE these features
- sparker@eiffel.ie
- saunderscj2000@yahoo.com
- gmc333@my-deja.com
- kwaxer@aha.ru
- franck@nenie.org
- arno.wagner@acm.org
- peter@deakin.edu.au
- Don't mind (happy either way)
- chcouder@club-internet.fr
10 FEBRUARY 2001 VERSION:
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)
The PREVIOUS version of 'index_of' looks like this:
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 has (c)
found_if_present:
has (c) implies item (result) = c
none_before: has (c)
implies
not substring (start_index, result - 1).has (c)
The difference between the previous version and the proposed new version
is that the new version fixes an error in the previous version. The
previous version only worked for a 'start_index' of 1. The bug was
analysed in Xavier Le Vourch's message of 28 January 2001, and the
proposed new version incorporates Xavier's fix.
The fix consists of replacing "has (c)" by "substring (start_index,
count).has (c)" in three places.
- Strongly accept the proposal
- usander@online.de
- xavier@halstenbach.com
- Accept the proposal
- sparker@eiffel.ie
- saunderscj2000@yahoo.com
- gmc333@my-deja.com
- kwaxer@aha.ru
- franck@nenie.org
- arno.wagner@acm.org
- manus@eiffel.com
- chcouder@club-internet.fr
- ericb@gobosoft.com
- peter@deakin.edu.au
13 FEBRUARY 2001 VERSIONS:
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.
to_real: REAL
-- Real value;
-- for example, when applied to "123.0",
will yield 123.0
require
represents_a_real:
is_real
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.
to_double: DOUBLE
-- "Double" value; for example, when
applied to "123.0",
-- will yield 123.0 (double)
require
represents_a_double:
is_double
The PREVIOUS versions of 'to_real' and 'to_double' were from ELKS95,
and
look like this:
to_real: REAL
-- Real value;
-- for example, when applied to "123.0",
will yield 123.0
to_double: DOUBLE
-- "Double" value; for example, when
applied to "123.0",
-- will yield 123.0 (double)
The difference between the previous versions and the proposed new
versions is the addition of a precondition to require that the STRING
is
convertible.
- Accept the proposal
- saunderscj2000@yahoo.com
- xavier@halstenbach.com
- pgcrism@attglobal.net
- ericb@gobosoft.com
- kwaxer@aha.ru
- sparker@eiffel.ie
- arno.wagner@acm.org
- gmc333@my-deja.com
- franck@nenie.org (by email)
17 FEBRUARY 2001 VERSION:
infix "<" (other: STRING): BOOLEAN
-- Is string lexicographically lower
than other?
-- (Inherited from COMPARABLE.)
require -- from COMPARABLE
other_exists: other
/= Void
ensure -- from COMPARABLE
asymmetric: Result
implies not (other < Current)
ensure then
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)))
The PREVIOUS version (from ELKS95) looks like this:
infix "<" (other: STRING): 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)
The differences between the previous version and the proposed new
version are:
- The behaviour of infix "<" in class STRING is
specified rigorously in terms of CHARACTER
comparisons by the 'definition' postcondition
- the phrase "Inherited from COMPARABLE" replaces
"From COMPARABLE" within the header comments
- the comment "-- from COMPARABLE" has been added to
inherited assertions
- Accept the proposal
- manus@eiffel.com
- gmc444@yahoo.com
- franck@nenie.org
- xavier@halstenbach.com
- chcouder@club-internet.fr
- saunderscj2000@yahoo.com
- peter@deakin.edu.au
- ericb@gobosoft.com
- kwaxer@aha.ru
- arno.wagner@acm.org
- James McKim (by email)
19 FEBRUARY 2001 VERSIONS:
infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal
to other?
-- (Inherited from COMPARABLE.)
require -- from COMPARABLE
other_exists: other
/= Void
ensure -- from COMPARABLE
definition: Result
= (Current < other or is_equal (other))
infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or
equal to other?
-- (Inherited from COMPARABLE.)
require -- from COMPARABLE
other_exists: other
/= Void
ensure -- from COMPARABLE
definition: Result
= (other <= Current)
infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (Inherited from COMPARABLE.)
require -- from COMPARABLE
other_exists: other
/= Void
ensure -- from COMPARABLE
definition: Result
= (other < Current)
max (other: like Current): like Current
-- The greater of current object and
other
-- (Inherited 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
-- (Inherited 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.
-- (Inherited from COMPARABLE.)
require -- from COMPARABLE
other_exists: other
/= Void
ensure -- from COMPARABLE
equal_zero: (Result
= 0) = is_equal (other)
smaller: (Result =
-1) = Current < other
greater_positive:
(Result = 1) = Current > other
The PREVIOUS versions of these features (from ELKS95) look like this:
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
The differences between the previous versions and the proposed new
versions are:
- the phrase "Inherited from COMPARABLE" replaces
"From COMPARABLE" within the header comments
- the comment "-- from COMPARABLE" has been added to
inherited assertions
- the unbalanced parenthesis that appeared at the end
of the ELKS95 signatures of 'max', 'min' and
'three_way_comparison' has been removed
- three trailing semicolons have been removed from
the postcondition of infix "<="
- Accept the proposal
- manus@eiffel.com
- gmc444@yahoo.com
- franck@nenie.org
- xavier@halstenbach.com
- chcouder@club-internet.fr
- saunderscj2000@yahoo.com
- ericb@gobosoft.com
- kwaxer@aha.ru
- arno.wagner@acm.org
- James McKim (by email)
- Reject the proposal
- peter@deakin.edu.au
Class STRING - 08 MARCH 2001 VERSION
as_lower: STRING
-- New string 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: STRING
-- New string 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)
These features are not present in ELKS95. If accepted into
ELKS 2001
STRING, it is anticipated that STRING 'to_lower' and 'to_upper'
will be
specified in terms of 'as_lower' and 'as_upper'.
- Strongly accept the proposal
- usander@online.de
- Accept the proposal
- gmc444@yahoo.com
- xavier@halstenbach.com
- saunderscj2000@yahoo.com
- arno.wagner@acm.org
- kiniry@acm.org
- chcouder@club-internet.fr
- franck@nenie.org
- jeff.clark@sdrc.com
- peter@deakin.edu.au
- kwaxer@aha.ru
- sparker@eiffel.ie
- James McKim (by email)
12 MARCH 2001 VERSION:
to_lower
-- Convert all letters to lower case.
ensure
length_and_content:
is_equal(old as_lower)
to_upper
-- Convert all letters to upper case.
ensure
length_and_content:
is_equal(old as_upper)
The PREVIOUS version of 'to_lower' and 'to_upper', from ELKS95,
looks like this:
to_lower
-- Convert to lower case.
to_upper
-- Convert to upper case.
The difference between the previous version and the proposed new
version is that the specification has been made rigorous, and the
header comment has been made consistent with the other lower/upper
features of classes STRING and CHARACTER.
- Accept the proposal
- gmc444@yahoo.com
- arno.wagner@acm.org
- kwaxer@aha.ru
- chcouder@club-internet.fr
- saunderscj2000@yahoo.com
- sparker@eiffel.ie
- xavier@halstenbach.com
- jeff.clark@sdrc.com
- kiniry@acm.org
- ericb@gobosoft.com
- franck@nenie.org
- icm_mandel@yahoo.es
- peter@deakin.edu.au
- James McKim (by email)
21 MARCH 2001 19:30 VERSION:
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
-- terminator: the
ASCII character at address c_string+count
--
is NUL
The PREVIOUS version of 'from_c' looks like this:
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
/= Void
The differences between the previous version and the proposed new
version are that a precondition error has been corrected, and the
semantics are more completely specified. There is no known
incompatibility between the 21 MARCH 2001 19:30 VERSION and the
ISE/HACT/VE versions of 'from_c'. There is no known incompatibility
(apart from the feature name) between the 21 MARCH 2001 19:30 VERSION
and the SE feature 'from_external_copy'.
- Strongly accept the proposal
- gmc444@yahoo.com
- Accept the proposal
- peter@deakin.edu.au
- manus@eiffel.com
- chcouder@club-internet.fr
- kwaxer@aha.ru
- arno.wagner@acm.org
- ericb@gobosoft.com
- jeff.clark@sdrc.com
- sparker@eiffel.ie
- xavier@halstenbach.com
- kiniry@acm.org
- icm_mandel@yahoo.es
- Ulrich Windl (by email)
- Abstain (not happy either way)
- saunderscj2000@yahoo.com
29 MARCH 2001 VERSION
wipe_out
-- Remove all characters.
ensure
empty_string: count
= 0
The PREVIOUS (ELKS95) version of 'wipe_out' looks like this:
wipe_out
-- Remove all characters.
ensure
empty_string: count
= 0;
wiped_out: is_empty
The difference between the previous version and the proposed new version
is that one of the redundant postcondition clauses has been removed.
- Strongly accept the proposal
- kiniry@acm.org
- Accept the proposal
- saunders@wchat.on.ca
- kwaxer@aha.ru
- ericb@gobosoft.com
- xavier@halstenbach.com
- usander@online.de
- arno.wagner@acm.org
- gmc444@yahoo.com
- manus@eiffel.com
- jeff.clark@sdrc.com
- sparker@eiffel.ie
- chcouder@club-internet.fr
- berend@pobox.com
- icm_mandel@yahoo.es
If 'make' is to be kept in ELKS 2001 STRING, the next vote will be to
refine its specification.
If 'make' is to be dropped from ELKS 2001 STRING, vendors may retain
their existing (incompatible) implementations of 'make' (outside of
ELKS).
Either way, 'make_empty' and 'make_filled' remain as creation features
in
the draft ELKS 2001 STRING class.
- Strongly prefer to keep 'make'
- jeff.clark@sdrc.com
- xavier@halstenbach.com
- saunders@wchat.on.ca
- berend@pobox.com
- Emmanuel Stapf (by email)
- Ulrich Windl
- Prefer to keep 'make'
- ericb@gobosoft.com
- gmc444@yahoo.com
- arno.wagner@acm.org
- sparker@eiffel.ie
- kiniry@acm.org
- Prefer to drop 'make'
- kwaxer@aha.ru
- Don't mind (happy either way)
- peter@deakin.edu.au
- Abstain (not happy either way)
- franck@nenie.org
27 APRIL 2001 VERSION:
make (suggested_capacity: INTEGER)
-- Create empty string.
require
non_negative_suggested_capacity:
suggested_capacity >= 0
ensure
empty_string: count
= 0
The PREVIOUS (ELKS95) version of 'make' looks like this:
frozen make (n: INTEGER)
-- Allocate space for at least n characters.
require
non_negative_size:
n >= 0
ensure
empty_string: count
= 0
The difference between the previous version and the proposed new
version is that the "frozen" status has been removed, and the requirement
to allocate a specific amount of space has been removed (because it
is a
"quality-of-implementation" rather than a "correctness" issue). There
are
also (cosmetic) changes to the argument name and header comment.
If this vote passes, it will be followed by a vote to consider changing
the name of 'make' to 'make_capacity'.
- Accept the proposal
- jeff.clark@sdrc.com
- manus@eiffel.com
- sparker@eiffel.ie
- saunders@wchat.on.ca
- kwaxer@aha.ru
- xavier@halstenbach.com
- gmc444@yahoo.com
- arno.wagner@acm.org
- ericb@gobosoft.com
- berend@pobox.com
- kiniry@acm.org
- franck@nenie.org
- peter@deakin.edu.au
- Ulrich Windl (by email)
During recent discussions, there has been some argument for renaming 'make' to reflect its specialized role (due to its 'suggested_capacity' argument). The names mentioned have included 'make_empty_with_capacity', 'make_with_capacity' and 'make_capacity'.
With this poll, we will establish whether this group feels that there is a genuine need to rename 'make'. So I'm not going to phrase the proposal in terms of a specific alternative name. If it turns out that the majority think the name should be changed, we can then discuss possible names. If not, then we are saved the bother of deciding which alternative name to consider.
- Strongly accept the proposal
- franck@nenie.org
- Accept the proposal
- sparker@eiffel.ie
- peter@deakin.edu.au
- arno.wagner@acm.org
- Alexander Kogtenkov (by email)
- Reject the proposal
- saunders@wchat.on.ca
- berend@pobox.com
- jeff.clark@sdrc.com
- gmc444@yahoo.com
- manus@eiffel.com
- ericb@gobosoft.com
- kiniry@acm.org
- Ulrich Windl (by email)
- Strongly reject the proposal
- xavier@halstenbach.com
- Don't mind (happy either way)
- James McKim (by email)
In ELKS95, 'remake' looked like this:
frozen remake (n: INTEGER)
-- Allocate space for at least n characters.
require
non_negative_size:
n >= 0
ensure
empty_string: count
= 0
If 'remake' is kept in ELKS 2001, it is likely to look like this:
30 APRIL 2001 VERSION:
remake (suggested_capacity: INTEGER)
-- Remove all characters.
require
non_negative_suggested_capacity:
suggested_capacity >= 0
ensure
empty_string: count
= 0
If 'remake' is removed from ELKS 2001, there will be an additional poll
to decide whether 'make' should be publicly exported, or whether it
should only be available at creation time (with 'wipe_out' remaining
available for reinitialization).
The arguments for removing 'remake' are that it is not universally
supported, it has different semantics in VE and ISE/HACT, it duplicates
functionality available in other features of the class, and it has
hardly
ever been used.
The argument for retaining 'remake' is that, if the issues above can
be
overcome, it offers the potential for slightly greater performance
than
'make' or 'wipe_out'.
- Strongly accept the proposal
- icm_mandel@yahoo.es
- berend@pobox.com
- Accept the proposal
- sparker@eiffel.ie
- ericb@gobosoft.com
- arno.wagner@acm.org
- peter@deakin.edu.au
- jeff.clark@sdrc.com
- manus@eiffel.com
- xavier@halstenbach.com
- saunders@wchat.on.ca
- kwaxer@aha.ru
- Ulrich Windl (by email)
- James McKim (by email)
The most recent version of 'make' looks like this:
make (suggested_capacity: INTEGER)
-- Create empty string.
require
non_negative_suggested_capacity:
suggested_capacity >= 0
ensure
empty_string: count
= 0
Currently, 'make' is only available for creation. If this proposal is accepted, 'make' will also become available for reinitialization. In that case, some tweak to the header comment may be appropriate.
If this proposal is rejected, 'wipe_out' can be used for reinitialization. However, 'wipe_out' does not take a 'suggested_capacity' argument.
- Accept the proposal
- saunders@wchat.on.ca
- peter@deakin.edu.au
- sparker@eiffel.ie
- jeff.clark@sdrc.com
- berend@pobox.com
- kiniry@acm.org
- xavier@halstenbach.com
- gmc444@yahoo.com
- James McKim (by email)
- Reject the proposal
- ericb@gobosoft.com
- Don't mind (happy either way)
- franck@nenie.org
- kwaxer@aha.ru
- arno.wagner@acm.org
- Emmanuel Stapf (by email)
The PREVIOUS (ELKS95) version of 'resize' looks like this:
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
This feature is currently implemented in different ways. ISE/HACT do not change 'count', whilst SE/VE set 'count' to 'newsize' and initialize any newly-allocated character positions to '%/0/'.
- Strongly accept the proposal
- franck@nenie.org
- Accept the proposal
- saunders@wchat.on.ca
- peter@deakin.edu.au
- kwaxer@aha.ru
- arno.wagner@acm.org
- sparker@eiffel.ie
- jeff.clark@sdrc.com
- berend@pobox.com
- gmc444@yahoo.com
- James McKim (by email)
- Ulrich Windl (by email)
- Reject the proposal
- ericb@gobosoft.com
- kiniry@acm.org
- xavier@halstenbach.com
- Emmanuel Stapf (by email)
Joesph Kiniry explained that although he voted to reject the removal of 'resize', he would prefer to switch to the VE/SE semantics than to retain the ELKS95 semantics.
22 MAY 2001 VERSION
string: STRING
-- New STRING having the same characters
as 'Current'.
-- Useful when working with descendants
of STRING.
ensure
same_count: Result.count
= count
first_item: count
> 0 implies
Result.item
(1) = item (1)
recurse: count > 1
implies
Result.substring(2,
count).is_equal(
substring(2,
count).string)
same_string(other: STRING): BOOLEAN
-- Do 'current' and 'other' have
the same characters?
-- Useful when working with descendants
of STRING.
require
other_not_void:
other /= Void
ensure
definition:
Result = string.is_equal(other.string)
These features do not appear in ELKS95. It is proposed to add them so
that features of STRING can be specified in a way that is usable in
descendants of STRING.
- Accept the proposal
- saunders@wchat.on.ca
- icm_mandel@yahoo.es
- peter@deakin.edu.au
- ericb@gobosoft.com
- kiniry@acm.org
- berend@pobox.com
- franck@nenie.org
- sparker@eiffel.ie
- kwaxer@aha.ru
- arno.wagner@acm.org
- manus@eiffel.com
- xavier@halstenbach.com
- jeff.clark@sdrc.com
- gmc444@yahoo.com
26 MAY 2001 VERSION
make_from_string (s: STRING) is
-- Initialize from the character sequence
of 's'.
-- (Useful in proper descendants of
class STRING,
-- to initialize a string-like object
from a manifest string.)
require
s_not_void: s /= Void
ensure
initialized: same_string
(s)
The PREVIOUS (ELKS95) version of 'make_from_string' looks like this:
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
The difference between the previous version and the proposed new version is that the proposed new version is rigorously specified with respect to its behaviour in class STRING and also in descendants of STRING.
In ELKS 95, 'make_from_string' is both a creation feature and a reinitialization feature. This vote does not change that status. A separate vote will be held later to resolve that issue if necessary.
- Accept the proposal
- berend@pobox.com
- pgcrism@attglobal.net
- chcouder@club-internet.fr
- manus@eiffel.com
- kwaxer@aha.ru
- sparker@eiffel.ie
- icm_mandel@yahoo.es
- ericb@gobosoft.com
- saunders@wchat.on.ca
- xavier@halstenbach.com
- gmc444@yahoo.com
- arno.wagner@acm.org
- jeff.clark@sdrc.com
- franck@nenie.org
- kiniry@acm.org
- peter@deakin.edu.au
- usander@online.de
- James McKim (by email)
4 JUNE 2001 VERSION:
invariant -- from COMPARABLE
irreflexive_comparison:
not (Current < Current);
invariant
non_negative_count:
count >= 0
The PREVIOUS (ELKS95) version of the class invariant looks like this:
invariant
irreflexive_comparison:
not (Current < Current);
empty_definition:
is_empty = (count = 0);
non_negative_count:
count >= 0
The difference between the previous version and the proposed new
version is that the clause inherited from COMPARABLE is labelled as
such,
and the clause that is redundant with the postcondition of 'is_empty'
has
been removed.
- Accept the proposal
- jeff.clark@sdrc.com
- ericb@gobosoft.com
- gmc444@yahoo.com
- berend@pobox.com
- xavier@halstenbach.com
- chcouder@club-internet.fr
- saunders@wchat.on.ca
- usander@online.de
- kwaxer@aha.ru
- kiniry@acm.org
- arno.wagner@acm.org
- Don't mind (happy either way)
- manus@eiffel.com
4 JUNE 2001 VERSION
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)
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))
as_lower: like current
-- New string 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 string 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)
is_boolean: BOOLEAN
-- Does 'current' represent a BOOLEAN?
ensure
is_boolean: result
= (same_string("true")
or same_string("false"))
to_boolean: BOOLEAN
-- Boolean value;
-- "true" yields true, "false" yields
false
require
represents_a_boolean:
is_boolean
ensure
to_boolean: result
= same_string("true")
infix "+" (other: STRING): like Current
-- Create a new object which is the
concatenation of Current
-- and 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)
The difference between the version currently in the ELKS2001 draft and
the proposed new version is:
substring_index
change 'is_equal' to 'same_string'
has_substring
change 'is_equal' to 'same_string'
as_lower
change result type from STRING to "like current"
as_upper
change result type from STRING to "like current"
is_boolean
change 'is_equal' to 'same_string'
to_boolean
change 'is_equal' to 'same_string'
infix "+"
in the "final" assertion only, change 'is_equal'
to 'same_string'
The purpose of these changes is to make the features usable in
descendants of STRING.
- Accept the proposal
- jeff.clark@sdrc.com
- ericb@gobosoft.com
- gmc444@yahoo.com
- berend@pobox.com
- xavier@halstenbach.com
- chcouder@club-internet.fr
- saunders@wchat.on.ca
- usander@online.de
- kwaxer@aha.ru
- kiniry@acm.org
- arno.wagner@acm.org
- Don't mind (happy either way)
- manus@eiffel.com
Strongly accept the proposal
Accept the proposal
Reject the proposal
Strongly reject the proposal
Don't mind (happy either way)
Abstain (not happy either way)
... the voting options do not cover all possibilities. If you wish to vote for something else (e.g. to include all or none of the features) please post your preference to the list and we will take it into account when compiling the results.
Neither 'remove_head' nor 'remove_tail' is in ELKS95. They are in the current draft for ELKS 2001 STRING as follows:
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_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)))
'remove_substring' is not in ELKS95 or in the ELKS 2001 draft. Here is a candidate specification:
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))
This time, we had a number of people who posted their vote direct to the list, because the options offered in the Yahoogroups poll did not meet their needs. Here are the merged votes:
- Accept the proposal
Franck Arnaud
Simon Parker
Alexander Kogtenkov
- Want all three features
Eric Bezault
Christian Couder
Chris Saunders
Joseph Kiniry
Berend de Boer
Arno Wagner
James McKim
- Don't mind
Emmanuel Stapf
Strongly accept the proposal
Accept the proposal
Reject the proposal
Strongly reject the proposal
Don't mind (happy either way)
Abstain (not happy either way)
- Strongly accept the proposal
- peter@deakin.edu.au
- franck@nenie.org
- Accept the proposal
- gmc444@yahoo.com
- chcouder@club-internet.fr
- sparker@eiffel.ie
- ericb@gobosoft.com
- manus@eiffel.com
- kwaxer@aha.ru
- arno.wagner@acm.org
- kiniry@acm.org
- jeff.clark@sdrc.com