Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

structure.set

Class DS_SET


Direct ancestors

DS_LINEAR, DS_EXTENDIBLE

Known direct descendants

DS_SPARSE_SET

Features

Invariants

indexing

description

Data structures whose items appear only once

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/06/04 22:24:40 $

revision

$Revision: 1.9 $

deferred class

DS_SET [G]

inherit

DS_LINEAR
DS_EXTENDIBLE

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
equality_tester: KL_EQUALITY_TESTER [G]

-- Equality tester;
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

first: G

-- First item in container

-- (From DS_LINEAR)

require
not_empty: not is_empty
ensure
has_first: has (Result)
infix "@" (v: G): G

-- Item equal to v held in set
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
has_v: has (v)
ensure
definition: same_items (Result, v)
intersection (other: DS_SET [G]): like Current

-- Clone of current set from with all items
-- not included in other have been removed
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
intersection_not_void: Result /= Void
is_subset: Result.is_subset (other)
item (v: G): G

-- Item equal to v held in set
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
has_v: has (v)
ensure
definition: same_items (Result, v)
item_for_iteration: G

-- Item at internal cursor position

-- (From DS_TRAVERSABLE)

require
not_off: not off
new_cursor: DS_SET_CURSOR [G]

-- New external cursor for traversal

-- (From DS_TRAVERSABLE)

ensure
cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)
subtraction (other: DS_SET [G]): like Current

-- Clone of current set from which all items
-- also included in other have been removed
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
subtraction_not_void: Result /= Void
is_disjoint: Result.is_disjoint (other)
symdifference (other: DS_SET [G]): like Current

-- Clone of current clone to which items of other
-- which are not included in current set have been
-- added and from which those which are current set
-- have been removed
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
symdifference_not_void: Result /= Void
union (other: DS_SET [G]): like Current

-- Clone of current set to which all items
-- of other have been added
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
union_not_void: Result /= Void
is_superset: Result.is_superset (other)

feature -- Measurement

count: INTEGER

-- Number of items in container

-- (From DS_CONTAINER)

occurrences (v: G): INTEGER

-- Number of times v appears in set
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
positive: Result >= 0
has: has (v) implies Result >= 1
ensure then
has_v: has (v) implies (Result = 1)
not_has_v: not has (v) implies (Result = 0)

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is other attached to an object considered
-- equal to current object?

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result

feature -- Status report

after: BOOLEAN

-- Is there no valid position to right of internal cursor?

-- (From DS_LINEAR)

equality_tester_settable (a_tester: like equality_tester): BOOLEAN

-- Can set_equality_tester be called with a_tester
-- as argument in current state of container?
-- (Answer: the set has to be empty.)

-- (From DS_SEARCHABLE)

extendible (n: INTEGER): BOOLEAN

-- May container be extended with n items?

-- (From DS_EXTENDIBLE)

require
positive_n: n >= 0
has (v: G): BOOLEAN

-- Does container include v?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

ensure
not_empty: Result implies not is_empty
is_disjoint (other: DS_SET [G]): BOOLEAN

-- Are none of the items of current set included in other?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

is_first: BOOLEAN

-- Is internal cursor on first item?

-- (From DS_LINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = first)
is_subset (other: DS_SET [G]): BOOLEAN

-- Are all items of current set included in other?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
is_superset (other: DS_SET [G]): BOOLEAN

-- Does current set include all items of other?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
definition: Result = other.is_subset (Current)
off: BOOLEAN

-- Is there no item at internal cursor position?

-- (From DS_TRAVERSABLE)

same_equality_tester (other: DS_SEARCHABLE [G]): BOOLEAN

-- Does container use the same comparison
-- criterion as other?

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: G): BOOLEAN

-- Are v and u considered equal?
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_SEARCHABLE)

same_position (a_cursor: like new_cursor): BOOLEAN

-- Is internal cursor at same position as a_cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
valid_cursor (a_cursor: DS_CURSOR [G]): BOOLEAN

-- Is a_cursor a valid cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void

feature -- Cursor movement

forth

-- Move internal cursor to next position.

-- (From DS_LINEAR)

require
not_after: not after
go_after

-- Move internal cursor to after position.

-- (From DS_LINEAR)

ensure
after: after
go_to (a_cursor: like new_cursor)

-- Move internal cursor to a_cursor's position.

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
valid_cursor: valid_cursor (a_cursor)
ensure
same_position: same_position (a_cursor)
search_forth (v: G)

-- Move internal cursor to first position at or after current
-- position where item_for_iteration and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
not_off: not off or after
start

-- Move internal cursor to first position.

-- (From DS_LINEAR)

ensure
empty_behavior: is_empty implies after
not_empty_behavior: not is_empty implies is_first

feature -- Element change

append (other: DS_LINEAR [G])

-- Add items of other to set, replacing any existing item.
-- Add other.first first, etc.

require
other_not_void: other /= Void
append_last (other: DS_LINEAR [G])

-- Add items of other to set, replacing any existing item.
-- Add other.first first, etc.
-- If items of other were not included yet, insert
-- them at last position if implementation permits.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
extend (other: DS_LINEAR [G])

-- Add items of other to set, replacing any existing item.
-- Add other.first first, etc.

require
other_not_void: other /= Void
extendible: extendible (other.count)
extend_last (other: DS_LINEAR [G])

-- Add items of other to set, replacing any existing item.
-- Add other.first first, etc.
-- If items of other were not included yet, insert
-- them at last position if implementation permits.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
force (v: G)

-- Add v to set, replacing any existing item.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

