Class ARRAY
Jim McKim's Revamped TOOLS USA ARRAY specification
OK, here is the revamped ARRAY spec based on the work of the TOOLS USA
group. Bertrand had a crack at this and did most of the cleaning up of
the format. He also cleaned up a number of comments and tag names. I
think he's done a good job with that, but let's hear from you if
you think differently.
One thing that might be controversial is that he changed the name of
`all_cleared' to `all_defeult'. This surprised me as ISE's current
name for the feature is the former. I think the SE people said they
also have `all_cleared'. Either is fine with me. I've left the new
name in this version so you can get a feel for it.
Bertrand started a `revision' indexing clause at the bottom, so I've
just added to that. Take a look down there for more details. I haven't
(yet) published Bertrand's revision as this one pretty well contains
it, but will gladly do so if asked. Once again, Bertrand's help does
not imply support for the proposal. I'm sure he'll speak to that when
he gets back from his latest trip.
I am very bad at spotting parenthesis problems by hand, so I am sure
there are more in here. I'll try to compile a version early next week.
I have not added `adjust' or `adjust_capacity' as yet, as I'm still
not quite sure just what we want it/them to do. As you know, that
discussion continues. I do expect that some variation will make the
final cut.
Enjoy,
-- Jim
indexing
description:"%[
Sequences of values ("items"), all of the same type
or of a conforming one, accessible through integer
indices in a contiguous interval
%]"
Basic_specifiers: lower, upper, item
Auxiliary_specifiers_1: is_equal, valid_index, subarray, all_default
Auxiliary_specifiers_2: has
more_indexing: "at end"
class interface
ARRAY [G]
create
make
feature -- Initialization
make (min_index, max_index: INTEGER)
-- Allocate array to hold values for indexes in
-- `min_index' .. `max_index'.
-- Set all values to default.
require
valid_bounds: min_index <= max_index + 1
ensure
lower_set: lower = min_index
upper_set: upper = max_index
items_set: all_default
make_from_array (a: ARRAY [G])
-- Initialize from values of `a'.
-- (Useful in descendants, to initialize from
-- e.g. manifest arrays.)
-- Note: representation may be shared; to avoid sharing,
-- use as `make_from_array (clone (a))'
require
original_not_void: a /= Void
ensure
same_as_original: is_equal (a)
feature -- Access
first: like item
-- Item at lowest index
require
not_empty: lower <= upper
ensure
definition: Result = item (lower)
has (v: like item): BOOLEAN
-- Is at least one of the items equal to `v'?
ensure
empty_implies_false: (upper < lower) implies not Result
upper_implies_true:
(lower <= upper and item (upper) = v)
implies Result
recurse:
(lower <= upper and item (upper) /= v) implies
(Result = subarray (lower, upper - 1).has (v))
index_of (v: like item): INTEGER
-- Index of first occurrence of `v' if any;
-- `upper' + 1 if no such occurrence.
ensure
valid_range: lower <= Result and Result <= upper + 1
not_found: not has (v) = (Result = upper + 1)
found:
has (v) = (Result <= upper and then
item (Result) = v) and then
not subarray (lower, Result - 1).has (v))
infix "@"(i: INTEGER): G
-- Item at index `i'.
require
valid_index: valid_index (i)
ensure
definition: Result = item (i)
item (i: INTEGER): G
-- Item at index `i'
-- Basic specifier
require
valid_index: valid_index (i)
last: INTEGER
-- Item at highest index
require
not_empty: lower <= upper
ensure
definition: Result = item (upper)
reverse_index_of (v: like item): INTEGER
-- Index of last occurrence of `v';
-- `lower' - 1 if no such occurrence.
ensure
valid_range: Result >= lower - 1 and Result <= upper
not_found: not has (v) = (Result = lower - 1)
found: has (v) =
(Result >= lower and then
item (Result) = v and
not subarray (Result + 1, upper).has (v))
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
lower_set: Result.lower = 1
upper_set: Result.upper = max - min + 1
items_set:
min <= max implies
(Result.item (max - min + 1) = item (max) and
Result.subarray (1, max - min).is_equal
(subarray (min, max - 1)))
feature -- Measurement
capacity: INTEGER
-- Size as allocated by the implementation
ensure
large_enough: Result >= upper - lower + 1 -- nondeterministic
count: INTEGER
-- Number of available indices
ensure
consistent_with_bounds: Result = upper - lower + 1
lower: INTEGER
-- Minimum index
-- Basic specifier
occurrences (v: like item): INTEGER
-- Number of times `v' appears in Current
ensure
zero_if_empty: upper < lower implies Result = 0
simple_recurse:
(lower <= upper and item (upper) /= v) implies
Result = subarray (lower, upper - 1).occurrences (v)
recurse_and_add:
(lower <= upper and item (upper) = v) implies
Result = 1 + subarray (lower, upper - 1).occurrences (v)
upper: INTEGER
-- Maximum index
-- Basic specifier
feature -- Comparison
all_default: BOOLEAN
-- Do all items have their type's default value?
ensure
true_if_empty: upper < lower implies Result
false_if_upper_not_default:
(lower <= upper and then
item (upper) /= Void and then
item (upper) /= item (upper).default)
implies not Result
recurse:
(lower <= upper and then
(item (upper) = Void or else
item (upper) = item (upper).default)) implies
Result = subarray (lower, upper - 1).all_default
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 =
((lower = other.lower) and then
(upper = other.upper) and then
(lower > upper or else
(item (upper) = other.item (upper) and
subarray (lower, upper - 1).is_equal
(other.subarray (lower, upper - 1)))))
feature -- Status report
is_empty: BOOLEAN
-- Does array have no valid index?
ensure
definition: Result = (upper < lower)
valid_index (i: INTEGER): BOOLEAN
-- Is `i' within bounds?
ensure
definition: Result = ((lower <= i) and (i <= upper))
feature -- Element change
insert (v: like item ; i: INTEGER)
-- Insert `v' at index `i', shifting to the right
-- any items previously at `i' or higher.
require
valid_insertion_index: lower <= i and i <= upper + 1
ensure
stable_lower: lower = old lower
new_upper: upper = old upper + 1
new_item: item (i) = v
stable_items:
subarray (lower, i - 1).is_equal
(old subarray (lower, i - 1))
shifted_items:
subarray (i + 1, upper).is_equal
(old subarray (i, upper))
insert_first (v: like item)
-- Insert `v' at index `lower', shifting items to the right.
ensure
stable_lower: lower = old lower
new_upper: upper = old upper + 1
new_item: item (lower) = v
shifted_items:
subarray (lower + 1, upper).is_equal
(old subarray (lower, upper))
insert_last (v: like item)
-- Append `v' at end.
ensure
stable_lower: lower = old lower
new_upper: upper = old upper + 1
new_item: item (upper) = v
stable_items:
subarray (lower, upper - 1).is_equal
(old subarray (lower, upper))
force (v: like item; i: INTEGER)
-- Make `v' the item at index `i'.
-- Always applicable: resize the array, preserving existing
-- items, if `i' falls out of current bounds.
ensure
new_item: item (i) = v
new_lower: lower = i.min (old lower)
new_upper: upper = i.max (old upper)
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
not_in_between:
not old valid_index (i) implies
subarray (old lower, old upper).is_equal
(old subarray (lower, upper))
in_between:
old valid_index (i) implies
(subarray (old lower, i - 1).is_equal
(old subarray (lower, i - 1)) and
subarray (i + 1, old upper).is_equal
(old subarray (i + 1, upper)))
put (v: like item; i: INTEGER)
-- Replace `i'-th entry, if in index interval, by `v'.
require
valid_index: valid_index (i)
ensure
stable_lower: lower = old lower
stable_upper: upper = old upper
new_item: item (i) = v
stable_before_i:
subarray (lower, i - 1).is_equal
(old subarray (lower, i - 1))
stable_after_i:
subarray (i + 1, upper).is_equal
(old subarray (i + 1, upper))
feature -- Removal
remove (i: INTEGER)
-- Remove item at index `i'; shift to the left any
-- items at higher indexes.
require
valid_index: valid_index (i)
ensure
stable_lower: lower = old lower
new_upper: upper = old upper - 1
stable_items:
subarray (lower, i - 1).is_equal
(old subarray (lower, i - 1))
shifted_items:
subarray (i, upper).is_equal
(old subarray (i + 1, upper))
remove_first
-- Remove the first item and shift left.
require
not_empty: lower <= upper
ensure
stable_lower: lower = old lower
new_upper: upper = old upper - 1
shifted_items:
subarray (lower, upper).is_equal
(old subarray (lower + 1, upper))
remove_last
-- Remove last item.
require
not_empty: lower <= upper
ensure
stable_lower: lower = old lower
new_upper: upper = old upper - 1
stable_items:
subarray (lower, upper).is_equal
(old subarray (lower, upper - 1))
feature -- Resizing
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:
(min_index.max (old lower) <=
max_index.min (old upper)
implies
subarray (min_index.max (old lower),
max_index.min (old upper)).is_equal
(old subarray (min_index.max (lower),
max_index.min (upper)))
feature -- Conversion
to_external: POINTER
-- Address of actual sequence of values,
-- for passing to external (non-Eiffel) routines.
feature -- Duplication
copy (other: like Current)
-- Reinitialize by copying all the items of `other'.
-- (Also used by `clone'.)
-- (Redefined from GENERAL.)
require --from GENERAL
other_not_void: other /= Void
type_identity: same_type (other)
ensure -- from GENERAL
is_equal: is_equal (other)
invariant
consistent_size: count = upper - lower + 1
nonnegative_count: count >= 0
valid_bounds: lower <= upper + 1
valid_capacity: capacity >= count
indexing
revision: "13 August 1999", "TOOLS USA working group", "%[Based on a new
version proposed by Dominique Colnet, Emmanuel Stapf,
and Olivier Zendra.
%]"
revision: "18 August 1999", "Bertrand Meyer",
Changed cosmetics only
(indentation and that kind of thing)
Put specifier lists in indexing clause
Changed some tag names and comments
Replaced `all_cleared' by `all_default'
%]"
revision: "20 August 1999", "James McKim", "%[
A few more cosmetic changes.
Corrected errors involving `upper' vs `item (upper)'
in `has' and `occurrences'.
Changed `large_enough' clause in `capacity' back to
the first version.
Corrected parenthesis error, and changed one use of
`implies' to `or else' in the postcondition of
`is_equal'. (Per Patrick Doyle)
Corrected parentheses problems in the
"default_if_too_small" clause of "resize"
Gave up on some indenting to keep line wraps at a
minimum.
Corrected a parenthesis problem in the `found' clause
of `reverse_index_of'.
Added checks to the `found' clauses of both
'index' routines. (Per Alexander Kogtenkov).
Changed name of "addxxx" routines to "insertxxx". (Per
numerous people.)
Used `valid_index' to slightly shorten the
`in_between' and _`not_in_between' clauses in the
postcondition of `force'. (Per Bertrand Meyer).
%]"
end
*------------------------------------------------------------------------------*
Jim McKim