indexing
description: "Sets whose items may be compared according to a partial 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
PART_SORTED_SET [G -> PART_COMPARABLE]
create
make
-- (from LINKED_LIST)
feature {ANY} -- Access
item: G
-- Current item
-- (from LINKED_LIST)
require -- from ACTIVE
readable: readable
require -- from TRAVERSABLE
not_off: not off
feature -- Access
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
feature -- Measurement
count: INTEGER
-- Number of items
-- (from LINKED_LIST)
feature -- 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
changeable_comparison_criterion: BOOLEAN
-- May object_comparison be changed?
-- (Answer: yes by default.)
-- (from CONTAINER)
ensure then -- from SET
only_on_empty: Result = empty
empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)
Extendible: BOOLEAN is true
-- May new items be added? (Answer: yes.)
-- (from DYNAMIC_CHAIN)
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)
feature {ANY} -- Status report
after: BOOLEAN
-- Is there no valid cursor position to the right of cursor?
-- (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
finish
-- Move cursor to last position.
-- (Go before if empty)
-- (from TWO_WAY_LIST)
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 -- from LINEAR
not_after: not after
start
-- Move cursor to first position.
-- (from LINKED_LIST)
ensure then -- from LINKED_LIST
empty_convention: empty implies after
ensure then -- from LINKED_LIST
empty_convention: empty implies after
feature -- Element change
extend (v: G)
-- Ensure that structure includes v.
-- Was declared in PART_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
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 -- from SUBSET
is_superset: is_superset (other)
put (v: G)
-- Ensure that structure includes v.
-- Was declared in PART_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)
feature {ANY} -- Element change
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;
feature -- Removal
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 PART_SORTED_TWO_WAY_LIST)
require -- DYNAMIC_CHAIN
precursor: True
require -- from COLLECTION
prunable
ensure -- from COLLECTION
no_more_occurrences: not has (v)
wipe_out
-- Remove all items.
-- (from TWO_WAY_LIST)
require -- DYNAMIC_LIST
precursor: True
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: empty
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
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
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 LINKED_LIST
prunable: prunable;
-- from FINITE
empty_definition: empty = (count = 0);
non_negative_count: count >= 0;
-- from DYNAMIC_CHAIN
extendible: extendible;
end -- class PART_SORTED_SET