ensure
inserted: has (v) and then item (v) = v
same_count: (old has (v)) implies (count = old count)
one_more: (not old has (v)) implies (count = old count + 1)
force_last (v: G)

-- Add v to set, replacing any existing item.
-- If v was not included yet, insert it at
-- last position if implementation permits.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_EXTENDIBLE)

ensure
added: has (v)
ensure then
inserted: has (v) and then item (v) = v
same_count: (old has (v)) implies (count = old count)
one_more: (not old has (v)) implies (count = old count + 1)
force_new (v: G)

-- Add v to set.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
new_item: not has (v)
ensure
one_more: count = old count + 1
inserted: has (v) and then item (v) = v
put (v: G)

-- Add v to set, replacing any existing item.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
extendible: extendible (1)
ensure
inserted: has (v) and then item (v) = v
same_count: (old has (v)) implies (count = old count)
one_more: (not old has (v)) implies (count = old count + 1)
put_last (v: G)

-- Add v to set, replacing any existing item.
-- If v was not included yet, insert it at
-- last position if implementation permits.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

-- (From DS_EXTENDIBLE)

require
extendible: extendible (1)
ensure
added: has (v)
ensure then
inserted: has (v) and then item (v) = v
same_count: (old has (v)) implies (count = old count)
one_more: (not old has (v)) implies (count = old count + 1)
put_new (v: G)

-- Add v to set.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
extendible: extendible (1)
new_item: not has (v)
ensure
one_more: count = old count + 1
inserted: has (v) and then item (v) = v

feature -- Removal

remove (v: G)

-- Remove item equal to v from set.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

ensure
same_count: (not old has (v)) implies (count = old count)
one_less: (old has (v)) implies (count = old count - 1)
removed: not has (v)
wipe_out

-- Remove all items from container.

-- (From DS_CONTAINER)

ensure
wiped_out: is_empty

feature -- Duplication

cloned_object: like Current

-- Clone of current object

-- (From KL_CLONABLE)

ensure
cloned_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
is_equal: Result.is_equal (Current)
copy (other: like Current)

-- Update current object using fields of object attached
-- to other, so as to yield equal objects.

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)
to_array: ARRAY [G]

-- Array containing the same items as current
-- container in the same order

-- (From DS_LINEAR)

ensure
to_array_not_void: Result /= Void
same_count: Result.count = count

feature -- Basic operations

intersect (other: DS_SET [G])

-- Remove all items not included in other.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
is_subset: is_subset (other)
merge (other: DS_SET [G])

-- Add all items of other to current set.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
is_superset: is_superset (other)
subtract (other: DS_SET [G])

-- Remove all items also included in other.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)
ensure
is_disjoint: is_disjoint (other)
symdif (other: DS_SET [G])

-- Add items of other which are not included
-- in current set and remove those which are.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)

require
other_not_void: other /= Void
same_equality_tester: same_equality_tester (other)

feature {DS_CURSOR} -- Cursor implementation

add_traversing_cursor (a_cursor: like new_cursor)

-- Add a_cursor to the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
cursor_after (a_cursor: like new_cursor): BOOLEAN

-- Is there no valid position to right of a_cursor?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_forth (a_cursor: like new_cursor)

-- Move a_cursor to next position.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_after: not cursor_after (a_cursor)
cursor_go_after (a_cursor: like new_cursor)

-- Move a_cursor to after position.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_after: cursor_after (a_cursor)
cursor_go_to (a_cursor, other: like new_cursor)

-- Move a_cursor to other's position.

-- (From DS_TRAVERSABLE)

require
cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
other_valid: valid_cursor (other)
ensure
same_position: cursor_same_position (a_cursor, other)
cursor_is_first (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on first item?

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
not_empty: Result implies not is_empty
a_cursor_not_off: Result implies not cursor_off (a_cursor)
definition: Result implies (cursor_item (a_cursor) = first)
cursor_item (a_cursor: like new_cursor): G

-- Item at a_cursor position

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor)
cursor_off (a_cursor: like new_cursor): BOOLEAN

-- Is there no item at a_cursor position?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
cursor_same_position (a_cursor, other: like new_cursor): BOOLEAN

-- Is a_cursor at same position as other?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
other_not_void: other /= Void
cursor_search_forth (a_cursor: like new_cursor; v: G)

-- Move a_cursor to first position at or after its current
-- position where cursor_item (a_cursor) and v are equal.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Move after if not found.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_off: not cursor_off (a_cursor) or cursor_after (a_cursor)
cursor_start (a_cursor: like new_cursor)

-- Move a_cursor to first position.

-- (From DS_LINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_after (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_first (a_cursor)
remove_traversing_cursor (a_cursor: like new_cursor)

-- Remove a_cursor from the list of traversing cursors
-- (i.e. cursors associated with current container
-- and which are not currently off).

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void

feature -- Setting

set_equality_tester (a_tester: like equality_tester)

-- Set equality_tester to a_tester.
-- A void equality tester means that =
-- will be used as comparison criterion.

-- (From DS_SEARCHABLE)

require
equality_tester_settable: equality_tester_settable (a_tester)
ensure
equality_tester_set: equality_tester = a_tester

invariant

-- From DS_LINEAR
after_constraint: initialized implies (after implies off)

empty_constraint: initialized implies (is_empty implies off)
internal_cursor_not_void: initialized implies (internal_cursor /= Void)
valid_internal_cursor: initialized implies valid_cursor (internal_cursor)

-- From DS_CONTAINER
positive_count: count >= 0
empty_definition: is_empty = (count = 0)

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end