work in progress | array |
September 2001:
3 SEPTEMBER 2001 VERSION:
make_from_array (a: ARRAY [G])
-- Initialize from the items of `a'.
require
a_not_void: a /= Void
ensure
initialized: same_array
(a)
array: ARRAY [G]
-- New ARRAY [X] having the same items
as `Current',
-- where "X" is the result type of the
`item' query.
ensure
array_not_void: Result
/= Void
same_count: Result.count
= count
same_indexes: Result.lower
= lower
first_item: count
> 0 implies
Result.item
(lower) = item (lower)
recurse: count > 0
implies
Result.subarray
(lower + 1, upper).is_equal (
subarray (lower
+ 1, upper).array)
same_array (other: ARRAY [G]): BOOLEAN
-- Do `current' and `other' have the
same items
-- with the same indices?
require
other_not_void: other
/= Void
ensure
definition:
Result = array.is_equal (other.array)
make_from_array (a: ARRAY [G])
-- Initialize from the items of a.
-- (Useful in proper descendants of
class ARRAY,
-- to initialize an array-like object
from a manifest array.)
This feature was dropped from ELKS 2000 ARRAY because we were unable to formalise its behaviour at the time. Since then, we worked on 'make_from_string' for class STRING, and have applied the same design to this class.
These features will provide the following benefits:
(1) within proper descendants of ARRAY, 'make_from_array'
and
'array' enable initialization
of the descendant object
from ARRAY data, and extraction
of ARRAY data from
the descendan object
(2) 'same_array' and 'array' enable the rigorous specification
of 'make_from_array'
(3) 'same_array' and 'array' can be used in the assertions
of other ARRAY features, so that
those features can be
specified in a way that is also
usable in ARRAY descendants
In the list discussion, it was agreed to change the header comment of 'array' to the following:
-- New ARRAY having the same items as `Current'
...and to add the following postcondition:
result_type: -- Result type is ARRAY [like item]
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:
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.
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'.
13 NOVEMBER 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:
max_index < old lower or min_index > old upper or else
subarray (min_index.max (old lower).min (max_index + 1),
max_index.min (old upper).max(min_index - 1)).is_equal
(old subarray (min_index.max (lower).min(upper + 1),
max_index.min (upper).max(lower - 1)))
The PREVIOUS version of 'resize' looks like this:
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)).is_equal
(old subarray ((min_index.max (lower)).min(upper + 1),
(max_index.min (upper)).max(lower - 1)))
The difference between the previous version and the proposed new
version is limited to the 'stable_in_intersection' postcondition.
In the previous version, there was a bug whereby 'subarray' could
be called with invalid arguments.
In the proposed version, this bug has been fixed whilst retaining
the ability of 'resize' to work in proper descendants of class ARRAY.
28 JANUARY 2002 VERSION:
count: INTEGER
-- Number of available indices
ensure
definition: Result
= upper - lower + 1