Top
ARRAY
ARRAY3
class interface ARRAY2[E]
--
-- General prurpose, resizable, two dimensional array.
--
creation
make (line_min, line_max, column_min, column_max: INTEGER)
-- Reset all bounds line_minimum / line_maximum / column_minimum and
-- column_maximum using arguments as new values.
-- All elements are set to the default value of type E.
require
line_min <= line_max;
column_min <= column_max
ensure
line_minimum = line_min;
line_maximum = line_max;
column_minimum = column_min;
column_maximum = column_max
copy (other: like Current)
require
same_dynamic_type(other)
ensure
is_equal(other)
from_collection2 (model: COLLECTION2[like item])
-- Uses model to initialize Current.
require
model /= Void
ensure
lower1 = model.lower1;
lower2 = model.lower2;
count1 = model.count1;
count2 = model.count2
from_collection (contents: COLLECTION[E]; line_min, line_max, column_min, column_max: INTEGER)
-- Reset all bounds using line_min, line_max, column_min,
-- and column_max .
-- Copy all elements of contents, line by line into Current.
require
line_min <= line_max;
column_min <= column_max;
contents.count = (line_max - line_min + 1) * (column_max - column_min + 1)
ensure
line_minimum = line_min;
line_maximum = line_max;
column_minimum = column_min;
column_maximum = column_max;
count = contents.count
from_model (model: COLLECTION[COLLECTION[E]])
-- The model is used to fill line by line the COLLECTION2.
-- Assume all sub-collections of model have the same indexing.
require
model /= Void
ensure
line_minimum = model.lower;
line_maximum = model.upper;
column_minimum = model.first.lower;
column_maximum = model.first.upper;
count1 = model.count;
count2 > 0 implies count2 = model.first.count
feature(s) from COLLECTION2
-- Indexing:
lower1: INTEGER
-- Upper index bounds.
lower2: INTEGER
-- Upper index bounds.
line_minimum: INTEGER
-- Equivalent of lower1.
column_minimum: INTEGER
-- Equivalent of lower2.
upper1: INTEGER
-- Upper index bounds.
upper2: INTEGER
-- Upper index bounds.
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 (element: like item; line, column: INTEGER)
require
valid_index(line,column)
ensure
item(line,column) = element
force (x: 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
True
require else
line >= 0;
column >= 0
ensure
item(line,column) = x;
count >= old count
feature(s) from COLLECTION2
-- Index validity:
valid_line (line: INTEGER): BOOLEAN
ensure
Result = (lower1 <= line and line <= upper1)
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_column(column))
feature(s) from COLLECTION2
-- Counting:
count1: INTEGER
-- Size of the first dimension.
ensure
Result = upper1 - lower1 + 1
line_count: INTEGER
-- Equivalent of count1.
count2: INTEGER
-- Size of the second dimension.
ensure
Result = upper2 - lower2 + 1
column_count: INTEGER
count: INTEGER
-- Total number of elements.
ensure
Result = line_count * column_count
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 (element: E)
-- Set all item with value v.
ensure
count = old count
clear_all
-- Set all items to default values.
ensure
count = old count;
all_default
feature(s) from COLLECTION2
-- Creating or initializing:
from_collection2 (model: COLLECTION2[like item])
-- Uses model to initialize Current.
require
model /= Void
ensure
lower1 = model.lower1;
lower2 = model.lower2;
count1 = model.count1;
count2 = model.count2
from_model (model: COLLECTION[COLLECTION[E]])
-- The model is used to fill line by line the COLLECTION2.
-- Assume all sub-collections of model have the same indexing.
require
model /= Void
ensure
line_minimum = model.lower;
line_maximum = model.upper;
column_minimum = model.first.lower;
column_maximum = model.first.upper;
count1 = model.count;
count2 > 0 implies count2 = model.first.count
feature(s) from COLLECTION2
-- Looking and comparison:
all_default: BOOLEAN
-- Do all items have their type's default value?
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:
occurrences (elt: E): INTEGER
-- Number of occurrences using equal.
-- See also fast_occurrences to chose the apropriate one.
ensure
Result >= 0
fast_occurrences (elt: E): INTEGER
-- Number of occurrences using =.
-- See also occurrences to chose the apropriate one.
ensure
Result >= 0
has (x: like item): BOOLEAN
-- Search if a element x is in the array using equal.
-- See also fast_has to chose the apropriate one.
fast_has (x: like item): BOOLEAN
-- Search if a element x is in the array using =.
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
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_max,column_max)
ensure
Result.lower1 = line_min;
Result.lower2 = column_min;
Result.upper1 = line_max;
Result.upper2 = column_max;
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,column_min);
valid_index(line_max,column_max)
ensure
count = old count
feature(s) from ARRAY2
-- Creation / modification:
make (line_min, line_max, column_min, column_max: INTEGER)
-- Reset all bounds line_minimum / line_maximum / column_minimum and
-- column_maximum using arguments as new values.
-- All elements are set to the default value of type E.
require
line_min <= line_max;
column_min <= column_max
ensure
line_minimum = line_min;
line_maximum = line_max;
column_minimum = column_min;
column_maximum = column_max
from_collection (contents: COLLECTION[E]; line_min, line_max, column_min, column_max: INTEGER)
-- Reset all bounds using line_min, line_max, column_min,
-- and column_max .
-- Copy all elements of contents, line by line into Current.
require
line_min <= line_max;
column_min <= column_max;
contents.count = (line_max - line_min + 1) * (column_max - column_min + 1)
ensure
line_minimum = line_min;
line_maximum = line_max;
column_minimum = column_min;
column_maximum = column_max;
count = contents.count
feature(s) from ARRAY2
-- Resizing:
resize (line_min, line_max, column_min, column_max: INTEGER)
-- Resize bounds of the Current array
require
line_max >= line_min;
column_max >= column_min
ensure
line_minimum = line_min;
line_maximum = line_max;
column_minimum = column_min;
column_maximum = column_max
feature(s) from ARRAY2
-- Looking and comparison:
copy (other: like Current)
require
same_dynamic_type(other)
ensure
is_equal(other)
is_equal (other: like Current): BOOLEAN
require
other /= Void
ensure
generating_type = other.generating_type implies Result = other.is_equal(Current)
feature(s) from ARRAY2
-- Only for ARRAY2:
transpose
-- Transpose the Current array
ensure
line_minimum = old column_minimum;
column_minimum = old line_minimum;
line_maximum = old column_maximum;
column_maximum = old line_maximum;
count = old count
to_external: POINTER
-- Gives C access to the internal storage (may be dangerous).
invariant
count2 = upper2 - lower2 + 1;
capacity >= count;
end of ARRAY2[E]
All classes inherit from ANY, ANY inherits from
PLATFORM
and PLATFORM inherits from GENERAL.
Generated by short -html_deb on 31 March 2005.