The following proposals were discussed earlier this month. There was some
agreement and no dissent, so I'm putting them to a vote.
You should soon receive an automatically-generated message from the
YahooGroups polling system, inviting you to vote on the following
two proposals.
Voting is open to all NICE members. The YahooGroups polls will run for
three days. If you cannot vote within that time, or have problems with
the YahooGroups polling system, feel free to post your vote to this list.
The first proposal is to make features of class CHARACTER safe in
descendants.
Proposal for class CHARACTER: Refine the specification of
'as_lower' and 'as_upper' to the 25 SEPTEMBER 2001 version.
25 SEPTEMBER 2001 VERSION
as_lower: like Current
-- Lower case equivalent
ensure
non_void_result:
Result /= Void
converted:
("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(item)
implies Result.item = ("abcdefghijklmnopqrstuvwxyz").item(
("ABCDEFGHIJKLMNOPQRSTUVWXYZ").index_of(item, 1))
unchanged:
not ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(item)
implies Result = Current
as_upper: like Current
-- Upper case equivalent
ensure
non_void_result:
Result /= Void
converted:
("abcdefghijklmnopqrstuvwxyz").has(item)
implies Result.item = ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").item(
("abcdefghijklmnopqrstuvwxyz").index_of(item, 1))
unchanged:
not ("abcdefghijklmnopqrstuvwxyz").has(item)
implies Result = Current
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 second proposal is to make features of class ARRAY safe in
descendants.
Proposal for class ARRAY: Refine the specification of
'resize', 'force', 'is_equal' and 'subarray' to the
25 SEPTEMBER 2001 version. Add a clause to the end-of-class
comments according to the 25 SEPTEMBER 2001 version.
25 SEPTEMBER 2001 VERSION
resize (min_index, max_index: INTEGER)
-- Resize to bounds `min_index' and `max_index'.
-- Do not lose any item whose index is in both
-- `lower..upper' and `min_index..max_index'.
require
valid_bounds: min_index <= max_index + 1
ensure
new_lower: lower = min_index
new_upper: upper = max_index
default_if_too_small:
min_index < old lower implies subarray
(min_index, max_index.min (old lower - 1)).all_default
default_if_too_large:
max_index > old upper implies subarray
(min_index.max (old upper + 1), max_index).all_default
stable_in_intersection:
stable_in_intersection:
subarray ((min_index.max (old lower)).min(old upper + 1),
(max_index.min (old upper)).max(old lower - 1)).is_equal
(old subarray ((min_index.max (lower)).min(upper + 1),
(max_index.min (upper)).max(lower - 1)))
force (v: like item; i: INTEGER)
-- Make `v' the item at index `i', enlarging the
-- array if necessary.
ensure
new_lower: lower = i.min (old lower)
new_upper: upper = i.max (old upper)
new_item: item (i) = v
new_low_items:
i < old lower implies
subarray (i + 1, old lower - 1).all_default
new_high_items:
i > old upper implies
subarray (old upper + 1, i - 1).all_default
between_lower_and_i:
subarray (old lower, ((i-1).max (old lower-1))
.min (old upper)).is_equal
(old subarray (lower, ((i-1).max (lower-1)).min (upper)))
between_i_and_upper:
subarray (((i+1).min (old upper+1))
.max (old lower), old upper).is_equal
(old subarray (((i+1).min (upper+1)).max (lower), upper))
is_equal (other: like Current): BOOLEAN
-- Do both arrays have the same `lower', `upper', and items?
-- (Redefined from GENERAL.)
require -- from GENERAL
other_not_void: other /= Void
ensure -- from GENERAL
consistent: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_equal (Current)
ensure then
definition: Result = (same_type (other) and then
same_array (other))
subarray (min, max: INTEGER): like current
-- New object consisting of items at indexes
-- in `min .. max'
require
min_large_enough: lower <= min
max_small_enough: max <= upper
valid_bounds: min <= max + 1
ensure
subarray_not_void: Result /= Void
lower_set: Result.lower = min
upper_set: Result.upper = max
items_set:
Result.count > 0 implies
(Result.item (max) = item (max) and
Result.subarray (min, max - 1).is_equal
(subarray (min, max - 1)))
-- The correctness of this specification is based on the following
-- assumptions:
--
-- 1. No feature of ARRAY calls a command on any of its arguments.
--
-- 2. No query of ARRAY changes the value of any basic specifier.
--
-- 3. No feature of ARRAY shares internal structures in any way that
-- could lead to behaviour not deducible from this
-- specification.
--
-- 4. The phrase "new ARRAY" in a header comment means a
-- newly-created ARRAY 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'.
--
-- 6. Every type has a single default value as returned by feature
-- 'default' in class GENERAL.
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 rest of this message shows the previous versions and summarises the
reasons for the proposed changes.
In class CHARACTER, the PREVIOUS version of 'as_lower' and 'as_upper'
looks like this:
as_lower: CHARACTER
-- Lower case equivalent
ensure
converted:
("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(Current)
implies Result = ("abcdefghijklmnopqrstuvwxyz").item(
("ABCDEFGHIJKLMNOPQRSTUVWXYZ").index_of(Current, 1))
unchanged:
not ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").has(Current)
implies Result = Current
as_upper: CHARACTER
-- Upper case equivalent
ensure
converted:
("abcdefghijklmnopqrstuvwxyz").has(Current)
implies Result = ("ABCDEFGHIJKLMNOPQRSTUVWXYZ").item(
("abcdefghijklmnopqrstuvwxyz").index_of(Current, 1))
unchanged:
not ("abcdefghijklmnopqrstuvwxyz").has(Current)
implies Result = Current
The differences between the previous version and the proposed new
version are that:
- The result type is changed from "CHARACTER" to
"like Current"
- "Result.item" is used instead of "Result", and
"item" is used instead of "Current", in several
places
- A new postcondition asserts that the result is
not void
The purpose of these changes is to make these features correct in proper
descendants of CHARACTER (where 'Current' is not a CHARACTER and might
not be expanded).
In class ARRAY, there are five proposed changes. Here are the previous
versions and the proposed changes...
1. 'resize': change postcondition
---------------------------------
In the last postcondition, change 'same_items' to 'is_equal'.
ELKS 2000 version:
resize (min_index, max_index: INTEGER)
-- Resize to bounds `min_index' and `max_index'.
-- Do not lose any item whose index is in both
-- `lower..upper' and `min_index..max_index'.
require
valid_bounds: min_index <= max_index + 1
ensure
new_lower: lower = min_index
new_upper: upper = max_index
default_if_too_small:
min_index < old lower implies subarray
(min_index, max_index.min (old lower - 1)).all_default
default_if_too_large:
max_index > old upper implies subarray
(min_index.max (old upper + 1), max_index).all_default
stable_in_intersection:
subarray ((min_index.max (old lower)).min(old upper + 1),
(max_index.min (old upper)).max(old lower - 1)).same_items
(old subarray ((min_index.max (lower)).min(upper + 1),
(max_index.min (upper)).max(lower - 1)))
Suggested change:
stable_in_intersection:
subarray ((min_index.max (old lower)).min(old upper + 1),
(max_index.min (old upper)).max(old lower - 1)).is_equal
(old subarray ((min_index.max (lower)).min(upper + 1),
(max_index.min (upper)).max(lower - 1)))
Reason: If a descendant adds new basic specifiers, and redefines
'is_equal' to take those new basic specifiers into account, the
postcondition of 'resize' will automatically check that those new basic
specifiers are maintained across a 'resize' operation.
2. 'force': change postcondition
--------------------------------
In two postconditions, change 'same_items' to 'is_equal'.
ELKS 2000 version:
force (v: like item; i: INTEGER)
-- Make `v' the item at index `i', enlarging the
-- array if necessary.
ensure
new_lower: lower = i.min (old lower)
new_upper: upper = i.max (old upper)
new_item: item (i) = v
new_low_items:
i < old lower implies
subarray (i + 1, old lower - 1).all_default
new_high_items:
i > old upper implies
subarray (old upper + 1, i - 1).all_default
between_lower_and_i:
subarray (old lower, ((i-1).max (old lower-1))
.min (old upper)).same_items
(old subarray (lower, ((i-1).max (lower-1)).min (upper)))
between_i_and_upper:
subarray (((i+1).min (old upper+1))
.max (old lower), old upper).same_items
(old subarray (((i+1).min (upper+1)).max (lower), upper))
Suggested change:
between_lower_and_i:
subarray (old lower, ((i-1).max (old lower-1))
.min (old upper)).is_equal
(old subarray (lower, ((i-1).max (lower-1)).min (upper)))
between_i_and_upper:
subarray (((i+1).min (old upper+1))
.max (old lower), old upper).is_equal
(old subarray (((i+1).min (upper+1)).max (lower), upper))
Reason for change: same as for 'resize'.
3. 'is_equal': change postcondition
-----------------------------------
Simplify the last postcondition by using 'same_array' instead of
'same_items' plus the test on 'lower'.
ELKS 2000 version:
is_equal (other: like Current): BOOLEAN
-- Do both arrays have the same `lower', `upper', and items?
-- (Redefined from GENERAL.)
require -- from GENERAL
other_not_void: other /= Void
ensure -- from GENERAL
consistent: standard_is_equal (other) implies Result
same_type: Result implies same_type (other)
symmetric: Result implies other.is_equal (Current)
ensure then
definition: Result = (same_type (other) and then
(lower = other.lower) and then same_items (other))
Suggested change:
ensure then
definition: Result = (same_type (other) and then
same_array (other))
Reason for change: The use of 'same_array' does not change the semantics,
but leads to a more compact (and hopefully more readable) postcondition.
4. 'subarray': change result type and header comment
----------------------------------------------------
Change the result type from "ARRAY [G]" to "like current". Change the
header comment from "New array..." to "New object...".
ELKS 2000 version:
subarray (min, max: INTEGER): ARRAY [G]
-- New array consisting of items at indexes
-- in `min .. max'
require
min_large_enough: lower <= min
max_small_enough: max <= upper
valid_bounds: min <= max + 1
ensure
subarray_not_void: Result /= Void
lower_set: Result.lower = min
upper_set: Result.upper = max
items_set:
Result.count > 0 implies
(Result.item (max) = item (max) and
Result.subarray (min, max - 1).is_equal
(subarray (min, max - 1)))
Suggested change:
subarray (min, max: INTEGER): like current
-- New object consisting of items at indexes
-- in `min .. max'
Reason for change: The revised signature makes this feature more likely
to be useful in descendants. It is consistent with the behaviour
exhibited by ELKS 2001 'substring' in descendants of STRING.
5. Add a clause to the end-of-class comments
--------------------------------------------
Add a new item, numbered "5", to the end-of-class comments. Renumber the
existing item "5" to item "6".
-- The correctness of this specification is based on the following
-- assumptions:
--
-- 1. No feature of ARRAY calls a command on any of its arguments.
--
-- 2. No query of ARRAY changes the value of any basic specifier.
--
-- 3. No feature of ARRAY shares internal structures in any way that
-- could lead to behaviour not deducible from this
-- specification.
--
-- 4. The phrase "new ARRAY" in a header comment means a
-- newly-created ARRAY to which there is no reference other than
-- from 'result'.
--
-- 5. Every type has a single default value as returned by feature
-- 'default' in class GENERAL.
Suggested change:
-- 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'.
--
-- 6. Every type has a single default value as returned by feature
-- 'default' in class GENERAL.
Reasons for change: This parallels the ELKS 2001 STRING end-of-class
comments, and clarifies the meaning of the header comment of 'subarray'.
--
Roger Browne -
roger@... - Everything Eiffel
19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428
Send Email