indexing
description: "Lists with fixed maximum numbers of items, implemented by arrays"
names: fixed, sequence
representation: array
access: index, cursor, membership
contents: generic
class interface
FIXED_LIST [G]
create
make (n: INTEGER)
-- Create an empty list.
ensure
is_before: before;
new_count: count = 0
make_filled (n: INTEGER)
-- Create a list with n void elements.
ensure
is_before: before;
new_count: count = n
feature -- Initialization
make (n: INTEGER)
-- Create an empty list.
ensure
is_before: before;
new_count: count = 0
make_filled (n: INTEGER)
-- Create a list with n void elements.
ensure
is_before: before;
new_count: count = n
setup (other: like Current)
-- Perform actions on a freshly created object so that
-- the contents of other can be safely copied onto it.
-- (from ARRAY)
ensure -- from GENERAL
consistent (other)
feature -- Access
count: INTEGER
cursor: CURSOR
-- Current cursor position
first: G
-- Item at first position
require -- from CHAIN
not_empty: not empty
has (v: G): BOOLEAN
-- Does v appear in array?
-- (Reference or object equality,
-- based on object_comparison.)
-- (from ARRAY)
ensure -- from CONTAINER
not_found_in_empty: Result implies not empty
index: INTEGER
-- Current position in the list
index_of (v: like item; i: INTEGER): INTEGER
-- Index of i-th occurrence of item identical to v.
-- (Reference or object equality,
-- based on object_comparison.)
-- 0 if none.
-- (from CHAIN)
require -- from LINEAR
positive_occurrences: i > 0
ensure -- from LINEAR
non_negative_result: Result >= 0
frozen i_th (i: INTEGER): G
-- Entry at index i, if in index interval
-- Was declared in ARRAY as synonym of item, @ and entry.
-- (from ARRAY)
require -- from TABLE
valid_key: valid_index (k)
item: G
-- Current item
require -- from ACTIVE
readable: readable
require -- from TRAVERSABLE
not_off: not off
last: like first
-- Item at last position
require -- from CHAIN
not_empty: not empty
sequential_occurrences (v: G): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from LINEAR)
ensure -- from BAG
non_negative_occurrences: Result >= 0
frozen infix "@" (i: INTEGER): G
-- Entry at index i, if in index interval
-- Was declared in ARRAY as synonym of item, @ and entry.
-- (from ARRAY)
require -- from TABLE
valid_key: valid_index (k)
feature {ANY} -- Access
area: SPECIAL [G]
-- Special data zone
-- (from TO_SPECIAL)
feature -- Measurement
capacity: INTEGER
-- Number of available indices
-- Was declared in ARRAY as synonym of count and capacity.
-- (from ARRAY)
occurrences (v: G): INTEGER
-- Number of times v appears in structure
-- (from ARRAY)
ensure -- from BAG
non_negative_occurrences: Result >= 0
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is array made of the same items as other?
-- (from ARRAY)
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
after: BOOLEAN
-- Is there no valid cursor position to the right of cursor?
-- (from LIST)
before: BOOLEAN
-- Is there no valid cursor position to the left of cursor?
-- (from LIST)
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).
-- (from ARRAY)
empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)
exhausted: BOOLEAN
-- Has structure been completely explored?
-- (from LINEAR)
ensure -- from LINEAR
exhausted_when_off: off implies Result
extendible: BOOLEAN
-- May new items be added?
full: BOOLEAN
-- Is the list full?
isfirst: BOOLEAN
-- Is cursor at first position?
-- (from CHAIN)
ensure -- from CHAIN
valid_position: Result implies not empty
islast: BOOLEAN
-- Is cursor at last position?
-- (from CHAIN)
ensure -- from CHAIN
valid_position: Result implies not empty
object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)
off: BOOLEAN
-- Is there no current item?
-- (from CHAIN)
prunable: BOOLEAN
-- May items be removed?
readable: BOOLEAN
-- Is there a current item that may be read?
-- (from SEQUENCE)
Resizable: BOOLEAN is false
-- May capacity be changed? (Answer: no.)
-- (from FIXED)
valid_cursor (p: CURSOR): BOOLEAN
-- Is p a valid cursor?
valid_cursor_index (i: INTEGER): BOOLEAN
-- Is i correctly bounded for cursor movement?
-- (from CHAIN)
ensure -- from CHAIN
valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1))
valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the array?
-- (from ARRAY)
ensure then -- from CHAIN
valid_index_definition: Result = ((i >= 1) and (i <= count))
writable: BOOLEAN
-- Is there a current item that may be modified?
-- (from SEQUENCE)
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 -- Cursor movement
back
-- Move cursor to previous position, if any.
require -- from BILINEAR
not_before: not before
ensure then -- from BILINEAR
moved_back: index = old index - 1
finish
-- Move cursor to last position.
ensure then -- from CHAIN
at_last: not empty implies islast
forth
-- Move cursor to next position, if any.
require -- from LINEAR
not_after: not after
ensure then -- from LIST
moved_forth: index = old index + 1
go_i_th (i: INTEGER)
-- Move cursor to i-th position.
require -- from CHAIN
valid_cursor_index: valid_cursor_index (i)
ensure -- from CHAIN
position_expected: index = i
go_to (p: CURSOR)
-- Move cursor to element remembered in p.
require -- from CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
move (i: INTEGER)
-- Move cursor i positions.
ensure -- from CHAIN
too_far_right: (old index + i > count) implies exhausted;
too_far_left: (old index + i < 1) implies exhausted;
expected_index: (not exhausted) implies (index = old index + i)
search (v: like item)
-- Move to first position (at or after current
-- position) where item and v are equal.
-- If structure does not include v ensure that
-- exhausted will be true.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from BILINEAR)
ensure -- from LINEAR
object_found: (not exhausted and object_comparison) implies equal (v, item);
item_found: (not exhausted and not object_comparison) implies v = item
start
-- Move cursor to first position.
ensure then -- from CHAIN
at_first: not empty implies isfirst
feature -- Element change
append (s: SEQUENCE [G])
-- Append a copy of s.
-- (from SEQUENCE)
require -- from SEQUENCE
argument_not_void: s /= void
ensure -- from SEQUENCE
new_count: count >= old count
extend (v: like item)
-- Add v to end.
-- Move index to the current item.
require -- from COLLECTION
extendible: extendible
ensure -- from COLLECTION
item_inserted: has (v)
ensure then -- from BAG
one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1
frozen put_i_th (v: like i_th; i: INTEGER)
-- Replace i-th entry, if in index interval, by v.
-- Was declared in ARRAY as synonym of put and enter.
-- (from ARRAY)
require -- from TABLE
valid_key: valid_index (k)
ensure then -- from INDEXABLE
insertion_done: i_th (k) = v
put (v: like first)
-- Replace current item by v.
-- (Synonym for replace)
require -- CHAIN
precursor: True
require -- from COLLECTION
extendible: extendible
require else
true
ensure then -- from CHAIN
same_count: count = old count
ensure -- from COLLECTION
item_inserted: has (v)
remove
-- Remove current item.
-- Move cursor to right neighbor
-- (or after if no right neighbor)
require -- from ACTIVE
prunable: prunable;
writable: writable
replace (v: like first)
-- Replace current item by v.
require -- from ACTIVE
writable: writable
ensure -- from ACTIVE
item_replaced: item = v
feature -- Removal
wipe_out
-- Make array empty.
-- (from ARRAY)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: empty
feature -- Transformation
swap (i: INTEGER)
-- Exchange item at i-th position with item
-- at cursor position.
require -- from CHAIN
not_off: not off;
valid_index: valid_index (i)
ensure -- from CHAIN
swapped_to_item: item = old i_th (i);
swapped_from_item: i_th (i) = old item
feature -- Conversion
linear_representation: LINEAR [G]
-- Representation as a linear structure
-- (from LINEAR)
feature -- Duplication
copy (other: like Current)
-- Reinitialize by copying all the items of other.
-- (This is also used by clone.)
-- (from ARRAY)
require -- ARRAY
precursor: True
require -- from GENERAL
other_not_void: other /= void;
type_identity: same_type (other)
ensure then -- from ARRAY
equal_areas: area.is_equal (other.area)
ensure -- from GENERAL
is_equal: is_equal (other)
ensure then -- from ARRAY
equal_areas: area.is_equal (other.area)
duplicate (n: INTEGER): like Current
-- Copy of sub-list beginning at cursor position
-- and having min (n, count - index + 1) items
require -- from CHAIN
not_off_unless_after: off implies after;
valid_subchain: n >= 0
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from LIST
before_definition: before = (index = 0);
after_definition: after = (index = count + 1);
-- from CHAIN
non_negative_index: index >= 0;
index_small_enough: index <= count + 1;
off_definition: off = ((index = 0) or (index = count + 1));
isfirst_definition: isfirst = ((not empty) and (index = 1));
islast_definition: islast = ((not empty) and (index = count));
item_corresponds_to_index: (not off) implies (item = i_th (index));
-- from ACTIVE
writable_constraint: writable implies readable;
empty_constraint: empty implies (not readable) and (not writable);
-- from BILINEAR
not_both: not (after and before);
empty_property: empty implies (after or before);
before_constraint: before implies off;
-- from LINEAR
after_constraint: after implies off;
-- from TRAVERSABLE
empty_constraint: empty implies off;
-- from FINITE
empty_definition: empty = (count = 0);
non_negative_count: count >= 0;
-- from ARRAY
non_negative_count: count >= 0;
-- from BOUNDED
valid_count: count <= capacity;
full_definition: full = (count = capacity);
-- from FIXED
not_resizable: not resizable;
end -- class FIXED_LIST