Class ARRAY
Draft proposal
indexing
description: "Resizable sequences of values, all of the same type or of a %
%conforming one, accessible through integer indices in a %
%contiguous interval"
class interface
ARRAY [G]
creation
make (minindex, maxindex: INTEGER)
-- Allocate array; set index interval to
-- minindex .. maxindex; set all values to default.
-- (Make array empty if minindex > maxindex.)
require
valid_indices: (minindex <= maxindex) or (maxindex = minindex - 1)
ensure
lower_set: lower = minindex
upper_set: upper = maxindex
-- array_set: for i in minindex..maxindex, item(i) = default item
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.)
require
valid_array: a /= Void
feature -- Initialization
make (minindex, maxindex: INTEGER)
-- Set index interval to minindex .. maxindex;
-- reallocate if necessary; set all values to default.
-- (Make array empty if minindex > maxindex.)
require
valid_indices: (minindex <= maxindex) or (maxindex = minindex - 1)
ensure
lower_set: lower = minindex
upper_set: upper = maxindex
-- array_set: for i in minindex..maxindex, item(i) = default item
make_from_array (a: ARRAY [G])
-- Initialize from the items of a; reallocate if
-- necessary. (Useful in proper descendants of
-- class ARRAY, to initialize an array-like object
-- from a manifest array.)
require
valid_array: a /= Void
feature -- Access
first: like item
-- First element
require
not_empty: not is_empty
ensure
definition: Result = item (lower)
has (v: like item): BOOLEAN
-- Does Current contain v?
-- Use equal as comparison operator.
ensure
definition: Result = valid_index(index_of(c));
index_of (v: like item): INTEGER
-- Index of first occurrence of v
-- Use equal as comparison operator.
-- Upper + 1 if not found
ensure
not_found: (Result = upper + 1) = not has(v);
found: has(v) implies equal(v,item(Result));
infix "@", item (i: INTEGER): G
-- Entry at index i
require
good_key: valid_index (i)
last: like item
-- Last element
require
not_empty: not is_empty
ensure
definition: Result = item (upper)
reverse_index_of (v: like item): INTEGER
-- Index of last occurrence of v?
-- Use equal as comparison operator.
-- Lower - 1 if not found
ensure
not_found: (Result = upper + 1) = not has(v);
found: has(v) implies equal(v,item(Result));
feature -- Measurement
capacity: INTEGER
-- Number of elements that Current can currently contain in the internal storage area.
-- Automatically updated when resizing is needed. Useful for fine tuning.
count: INTEGER
-- Number of valid indices
ensure
definition: Result = upper - lower + 1;
lower: INTEGER
-- Minimum valid index
occurrences (v: like item): INTEGER
-- Number of times v appears in Current.
-- Use equal as comparison operator.
ensure
non_negative_occurrences: Result >= 0
upper: INTEGER
-- Maximum valid index
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Do both arrays have same lower, upper and
-- items (compared with is_equal)?
-- (Redefined from GENERAL.)
feature -- Status report
is_empty: BOOLEAN
-- Is array empty?
ensure
definition: Result = (count = 0)
valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the array?
ensure
definition: lower <= i and i <= upper
feature -- Element change
add (v: like item; i: INTEGER)
-- Insert v at index i, shifting elements between ranks i and upper rightwards.
require
valid_insertion_index: lower <= i and i <= upper + 1
ensure
inserted: item (i) = v;
same_lower: lower = old lower;
higher_upper: upper = old upper + 1
add_first (v: like item)
-- Insert v at index lower, shifting all elements rightwards.
ensure
inserted: first = v;
same_lower: lower = old lower;
higher_upper: upper = old upper + 1
add_last (v: like item)
-- Append v at end.
ensure
inserted: last = v;
same_lower: lower = old lower;
higher_upper: upper = old upper + 1
force (v: like item; i: INTEGER)
-- Assign v to i-th entry.
-- Always applicable: resize the array if i falls out of
-- currently defined bounds; preserve existing items.
-- New entries if any are initialized to default value.
ensure
put: item (i) = v;
higher_count: count >= old count
put (v: like item; i: INTEGER)
-- Assign v to i-th entry.
require
good_index: valid_index (i)
ensure
put: item (i) = v
feature -- Removal
remove (i: INTEGER)
-- Remove element at index i and shift elements between ranks i+1 and upper leftwards.
require
good_index: valid_index (i)
ensure
same_lower: lower = old lower;
smaller_upper: upper = old upper - 1
remove_first
-- Remove first element and shift all elements leftwards.
require
not_is_empty: not is_empty
ensure
same_lower: lower = old lower;
smaller_upper: upper = old upper - 1
remove_last
-- Remove last element.
require
not_is_empty: not is_empty
ensure
same_lower: lower = old lower;
smaller_upper: upper = old upper - 1
wipe_out
-- Remove all elements.
ensure
is_empty: is_empty
same_capacity: capacity = old capacity
same_lower: lower = old lower
feature -- Resizing
resize (minindex, maxindex: INTEGER)
-- Rearrange array so that it can accommodate
-- indices down to minindex and up to maxindex.
-- Do not lose any previously entered item in the
-- intersection between [old lower .. old upper] and
-- [minindex .. maxindex].
-- New positions are initialized to their default value.
require
valid_indices: (minindex <= maxindex) or (maxindex = minindex - 1)
ensure
lower_set: lower = minindex
upper_set: upper = maxindex
feature -- Conversion
to_external: POINTER
-- Address of the storage area containing the actual sequence of elements,
-- to be passed to some external (non-Eiffel) routine.
-- Keep in mind that this storage area is subject to garbage collection.
feature -- Duplication
copy (other: like Current)
-- Reinitialize by copying all the items of other.
-- Shallow copy: if the elements are references, only the references
-- are copied, not the object they point to.
-- (Redefined from GENERAL.)
ensure
same_lower: lower = other.lower;
same_upper: upper = other.upper;
-- same_content: For every i in lower..upper,
-- item (i) = other.item (i)
feature -- Indexing
reindex (new_lower: INTEGER)
-- Change bounds according to new_lower, keeping same size and contents.
ensure
reindexed_lower: lower = new_lower;
same_contents: count = old count;
feature -- Optimization
adjust_capacity (n: INTEGER)
-- Rearrange array so that it can accommodate
-- at least n elements.
-- Do not loose any previously entered element.
require
no_item_lost: n >= count
ensure
enough_capacity: capacity >= n
invariant
consistent_count: count = upper - lower + 1;
non_negative_count: count >= 0;
good_capacity: capacity >= count
end
Last Updated: 01 September 1999