deferred class interface ARRAYED_COLLECTION[E]
--
-- Common root for ARRAY[E] and FIXED_ARRAY[E].
--
feature(s) from COLLECTION
-- Indexing :
lower: INTEGER
-- Lower index bound.
upper: INTEGER
-- Upper index bound.
valid_index (index: INTEGER): BOOLEAN
-- True when index is valid (ie. inside actual
-- bounds of the collection).
ensure
Result = (lower <= index and then index <= upper)
feature(s) from COLLECTION
-- Counting :
count: INTEGER
-- Number of elements actually stored in the collection.
ensure
Result = upper - lower + 1
empty: BOOLEAN
-- Is collection empty?
feature(s) from COLLECTION
-- Accessing :
item (index: INTEGER): E
-- Item at position index.
require
valid_index(index)
feature(s) from COLLECTION
-- Accessing :
infix "@" (index: INTEGER): E
-- Item at position index.
require
valid_index(index)
first: like item
-- The very first item.
require
count >= 1
ensure
Result = item(lower)
last: like item
-- The last item.
require
count >= 1
ensure
Result = item(upper)
feature(s) from COLLECTION
-- Writing :
put (element: like item; index: INTEGER)
-- Put element at position index.
require
valid_index(index)
ensure
item(index) = element;
count = old count
swap (i1, i2: INTEGER)
-- Swap item at index i1 with item at index i2.
require
valid_index(i1);
valid_index(i2)
ensure
item(i1) = old item(i2);
item(i2) = old item(i1);
count = old count
set_all_with (v: like item)
-- Set all items with value v.
ensure
count = old count
set_slice_with (v: like item; lower_index, upper_index: INTEGER)
-- Set all items in range [lower_index .. upper_index] with v.
require
lower_index <= upper_index;
valid_index(lower_index);
valid_index(upper_index)
ensure
count = old count
clear_all
-- Set all items to default values.
-- The count is not affected (see also clear).
ensure
count = old count;
all_cleared
feature(s) from COLLECTION
-- Adding :
add_first (element: like item)
-- Add a new item in first position : count is increased by
-- one and all other items are shifted right.
ensure
first = element;
count = 1 + old count;
lower = old lower;
upper = 1 + old upper
add_last (element: like item)
-- Add a new item at the end : count is increased by one.
ensure
last = element;
count = 1 + old count;
lower = old lower;
upper = 1 + old upper
add (element: like item; index: INTEGER)
-- Add a new element at rank index : count is increased
-- by one and range [index .. upper] is shifted right
-- by one position.
require
lower <= index;
index <= upper + 1
ensure
item(index) = element;
count = 1 + old count;
upper = 1 + old upper
feature(s) from COLLECTION
-- Modification :
force (element: E; index: INTEGER)
-- Put element at position index. Collection is
-- resized if index is not inside current bounds.
-- New bounds are initialized with default values.
require
index >= lower
ensure
valid_index(index);
item(index) = element
from_collection (model: COLLECTION[like item])
-- Initialize the current object with the contents of model.
require
model /= Void
ensure
count = model.count
feature(s) from COLLECTION
-- Removing :
remove_first
-- Remove the first element of the collection.
require
not empty
ensure
count = old count - 1;
lower = old lower + 1 xor upper = old upper - 1
remove (index: INTEGER)
-- Remove the item at position index. Followings items
-- are shifted left by one position.
require
valid_index(index)
ensure
count = old count - 1;
upper = old upper - 1
remove_last
-- Remove the last item.
require
not empty
ensure
count = old count - 1;
upper = old upper - 1
clear
-- Discard all items in order to make it empty.
-- See also clear_all.
ensure
empty
feature(s) from COLLECTION
-- Looking and Searching :
has (x: like item): BOOLEAN
-- Look for x using equal for comparison.
-- Also consider fast_has to choose the most appropriate.
fast_has (x: like item): BOOLEAN
-- Look for x using basic = for comparison.
-- Also consider has to choose the most appropriate.
index_of (element: like item): INTEGER
-- Give the index of the first occurrence of element using
-- is_equal for comparison.
-- Answer upper + 1 when element is not inside.
-- Also consider fast_index_of to choose the most appropriate.
ensure
lower <= Result;
Result <= upper + 1;
Result <= upper implies equal(element,item(Result))
fast_index_of (element: like item): INTEGER
-- Give the index of the first occurrence of element using
-- basic = for comparison.
-- Answer upper + 1 when element is not inside.
-- Also consider index_of to choose the most appropriate.
ensure
lower <= Result;
Result <= upper + 1;
Result <= upper implies element = item(Result)
feature(s) from COLLECTION
-- Looking and comparison :
all_cleared: BOOLEAN
-- Are all items set to the default value ?
nb_occurrences (element: like item): INTEGER
-- Number of occurrences of element using equal for comparison.
-- Also consider fast_nb_occurences to choose the most appropriate.
ensure
Result >= 0
fast_nb_occurrences (element: like item): INTEGER
-- Number of occurrences of element using basic = for comparison.
-- Also consider nb_occurences to choose the most appropriate.
ensure
Result >= 0
feature(s) from COLLECTION
-- Printing :
fill_tagged_out_memory
-- Append a viewable information in tagged_out_memory in
-- order to affect the behavior of out, tagged_out, etc.
feature(s) from COLLECTION
-- Other Features :
replace_all (old_value, new_value: like item)
-- Replace all occurences of the element old_value by new_value
-- using equal for comparison.
-- See also fast_replace_all to choose the apropriate one.
ensure
count = old count;
nb_occurrences(old_value) = 0
fast_replace_all (old_value, new_value: like item)
-- Replace all occurences of the element old_value by new_value
-- using operator = for comparison.
-- See also replace_all to choose the apropriate one.
ensure
count = old count;
fast_nb_occurrences(old_value) = 0
move (lower_index, upper_index, distance: INTEGER)
-- Move range lower_index .. upper_index by distance
-- positions. Negative distance moves towards lower indices.
-- Free places get default values.
require
lower_index <= upper_index;
valid_index(lower_index);
valid_index(lower_index + distance);
valid_index(upper_index);
valid_index(upper_index + distance)
ensure
count = old count
slice (low, up: INTEGER): like Current
-- Create a new collection initialized with elements of
-- range low..up. Result has the same dynamic type
-- as Current collection. The lower index of the new
-- collection is the same as lower of Current.
require
valid_index(low);
valid_index(up);
low <= up
ensure
same_type(Result);
Result.count = up - low + 1;
Result.lower = lower
feature(s) from ARRAYED_COLLECTION
capacity: INTEGER
-- Internal storage capacity in number of item.
feature(s) from ARRAYED_COLLECTION
sub_array (low, up: INTEGER): like Current
require
valid_index(low);
valid_index(up);
low <= up
ensure
same_type(Result);
Result.count = up - low + 1;
Result.lower = low or Result.lower = 0
feature(s) from ARRAYED_COLLECTION
-- Interfacing with C :
to_external: POINTER
-- Gives C access into the internal storage of the ARRAY.
-- Result is pointing the element at index lower.
--
-- NOTE: do not free/realloc the Result. Resizing of the array
-- can makes this pointer invalid.
require
not empty
ensure
Result.is_not_null
invariant
capacity >= upper - lower + 1;
capacity > 0 implies storage.is_not_null;
end of deferred ARRAYED_COLLECTION[E]