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

structure.set

Class DS_SPARSE_SET


Direct ancestors

DS_SET, DS_SPARSE_CONTAINER, KL_IMPORTED_ANY_ROUTINES

Known direct descendants

DS_ARRAYED_SPARSE_SET, DS_MULTIARRAYED_SPARSE_SET

Features

Invariants

indexing

description

Sets implemented with sparse arrays. Ancestor of hash sets %
%which should supply its hashing mechanism.

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 1999-2003, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/02/07 16:31:32 $

revision

$Revision: 1.24 $

deferred class

DS_SPARSE_SET [G]

inherit

DS_SET
DS_SPARSE_CONTAINER

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)
found_item: G

-- Item found by last call to search

-- (From DS_SPARSE_CONTAINER)

require
item_found: found
infix "@" (v: G): G

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

-- (From DS_SET)

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.)

-- (From DS_SET)

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.)

-- (From DS_SET)

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
last: G

-- Last item in container

-- (From DS_BILINEAR)

require
not_empty: not is_empty
ensure
has_last: has (Result)
new_cursor: DS_SPARSE_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.)

-- (From DS_SET)

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.)

-- (From DS_SET)

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.)

-- (From DS_SET)

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

capacity: INTEGER

-- Maximum number of items in container

-- (From DS_RESIZABLE)

count: INTEGER

-- Number of items in container

-- (From DS_CONTAINER)

default_capacity: INTEGER

-- Initial capacity in make_default
-- (Default value: 10)

-- (From DS_RESIZABLE)

ensure
default_capacity_positive: Result >= 0
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 set equal to other?
-- Do not take cursor positions, and capacity into
-- account, but equality_tester should be the same.

-- (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)

before: BOOLEAN

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

-- (From DS_BILINEAR)

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 set be extended with n items?

-- (From DS_EXTENDIBLE)

require
positive_n: n >= 0
ensure then
enough_space: Result implies (capacity >= count + n)
found: BOOLEAN

-- Did last call to search succeed?

-- (From DS_SPARSE_CONTAINER)

ensure
definition: Result = (found_position /= No_position)
has (v: G): BOOLEAN

-- Does set 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.)

-- (From DS_SET)

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_full: BOOLEAN

-- Is container full?

-- (From DS_RESIZABLE)

is_last: BOOLEAN

-- Is internal cursor on last item?

-- (From DS_BILINEAR)

ensure
not_empty: Result implies not is_empty
not_off: Result implies not off
definition: Result implies (item_for_iteration = last)
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.)

-- (From DS_SET)

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.)

-- (From DS_SET)

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

back

-- Move internal cursor to previous position.

-- (From DS_BILINEAR)

require
not_before: not before
finish

-- Move internal cursor to last position.

-- (From DS_BILINEAR)

ensure
empty_behavior: is_empty implies before
not_empty_behavior: not is_empty implies is_last
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_before

-- Move internal cursor to before position.

-- (From DS_BILINEAR)

ensure
before: before
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_back (v: G)

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

-- (From DS_BILINEAR)

require
not_off: not off or before
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.
-- Resize set if necessary.
-- Do not move cursors.

-- (From DS_SET)

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.
-- Resize set if necessary.
-- Do not move cursors.

-- (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.
-- Do not move cursors.

-- (From DS_SET)

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.
-- Do not move cursors.

-- (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.)
-- Resize set if necessary.
-- Do not move cursors.

-- (From DS_SET)

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 at the end of set if not already included,
-- or replace it otherwise.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Resize set if necessary.
-- Do not move cursors.

-- (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)
ensure then
last: (not old has (v)) implies last = v
force_new (v: G)

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

-- (From DS_SET)

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.)
-- Do not move cursors.

-- (From DS_SET)

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 at the end of set if not already included,
-- or replace it otherwise.
-- (Use equality_tester's comparison criterion
-- if not void, use = criterion otherwise.)
-- Do not move cursors.

-- (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)
ensure then
last: (not old has (v)) implies last = v
put_new (v: G)

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

-- (From DS_SET)

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 (k: G)

-- Remove item associated with k.
-- Move any cursors at this position forth.

