deferred class interface COLLECTION[E]
--
-- Common abstract definition of a sequenceable collection of objects.
-- Such a collection is traversable using a simple INTEGER index from lower
-- to upper. Items can be added, changed or removed.
--
-- The SmartEiffel standard library provides four implementations of
-- COLLECTION[E]: ARRAY[E], FIXED_ARRAY[E], LINKED_LIST[E] and
-- TWO_WAY_LINKED_LIST[E]. All implementations have exactly the same
-- behavior. Switching from one implementation to another only change the
-- memory used and the execution time.
--
feature(s) from COLLECTION
-- Indexing:
lower: INTEGER
-- Minimum index.
upper: INTEGER
-- Maximum index.
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 available indices.
ensure
Result = upper - lower + 1
is_empty: BOOLEAN
-- Is collection empty ?
ensure
Result = (count = 0)
feature(s) from COLLECTION
-- Accessing:
item (i: INTEGER): E
-- Item at the corresponding index i.
require
valid_index(i)
infix "@" (i: INTEGER): E
-- Item at the corresponding index i.
require
valid_index(i)
first: like item
-- The very first item.
require
count >= 1
ensure
Result = item(lower)
last: like item
-- The last item.
require
not is_empty
ensure
Result = item(upper)
feature(s) from COLLECTION
-- Writing:
put (element: like item; i: INTEGER)
-- Make element the item at index i.
require
valid_index(i)
ensure
item(i) = 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 every item to its default value.
-- The count is not affected (see also clear).
ensure
stable_upper: upper = old upper;
stable_lower: lower = old lower;
all_default
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
index.in_range(lower,upper + 1)
ensure
item(index) = element;
count = 1 + old count;
upper = 1 + old upper
append_collection (other: COLLECTION[E])
-- Append other to Current.
require
other /= Void
ensure
count = other.count + old count
feature(s) from COLLECTION
-- Modification:
force (element: E; index: INTEGER)
-- Make element the item at index, enlarging the collection if
-- necessary (new bounds except index are initialized with
-- default values).
require
index >= lower
ensure
upper = index.max(old upper);
item(index) = element
copy (other: like Current)
-- Reinitialize by copying all the items of other.
require
same_dynamic_type(other)
ensure
is_equal(other)
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 is_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 is_empty
ensure
count = old count - 1;
upper = old upper - 1
clear
-- Discard all items in order to make it is_empty.
-- See also clear_all.
ensure
is_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.
--
-- Note: we'll have to mimic what's done in the new ELKS STRING class
-- for index_of (ie. to add an extra argument). This is in the todo
-- list ... let people switch first to ELKS 2001 at time being.
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:
is_equal (other: like Current): BOOLEAN
-- Do both collections have the same lower, upper, and
-- items?
-- The basic = is used for comparison of items.
-- See also is_equal_map.
require
other /= Void
ensure
Result implies lower = other.lower and upper = other.upper;
generating_type = other.generating_type implies Result = other.is_equal(Current)
is_equal_map (other: like Current): BOOLEAN
-- Do both collections have the same lower, upper, and
-- items?
-- Feature is_equal is used for comparison of items.
-- See also is_equal.
ensure
Result implies lower = other.lower and upper = other.upper
all_default: BOOLEAN
-- Do all items have their type's default value?
-- Note: for non Void items, the test is performed with the
-- is_default predicate.
same_items (other: COLLECTION[E]): BOOLEAN
-- Do both collections have the same items? The basic = is used
-- for comparison of items and indices are not considered (for
-- example this routine may yeld True with Current indexed in
-- range [1..2] and other indexed in range [2..3]).
require
other /= Void
ensure
Result implies count = other.count
occurrences (element: like item): INTEGER
-- Number of occurrences of element using equal for comparison.
-- Also consider fast_occurrences to choose the most appropriate.
ensure
Result >= 0
fast_occurrences (element: like item): INTEGER
-- Number of occurrences of element using basic = for comparison.
-- Also consider occurrences 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
-- Agents based features:
do_all (action: ROUTINE[ANY,TUPLE[ANY]])
-- Apply action to every item of Current.
for_all (test: PREDICATE[ANY,TUPLE[ANY]]): BOOLEAN
-- Do all items satisfy test?
exists (test: PREDICATE[ANY,TUPLE[ANY]]): BOOLEAN
-- Does at least one item satisfy test?
feature(s) from COLLECTION
-- Other features:
get_new_iterator: ITERATOR[E]
replace_all (old_value, new_value: like item)
-- Replace all occurrences 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;
occurrences(old_value) = 0
fast_replace_all (old_value, new_value: like item)
-- Replace all occurrences 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_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 (min, max: INTEGER): like Current
-- New collection consisting of items at indexes in [min..max].
-- Result has the same dynamic type as Current.
-- The lower index of the Result is the same as lower.
require
lower <= min;
max <= upper;
min <= max + 1
ensure
same_dynamic_type(Result);
Result.count = max - min + 1;
Result.lower = lower
reverse
-- Reverse the order of the elements.
ensure
count = old count
invariant
valid_bounds: lower <= upper + 1;
end of deferred COLLECTION[E]