class interface FIXED_ARRAY2[E]
--
-- Resizable two dimensional array.
-- Unlike ARRAY2, the lower1 bound and the lower2 bound are
-- frozen to 0. Thus, one can expect better performances.
--
creation
make (new_count1, new_count2: INTEGER)
-- Create or reset Current with new dimensions.
-- All elements are set to the default value of type E.
require
new_count1 > 0;
new_count2 > 0
ensure
count1 = new_count1;
count2 = new_count2;
all_cleared
copy (other: like Current)
require
other_not_void: other /= Void
ensure
is_equal: is_equal(other)
from_collection2 (model: COLLECTION2[like item])
-- Uses model to initialize Current.
require
model /= Void
ensure
count1 = model.count1;
count2 = model.count2
from_collection (model: COLLECTION2[like item])
-- Uses the model to update Current.
from_model (model: COLLECTION[COLLECTION[E]])
-- The model is used to fill line by line Current.
-- Assume all sub-collections of model have the same
-- number of lines.
require
model /= Void
ensure
count1 = model.count;
count2 > 0 implies count2 = model.first.count
feature(s) from COLLECTION2
-- Indexing :
lower1: INTEGER
-- Lower index bounds.
feature(s) from COLLECTION2
-- Indexing :
lower2: INTEGER
-- Lower index bounds.
line_minimum: INTEGER
-- Equivalent of lower1.
column_minimum: INTEGER
-- Equivalent of lower2.
upper1: INTEGER
-- Total number of elements.
upper2: INTEGER
-- Total number of elements.
line_maximum: INTEGER
-- Equivalent of upper1.
column_maximum: INTEGER
-- Equivalent of upper2.
feature(s) from COLLECTION2
-- Reading :
item (line, column: INTEGER): E
require
valid_index(line,column)
feature(s) from COLLECTION2
-- Writing :
put (x: like item; line, column: INTEGER)
require
valid_index(line,column)
ensure
item(line,column) = x
force (element: like item; line, column: INTEGER)
-- Put element at position (line,column). Collection is
-- resized first when (line,column) is not inside current
-- bounds. New bounds are initialized with default values.
require
line >= 0;
column >= 0
ensure
item(line,column) = element;
count >= old count
feature(s) from COLLECTION2
-- Index validity :
valid_line (line: INTEGER): BOOLEAN
ensure
Result = (lower1 <= line and line <= upper1)
feature(s) from COLLECTION2
-- Index validity :
valid_index1 (line: INTEGER): BOOLEAN
ensure
Result = (lower1 <= line and line <= upper1)
valid_column (column: INTEGER): BOOLEAN
ensure
Result = (lower2 <= column and column <= upper2)
valid_index2 (column: INTEGER): BOOLEAN
ensure
Result = (lower2 <= column and column <= upper2)
valid_index (line, column: INTEGER): BOOLEAN
ensure
Result = (valid_line(line) and valid_index2(column))
feature(s) from COLLECTION2
-- Counting :
count1: INTEGER
-- Total number of elements.
line_count: INTEGER
-- Equivalent of count1.
count2: INTEGER
-- Total number of elements.
column_count: INTEGER
count: INTEGER
-- Total number of elements.
feature(s) from COLLECTION2
swap (line1, column1, line2, column2: INTEGER)
-- Swap the element at index (line1,column1) with the
-- the element at index (line2,column2).
require
valid_index(line1,column1);
valid_index(line2,column2)
ensure
item(line1,column1) = old item(line2,column2);
item(line2,column2) = old item(line1,column1);
count = old count
set_all_with (x: E)
-- All element are set with the value x.
ensure
count = old count;
count = old count
clear_all
-- Set all items to default values.
ensure
count = old count
feature(s) from COLLECTION2
-- Creating or initializing :
from_collection2 (model: COLLECTION2[like item])
-- Uses model to initialize Current.
require
model /= Void
ensure
count1 = model.count1;
count2 = model.count2
from_model (model: COLLECTION[COLLECTION[E]])
-- The model is used to fill line by line Current.
-- Assume all sub-collections of model have the same
-- number of lines.
require
model /= Void
ensure
count1 = model.count;
count2 > 0 implies count2 = model.first.count
feature(s) from COLLECTION2
-- Looking and comparison :
all_cleared: BOOLEAN
-- Are all items set to default values ?
same_as (other: COLLECTION2[E]): BOOLEAN
-- Unlike is_equal, this feature can be used to compare
-- distinct implementation of COLLECTION2.
require
other /= Void
ensure
Result implies standard_same_as(other)
feature(s) from COLLECTION2
-- 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 COLLECTION2
-- Miscellaneous features :
nb_occurrences (elt: E): INTEGER
-- Number of occurrences using equal.
-- See also fast_nb_occurrences to chose
-- the apropriate one.
ensure
Result >= 0;
Result >= 0
fast_nb_occurrences (elt: E): INTEGER
-- Number of occurrences using =.
ensure
Result >= 0;
Result >= 0
has (x: like item): BOOLEAN
-- Look for x using equal for comparison.
fast_has (x: like item): BOOLEAN
-- Same as has but use = for comparison
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
sub_collection2 (line_min, line_max, column_min, column_max: INTEGER): like Current
-- Create a new object using selected area of Current.
require
valid_index(line_min,column_min);
valid_index(line_min,column_min)
ensure
Result /= Void
set_area (element: like item; line_min, line_max, column_min, column_max: INTEGER)
-- Set all the elements of the selected area rectangle with element.
require
valid_index(line_min,line_max);
valid_index(column_min,column_max)
ensure
count = old count
feature(s) from FIXED_ARRAY2
make (new_count1, new_count2: INTEGER)
-- Create or reset Current with new dimensions.
-- All elements are set to the default value of type E.
require
new_count1 > 0;
new_count2 > 0
ensure
count1 = new_count1;
count2 = new_count2;
all_cleared
from_collection (model: COLLECTION2[like item])
-- Uses the model to update Current.
feature(s) from FIXED_ARRAY2
-- Implementation of others feature from COLLECTION2 :
copy (other: like Current)
require
other_not_void: other /= Void
ensure
is_equal: is_equal(other)
is_equal (other: like Current): BOOLEAN
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal(other) implies Result;
symmetric: Result implies other.is_equal(Current)
feature(s) from FIXED_ARRAY2
-- Writing :
slice (l1, up1, l2, up2: INTEGER): like Current
-- Create a new collection initialized with elements of
-- range low..up. Result has the same dynamic type
-- as Current collection.
set_slice (element: like item; l1, up1, l2, up2: INTEGER)
-- Set all the elements in the
-- range [(l1,up1),(l2,up2)] of
-- Current with the element 'element'.
feature(s) from FIXED_ARRAY2
-- Resizing :
resize (new_count1, new_count2: INTEGER)
require
new_count1 > 0;
new_count2 > 0
ensure
upper1 = new_count1 - 1;
count1 = new_count1;
upper2 = new_count2 - 1;
count2 = new_count2;
count = new_count1 * new_count2
feature(s) from FIXED_ARRAY2
-- Other features :
transpose
-- Transpose the Current array
to_external: POINTER
-- Gives C access to the internal storage (may be dangerous).
invariant
count1 = upper1 + 1;
count2 = upper2 + 1;
count = count1 * count2;
capacity >= count;
end of FIXED_ARRAY2[E]