-- (From DS_SET)

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)
remove_found_item

-- Remove item found by last call to search.
-- Move any cursors at this position forth.

-- (From DS_SPARSE_CONTAINER)

require
item_found: found
ensure
one_less: count = old count - 1
wipe_out

-- Remove all items from container.
-- Move all cursors off.

-- (From DS_CONTAINER)

ensure
wiped_out: is_empty

feature -- Resizing

resize (n: INTEGER)

-- Resize container so that it can contain
-- at least n items. Do not lose any item.
-- Do not move cursors.

-- (From DS_RESIZABLE)

require
n_large_enough: n >= capacity
ensure
capacity_set: capacity = n

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)

-- Copy other to current container.
-- Move all cursors off (unless other = Current).

-- (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.)
-- Move all cursors off.

-- (From DS_SET)

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.)
-- Do not move cursors.

-- (From DS_SET)

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.)
-- Move all cursors off.

-- (From DS_SET)

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.)
-- Move all cursors off.

-- (From DS_SET)

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

feature -- Search

search (v: G)

-- Search for item equal to v.
-- (Use equality_tester's comparison criterion
-- if not Void, use = criterion otherwise.)
-- If found, set found to true, and make that
-- item available in found_item.

-- (From DS_SPARSE_CONTAINER)

ensure then
found_set: found = has (v)
found_item_set: found implies (found_item = item (v))

feature -- Optimization

compress

-- Remove holes between stored items. May avoid
-- resizing when calling force_last for example.
-- Do not lose any item. Do not move cursors.

-- (From DS_SPARSE_CONTAINER)

ensure
same_count: count = old count
compressed: last_position = count
not_reszied: capacity = old capacity

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
after_position: INTEGER

-- Special values for before and after cursor positions

-- (From DS_SPARSE_CONTAINER)

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_back (a_cursor: like new_cursor)

-- Move a_cursor to previous position.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
a_cursor_not_before: not cursor_before (a_cursor)
cursor_before (a_cursor: like new_cursor): BOOLEAN

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

-- (From DS_BILINEAR)

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

-- Move a_cursor to last position.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
empty_behavior: is_empty implies cursor_before (a_cursor)
not_empty_behavior: not is_empty implies cursor_is_last (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_before (a_cursor: like new_cursor)

-- Move a_cursor to before position.

-- (From DS_BILINEAR)

require
a_cursor_not_void: a_cursor /= Void
a_cursor_valid: valid_cursor (a_cursor)
ensure
a_cursor_before: cursor_before (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_is_last (a_cursor: like new_cursor): BOOLEAN

-- Is a_cursor on last item?

-- (From DS_BILINEAR)

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) = last)
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_back (a_cursor: like new_cursor; v: G)

-- Move a_cursor to first position at or before 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 before if not found.

-- (From DS_BILINEAR)

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_before (a_cursor)
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

feature {DS_SPARSE_CONTAINER_CURSOR} -- Implementation

clashes_item (i: INTEGER): INTEGER

-- Item at position i in clashes

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
items_item (i: INTEGER): G

-- Item at position i in items

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
items_put (v: G; i: INTEGER)

-- Put v at position i in items.

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
ensure
inserted: items_item (i) = v
keys_item (i: INTEGER): G

-- Item at position i in keys

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
last_position: INTEGER

-- All slots to the right of this position
-- are guaranteed to be free

-- (From DS_SPARSE_CONTAINER)

valid_position (i: INTEGER): BOOLEAN

-- Is there a slot at position i?

-- (From DS_SPARSE_CONTAINER)

ensure
definition: Result = (1 <= i and i <= capacity)
valid_slot (i: INTEGER): BOOLEAN

-- Is there an item at position i?

-- (From DS_SPARSE_CONTAINER)

require
valid_i: valid_position (i)

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)

valid_position: position = No_position or else valid_position (position)
capacity_constraint: capacity < modulus

-- From DS_BILINEAR
not_both: initialized implies (not (after and before))
before_constraint: initialized implies (before implies off)

-- From DS_RESIZABLE
count_constraint: count <= capacity
full_definition: is_full = (count = capacity)

end