indexing
description: "Sets whose items may be compared according to a total order relation; implemented as sorted two-way lists."
names: sorted_set, set, two_way_list
representation: linked
access: membership, min, max
contents: generic
class interface
TWO_WAY_SORTED_SET [G -> COMPARABLE]
create
make
-- Create an empty list.
-- (from LINKED_LIST)
ensure -- from LINKED_LIST
is_before: before
feature -- Initialization
make
-- Create an empty list.
-- (from LINKED_LIST)
ensure -- from LINKED_LIST
is_before: before
feature -- Access
cursor: CURSOR
-- Current cursor position
-- (from LINKED_LIST)
first: like item
-- Item at first position
-- (from LINKED_LIST)
require -- from CHAIN
not_empty: not empty
first_element: BI_LINKABLE [G]
-- Head of list
-- (Anchor redefinition)
-- (from TWO_WAY_LIST)
has (v: G): BOOLEAN
-- Does structure include v?
-- (Reference or object equality,
-- based on object_comparison.)
-- (from PART_SORTED_LIST)
ensure -- from CONTAINER
not_found_in_empty: Result implies not empty
i_th (i: INTEGER): like item
-- Item at i-th position
-- Was declared in CHAIN as synonym of i_th and @.
-- (from CHAIN)
require -- from TABLE
valid_key: valid_index (k)
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
last: like item
-- Item at last position
-- (from LINKED_LIST)
require -- from CHAIN
not_empty: not empty
last_element: like first_element
-- Tail of the list
-- (from TWO_WAY_LIST)
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
occurrences (v: like item): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from CHAIN)
ensure -- from BAG
non_negative_occurrences: Result >= 0
occurrences (v: like item): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from CHAIN)
ensure -- from BAG
non_negative_occurrences: Result >= 0
search_after (v: like item)
-- Go to first position with item greater
-- than or equal to v.
-- (from PART_SORTED_LIST)
ensure -- from PART_SORTED_LIST
argument_less_than_item: (not after) implies (v <= item)
search_before (v: like item)
-- Go to last position with item less
-- than or equal to v.
-- (from PART_SORTED_LIST)
ensure -- from PART_SORTED_LIST
(not off) implies (item <= v)
sublist: like Current
-- Result produced by last split
-- (from TWO_WAY_LIST)
infix "@" (i: INTEGER): like item
-- Item at i-th position
-- Was declared in CHAIN as synonym of i_th and @.
-- (from CHAIN)
require -- from TABLE
valid_key: valid_index (k)
feature {ANY} -- Access
index: INTEGER
-- Index of current position
-- (from LINKED_LIST)
item: G
-- Current item
-- (from LINKED_LIST)
require -- from ACTIVE
readable: readable
require -- from TRAVERSABLE
not_off: not off
feature -- Measurement
count: INTEGER
-- Number of items
-- (from LINKED_LIST)
max: like item
-- Maximum item
-- (from SORTED_LIST)
require -- from SORTED_LIST
not_empty: not empty
require -- from COMPARABLE_SET
not_empty: not empty
require -- from SORTED_LIST
not_empty: not empty
ensure -- from SORTED_LIST
max_is_last: Result = last
ensure -- from SORTED_LIST
max_is_last: Result = last
median: like item
-- Median item
-- (from SORTED_LIST)
require -- from SORTED_LIST
not_empty: not empty
ensure -- from SORTED_LIST
median_definition: Result = i_th ((count + 1) // 2)
min: like item
-- Minimum item
-- (from SORTED_LIST)
require -- from SORTED_LIST
not_empty: not empty
require -- from COMPARABLE_SET
not_empty: not empty
require -- from SORTED_LIST
not_empty: not empty
ensure -- from SORTED_LIST
min_is_first: Result = first
ensure -- from SORTED_LIST
min_is_first: Result = first
feature -- Comparison
disjoint (other: like Current): BOOLEAN
-- Do current set and other have no
-- items in common?
require -- from SUBSET
set_exists: other /= void;
same_rule: object_comparison = other.object_comparison
is_subset (other: like Current): BOOLEAN
-- Is current set a subset of other?
require -- from SUBSET
set_exists: other /= void;
same_rule: object_comparison = other.object_comparison
is_superset (other: like Current): BOOLEAN
-- Is current set a superset of other?
-- (from SUBSET)
require -- from SUBSET
set_exists: other /= void;
same_rule: object_comparison = other.object_comparison
feature -- Status report
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 is true
-- May new items be added? (Answer: yes.)
-- (from DYNAMIC_CHAIN)
Full: BOOLEAN is false
-- Is structured filled to capacity? (Answer: no.)
-- (from LINKED_LIST)
isfirst: BOOLEAN
-- Is cursor at first position?
-- (from LINKED_LIST)
ensure -- from CHAIN
valid_position: Result implies not empty
islast: BOOLEAN
-- Is cursor at last position?
-- (from TWO_WAY_LIST)
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)
prunable: BOOLEAN
-- May items be removed? (Answer: yes.)
-- (from DYNAMIC_CHAIN)
readable: BOOLEAN
-- Is there a current item that may be read?
-- (from LINKED_LIST)
sorted: BOOLEAN
-- Is the structure sorted?
-- (from SORTED_TWO_WAY_LIST)
valid_cursor (p: CURSOR): BOOLEAN
-- Can the cursor be moved to position p?
-- (from LINKED_LIST)
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 allowable bounds?
-- (from CHAIN)
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 {ANY} -- Status report
after: BOOLEAN
-- Is there no valid cursor position to the right of cursor?
-- (from LINKED_LIST)
before: BOOLEAN
-- Is there no valid cursor position to the left of cursor?
-- (from LINKED_LIST)
off: BOOLEAN
-- Is there no current item?
-- (from LINKED_LIST)
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 {ANY} -- Cursor movement
back
-- Move cursor to previous position, if any.
-- (from TWO_WAY_LIST)
require -- from BILINEAR
not_before: not before
ensure then -- from BILINEAR
moved_back: index = old index - 1
finish
-- Move cursor to last position.
-- (Go before if empty)
-- (from TWO_WAY_LIST)
ensure then -- from LINKED_LIST
empty_convention: empty implies before
ensure then -- from CHAIN
at_last: not empty implies islast
ensure then -- from TWO_WAY_LIST
not_after: not after
ensure then -- from TWO_WAY_LIST
not_after: not after
forth
-- Move cursor to next position, if any.
-- (from TWO_WAY_LIST)
require -- LIST
precursor: True
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.
-- (from LINKED_LIST)
require -- from CHAIN
valid_cursor_index: valid_cursor_index (i)
ensure -- from CHAIN
position_expected: 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.
-- (from LINKED_LIST)
ensure then -- from CHAIN
at_first: not empty implies isfirst
ensure then -- from LINKED_LIST
empty_convention: empty implies after
ensure then -- from LINKED_LIST
empty_convention: empty implies after
feature -- Cursor movement
go_to (p: CURSOR)
-- Move cursor to position p.
-- (from LINKED_LIST)
require -- from CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
move (i: INTEGER)
-- Move cursor i positions. The cursor
-- may end up off if the offset is to big.
-- (from TWO_WAY_LIST)
ensure then -- from LINKED_LIST
moved_if_inbounds: ((old index + i) >= 0 and (old index + i) <= (count + 1)) implies index = (old index + i);
before_set: (old index + i) <= 0 implies before;
after_set: (old index + i) >= (count + 1) implies after
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)
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: G)
-- Ensure that structure includes v.
-- Was declared in TWO_WAY_SORTED_SET as synonym of extend and put.
require -- from COLLECTION
extendible: extendible
ensure -- from COLLECTION
item_inserted: has (v)
ensure then -- from SET
in_set_already: old has (v) implies (count = old count);
added_to_set: not old has (v) implies (count = old count + 1)
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)
-- Add v to end.
-- (from SEQUENCE)
require -- from SEQUENCE
extendible: extendible
ensure then -- from SEQUENCE
new_count: count = old count + 1;
item_inserted: has (v)
merge (other: like Current)
-- Add all items of other.
require -- PART_SORTED_LIST
precursor: True
require -- from SUBSET
set_exists: other /= void;
same_rule: object_comparison = other.object_comparison
ensure then -- from PART_SORTED_LIST
remains_sorted: (old sorted) implies sorted
ensure -- from SUBSET
is_superset: is_superset (other)
merge_left (other: like Current)
-- Merge other into current structure before cursor
-- position. Do not move cursor. Empty other.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: extendible;
not_off: not before;
other_exists: other /= void
ensure -- from DYNAMIC_CHAIN
new_count: count = old count + old other.count;
new_index: index = old index + old other.count;
other_is_empty: other.empty
merge_right (other: like Current)
-- Merge other into current structure after cursor
-- position. Do not move cursor. Empty other.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: extendible;
not_off: not after;
other_exists: other /= void
ensure -- from DYNAMIC_CHAIN
new_count: count = old count + old other.count;
same_index: index = old index;
other_is_empty: other.empty
put (v: G)
-- Ensure that structure includes v.
-- Was declared in TWO_WAY_SORTED_SET as synonym of extend and put.
require -- from COLLECTION
extendible: extendible
ensure -- from COLLECTION
item_inserted: has (v)
ensure then -- from SET
in_set_already: old has (v) implies (count = old count);
added_to_set: not old has (v) implies (count = old count + 1)
put_front (v: like item)
-- Add v to beginning.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
ensure -- from DYNAMIC_CHAIN
new_count: count = old count + 1;
item_inserted: first = v
put_i_th (v: like item; i: INTEGER)
-- Put v at i-th position.
-- (from CHAIN)
require -- from TABLE
valid_key: valid_index (k)
ensure then -- from INDEXABLE
insertion_done: i_th (k) = v
put_left (v: like item)
-- Add v to the left of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: extendible;
not_before: not before
ensure -- from DYNAMIC_CHAIN
new_count: count = old count + 1;
new_index: index = old index + 1
put_right (v: like item)
-- Add v to the right of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: extendible;
not_after: not after
ensure -- from DYNAMIC_CHAIN
new_count: count = old count + 1;
same_index: index = old index
replace (v: like item)
-- Replace current item by v.
-- (from LINKED_LIST)
require -- from ACTIVE
writable: writable
ensure -- from ACTIVE
item_replaced: item = v
feature -- Removal
changeable_comparison_criterion: BOOLEAN
-- May object_comparison be changed?
-- (Answer: only if set empty; otherwise insertions might
-- introduce duplicates, destroying the set property.)
-- (from SET)
ensure then -- from SET
only_on_empty: Result = empty
ensure then -- from SET
only_on_empty: Result = empty
prune (v: like item)
-- Remove v if present.
require -- from COLLECTION
prunable: prunable
ensure then -- from SET
removed_count_change: old has (v) implies (count = old count - 1);
not_removed_no_count_change: not old has (v) implies (count = old count);
item_deleted: not has (v)
prune_all (v: like item)
-- Remove all items identical to v.
-- (Reference or object equality,
-- based on object_comparison.)
-- Leave cursor off.
-- (from SORTED_TWO_WAY_LIST)
require -- DYNAMIC_CHAIN
precursor: True
require -- from COLLECTION
prunable
ensure then -- from DYNAMIC_CHAIN
is_exhausted: exhausted
ensure -- from COLLECTION
no_more_occurrences: not has (v)
remove_left
-- Remove item to the left of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
left_exists: index > 1
require else -- from DYNAMIC_LIST
not_before: not before
ensure -- from DYNAMIC_CHAIN
new_count: count = old count - 1;
new_index: index = old index - 1
remove_right
-- Remove item to the right of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
right_exists: index < count
ensure -- from DYNAMIC_CHAIN
new_count: count = old count - 1;
same_index: index = old index
remove_sublist
-- (from TWO_WAY_LIST)
split (n: INTEGER)
-- Remove from current list
-- min (n, count - index - 1) items
-- starting at cursor position.
-- Move cursor right one position.
-- Make extracted sublist accessible
-- through attribute sublist.
-- (from TWO_WAY_LIST)
require -- from TWO_WAY_LIST
not_off: not off;
valid_sublist: n >= 0
wipe_out
-- Remove all items.
-- (from TWO_WAY_LIST)
require -- DYNAMIC_LIST
precursor: True
require -- from COLLECTION
prunable
ensure then -- from DYNAMIC_LIST
is_before: before
ensure -- from COLLECTION
wiped_out: empty
feature {ANY} -- Removal
remove
-- Remove current item.
-- Move cursor to right neighbor
-- (or after if no right neighbor).
-- (from TWO_WAY_LIST)
require -- DYNAMIC_LIST
precursor: True
require -- from ACTIVE
prunable: prunable;
writable: writable
ensure then -- from DYNAMIC_LIST
after_when_empty: empty implies after
feature -- Transformation
sort
-- Sort all items.
-- Has O(count * log (count)) complexity.
-- (from SORTED_TWO_WAY_LIST)
swap (i: INTEGER)
-- Exchange item at i-th position with item
-- at cursor position.
-- (from CHAIN)
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
duplicate (n: INTEGER): like Current
-- Copy of sub-set 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
require -- from SUBSET
non_negative: n >= 0
ensure -- from SUBSET
correct_count_1: n <= count implies Result.count = n;
correct_count_2: n >= count implies Result.count = count
feature -- Basic operations
intersect (other: like Current)
-- Remove all items not in other.
require -- from SUBSET
set_exists: other /= void;
same_rule: object_comparison = other.object_comparison
ensure -- from SUBSET
is_subset_other: is_subset (other)
subtract (other: like Current)
-- Remove all items also in other.
require -- from SUBSET
set_exists: other /= void;
same_rule: object_comparison = other.object_comparison
ensure -- from SUBSET
is_disjoint: disjoint (other)
symdif (other: like Current)
-- Remove all items also in other, and add all items
-- of other not already present.
require -- from SUBSET
set_exists: other /= void;
same_rule: object_comparison = other.object_comparison
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- 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 LINKED_LIST
prunable: prunable;
-- 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 FINITE
empty_definition: empty = (count = 0);
non_negative_count: count >= 0;
-- from DYNAMIC_CHAIN
extendible: extendible;
end -- class TWO_WAY_SORTED_SET