Class ARRAY
Halstenbach Eiffel 3.1
indexing
description: "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 + 1).
require
valid_indices: minindex <= maxindex or (minindex = maxindex + 1)
ensure
lower = minindex;
upper = maxindex
feature -- Initialization
make (minindex, maxindex: INTEGER)
-- Allocate array; set index interval to
-- minindex .. maxindex; set all values to default.
-- (Make array empty if minindex = maxindex + 1).
require
valid_indices: minindex <= maxindex or (minindex = maxindex + 1)
ensure
lower = minindex;
upper = maxindex
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
array_exists: a /= void
setup (other: like Current)
-- Perform actions on a freshly created object so that
-- the contents of other can be safely copied onto it.
ensure -- from GENERAL
consistent (other)
feature -- Access
area: SPECIAL [G]
-- Special data zone
-- (from TO_SPECIAL)
entry (i: INTEGER): G
-- Entry at index i, if in index interval
-- Was declared in ARRAY as synonym of item, @ and entry.
has (v: G): BOOLEAN
-- Does v appear in array?
-- (Reference or object equality,
-- based on object_comparison.)
ensure -- from CONTAINER
not_found_in_empty: Result implies not empty
frozen item (i: INTEGER): G
-- Entry at index i, if in index interval
-- Was declared in ARRAY as synonym of item, @ and entry.
require -- from TABLE
valid_key: valid_index (i)
frozen infix "@" (i: INTEGER): G
-- Entry at index i, if in index interval
-- Was declared in ARRAY as synonym of item, @ and entry.
require -- from TABLE
valid_key: valid_index (i)
feature -- Measurement
additional_space: INTEGER
-- Proposed number of additional items
-- (from RESIZABLE)
ensure -- from RESIZABLE
at_least_one: Result >= 1
capacity: INTEGER
-- Number of available indices
-- Was declared in ARRAY as synonym of count and capacity.
count: INTEGER
-- Number of available indices
-- Was declared in ARRAY as synonym of count and capacity.
Growth_percentage: INTEGER is 50
-- Percentage by which structure will grow automatically
-- (from RESIZABLE)
lower: INTEGER
-- Minimum index
Minimal_increase: INTEGER is 5
-- Minimal number of additional items
-- (from RESIZABLE)
occurrences (v: G): INTEGER
-- Number of times v appears in structure
ensure -- from BAG
non_negative_occurrences: Result >= 0
upper: INTEGER
-- Maximum index
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is array made of the same items as other?
require -- from GENERAL
other_not_void: other /= void
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result
feature -- Status report
all_cleared: BOOLEAN
-- Are all items set to default values?
changeable_comparison_criterion: BOOLEAN
-- May object_comparison be changed?
-- (Answer: yes by default.)
-- (from CONTAINER)
consistent (other: like Current): BOOLEAN
-- Is object in a consistent state so that other
-- may be copied onto it? (Default answer: yes).
empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)
extendible: BOOLEAN
-- May items be added?
-- (Answer: no, although array may be resized.)
full: BOOLEAN
-- Is structure filled to capacity? (Answer: yes)
object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)
prunable: BOOLEAN
-- May items be removed? (Answer: no.)
resizable: BOOLEAN
-- May capacity be changed? (Answer: yes.)
-- (from RESIZABLE)
valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the array?
feature -- Status setting
compare_objects
-- Ensure that future search operations will use equal
-- rather than = for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
object_comparison
compare_references
-- Ensure that future search operations will use =
-- rather than equal for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
reference_comparison: not object_comparison
feature -- Element change
enter (v: like item; i: INTEGER)
-- Replace i-th entry, if in index interval, by v.
-- Was declared in ARRAY as synonym of put and enter.
fill (other: CONTAINER [G])
-- Fill with as many items of other as possible.
-- The representations of other and current structure
-- need not be the same.
-- (from COLLECTION)
require -- from COLLECTION
other_not_void: other /= void;
extendible
force (v: like item; i: INTEGER)
-- Assign item v to i-th entry.
-- Always applicable: resize the array if i falls out of
-- currently defined bounds; preserve existing items.
ensure
inserted: item (i) = v;
higher_count: count >= old count
frozen put (v: like item; i: INTEGER)
-- Replace i-th entry, if in index interval, by v.
-- Was declared in ARRAY as synonym of put and enter.
require -- from TABLE
valid_key: valid_index (i)
ensure then -- from INDEXABLE
insertion_done: item (i) = v
subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER)
-- Copy items of other within bounds start_pos and end_pos
-- to current array starting at index index_pos.
require
other_not_void: other /= void;
valid_start_pos: other.valid_index (start_pos);
valid_end_pos: other.valid_index (end_pos);
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1);
valid_index_pos: valid_index (index_pos);
enough_space: (upper - index_pos) >= (end_pos - start_pos)
feature -- Removal
clear_all
-- Reset all items to default values.
ensure
all_cleared: all_cleared
prune_all (v: G)
-- Remove all occurrences of v.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from COLLECTION)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
no_more_occurrences: not has (v)
wipe_out
-- Make array empty.
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: empty
feature -- Resizing
automatic_grow
-- Change the capacity to accommodate at least
-- Growth_percentage more items.
-- (from RESIZABLE)
ensure -- from RESIZABLE
increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100
grow (i: INTEGER)
-- Change the capacity to at least i.
ensure -- from RESIZABLE
new_capacity: capacity >= i
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.
require
good_indices: minindex <= maxindex
ensure
no_low_lost: lower = minindex.min (old lower);
no_high_lost: upper = maxindex.max (old upper)
feature -- Conversion
linear_representation: LINEAR [G]
-- Representation as a linear structure
to_c: ANY
-- Address of actual sequence of values,
-- for passing to external (non-Eiffel) routines.
feature -- Duplication
copy (other: like Current)
-- Reinitialize by copying all the items of other.
-- (This is also used by clone.)
require -- from GENERAL
other_not_void: other /= void;
type_identity: same_type (other)
ensure -- from GENERAL
is_equal: is_equal (other)
ensure then
equal_areas: area.is_equal (other.area)
subarray (start_pos, end_pos: INTEGER): like Current
-- Array made of items of current array within
-- bounds start_pos and end_pos.
require
valid_start_pos: valid_index (start_pos);
valid_end_pos: valid_index (end_pos);
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
ensure
lower: Result.lower = start_pos;
upper: Result.upper = end_pos
invariant
consistent_size: count = upper - lower + 1;
non_negative_count: count >= 0;
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from RESIZABLE
increase_by_at_least_one: minimal_increase >= 1;
-- from BOUNDED
valid_count: count <= capacity;
full_definition: full = (count = capacity);
-- from FINITE
empty_definition: empty = (count = 0);
non_negative_count: count >= 0;
end -- class ARRAY