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

em.highscore

Class EM_HIGHSCORE_ENTRY


Direct ancestors

DS_HASH_TABLE

Creation

Features

Invariants

indexing

description

A highscore entry consists of a name, a score and possibly
other keys, which are accessible through a hash table.

date

$Date: 2005/10/26 15:41:47 $

revision

$Revision: 1.9 $

class

EM_HIGHSCORE_ENTRY

Inherit

DS_HASH_TABLE

create

make_default

-- Create an empty table and allocate memory
-- space for at least default_capacity items.
-- Use = as comparison criterion for items.
-- Use equal as comparison criterion for keys.

-- (From DS_CONTAINER)

ensure
empty: is_empty
ensure then
before: before
make (n: INTEGER)

-- Create an empty table and allocate
-- memory space for at least n items.
-- Use = as comparison criterion for items.
-- Use equal as comparison criterion for keys.

-- (From DS_SPARSE_TABLE)

require
positive_n: n >= 0
ensure
empty: is_empty
capacity_set: capacity = n
before: before

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
special_any_: KL_SPECIAL_ROUTINES [ANY]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_any_routines_not_void: Result /= Void
special_boolean_: KL_SPECIAL_ROUTINES [BOOLEAN]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_boolean_routines_not_void: Result /= Void
special_character_: KL_SPECIAL_ROUTINES [CHARACTER]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_character_routines_not_void: Result /= Void
special_integer_: KL_SPECIAL_ROUTINES [INTEGER]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_integer_routines_not_void: Result /= Void
special_string_: KL_SPECIAL_ROUTINES [STRING]

-- Routines that ought to be in class SPECIAL

-- (From KL_IMPORTED_SPECIAL_ROUTINES)

ensure
special_string_routines_not_void: Result /= Void
equality_tester: KL_EQUALITY_TESTER [STRING]

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

-- (From DS_SEARCHABLE)

first: STRING

-- First item in container

-- (From DS_LINEAR)

require
not_empty: not is_empty
ensure
has_first: has (Result)
found_item: STRING

-- Item found by last call to search

-- (From DS_SPARSE_CONTAINER)

require
item_found: found
found_key: STRING

-- Key of item found by last call to search

-- (From DS_SPARSE_TABLE)

require
key_found: found
infix "@" (k: STRING): STRING

-- Item associated with k

-- (From DS_TABLE)

require
has_k: has (k)
item (k: STRING): STRING

-- Item associated with k

-- (From DS_TABLE)

require
has_k: has (k)
item_for_iteration: STRING

-- Item at internal cursor position

-- (From DS_TRAVERSABLE)

require
not_off: not off
key (k: STRING): STRING

-- Key associated with k

-- (From DS_SPARSE_TABLE)

require
has_k: has (k)
key_equality_tester: KL_EQUALITY_TESTER [STRING]

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

-- (From DS_SPARSE_CONTAINER)

key_for_iteration: STRING

-- Key at internal cursor position

-- (From DS_SPARSE_TABLE)

require
not_off: not off
last: STRING

-- Last item in container

-- (From DS_BILINEAR)

require
not_empty: not is_empty
ensure
has_last: has (Result)
name: STRING

-- user's name

new_cursor: DS_HASH_TABLE_CURSOR [STRING, STRING]

-- New external cursor for traversal

-- (From DS_TRAVERSABLE)

ensure
cursor_not_void: Result /= Void
valid_cursor: valid_cursor (Result)
score: INTEGER

-- user's score

value (k: STRING): STRING

-- Item associated with k;
-- Return default value if no such item

-- (From KL_VALUES)

require
k_not_void: k /= Void
require else
True

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: STRING): INTEGER

-- Number of times v appears in container
-- (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

feature -- Comparison

is_equal (other: like Current): BOOLEAN

-- Is table equal to other?
-- Do not take cursor positions, capacity
-- nor equality_tester into account.

-- (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?
-- (Default answer: True.)

-- (From DS_SEARCHABLE)

found: BOOLEAN

-- Did last call to search succeed?

-- (From DS_SPARSE_CONTAINER)

ensure
definition: Result = (found_position /= No_position)
has (k: STRING): BOOLEAN

-- Is there an item associated with k?

-- (From DS_TABLE)

ensure
valid_key: Result implies valid_key (k)
has_item (v: STRING): 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_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)
key_equality_tester_settable (a_tester: like key_equality_tester): BOOLEAN

-- Can set_key_equality_tester be called with a_tester
-- as argument in current state of container?

-- (From DS_SPARSE_TABLE)

off: BOOLEAN

-- Is there no item at internal cursor position?

-- (From DS_TRAVERSABLE)

same_equality_tester (other: DS_SEARCHABLE [STRING]): BOOLEAN

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

-- (From DS_SEARCHABLE)

require
other_not_void: other /= Void
same_items (v, u: STRING): 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 [STRING]): BOOLEAN

-- Is a_cursor a valid cursor?

-- (From DS_TRAVERSABLE)

require
a_cursor_not_void: a_cursor /= Void
valid_key (k: STRING): BOOLEAN

-- Is k a valid key?

-- (From DS_TABLE)

ensure then
defintion: Result = True

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: STRING)

-- 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: STRING)

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

force (v: STRINGk: STRING)

-- Associate v with key k.
-- Resize table if necessary.
-- Do not move cursors.

-- (From DS_TABLE)

require
valid_key: valid_key (k)
ensure
inserted: has (k) and then item (k) = v
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
force_last (v: STRINGk: STRING)

-- Associate v with key k. Put v at the end of table
-- if no item was already associated with k, or replace
-- existing item otherwise.
-- Resize table if necessary.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

ensure
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
inserted: has (k) and then item (k) = v
last: (not old has (k)) implies last = v
force_new (v: STRINGk: STRING)

-- Associate v with key k.
-- Resize table if necessary.
-- Do not move cursors.

-- (From DS_TABLE)

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

-- Associate v with key k.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
not_full: not is_full
ensure
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
inserted: has (k) and then item (k) = v
put_last (v: STRINGk: STRING)

-- Associate v with key k. Put v at the end of table
-- if no item was already associated with k, or replace
-- existing item otherwise.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
not_full: not is_full
ensure
same_count: (old has (k)) implies (count = old count)
one_more: (not old has (k)) implies (count = old count + 1)
inserted: has (k) and then item (k) = v
last: (not old has (k)) implies last = v
put_new (v: STRINGk: STRING)

-- Associate v with key k.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
not_full: not is_full
new_item: not has (k)
ensure
one_more: count = old count + 1
inserted: has (k) and then item (k) = v
replace (v: STRINGk: STRING)

-- Replace item associated with k by v.
-- Do not move cursors.

-- (From DS_TABLE)

require
has_k: has (k)
ensure
replaced: item (k) = v
same_count: count = old count
replace_found_item (v: STRING)

-- Replace item associated with
-- the key of found_item by v.
-- Do not move cursors.

-- (From DS_SPARSE_TABLE)

require
item_found: found
ensure
replaced: found_item = v
same_count: count = old count
set_name (a_name: like name)

-- Set name to a_name.

ensure
name_assigned: name = a_name
set_score (a_score: like score)

-- Set score to a_score.

ensure
score_assigned: score = a_score
swap (k, l: STRING)

-- Exchange items associated with k and l.

-- (From DS_TABLE)

require
valid_k: has (k)
valid_l: has (l)
ensure
same_count: count = old count
new_k: item (k) = old item (l)
new_l: item (l) = old item (k)

feature -- Removal

remove (k: STRING)

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

-- (From DS_TABLE)

require
valid_key: valid_key (k)
ensure
same_count: (not old has (k)) implies (count = old count)
one_less: (old has (k)) implies (count = old count - 1)
removed: not has (k)
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 [STRING]

-- 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 -- 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
set_key_equality_tester (a_tester: like key_equality_tester)

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

-- (From DS_SPARSE_TABLE)

require
key_equality_tester_settable: key_equality_tester_settable (a_tester)
ensure
key_equality_tester_set: key_equality_tester = a_tester

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 -- Search

search (k: STRING)

-- Search for item at key k.
-- If found, set found to true, and set
-- found_item to item associated with k.

-- (From DS_SPARSE_CONTAINER)

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

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): STRING

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

-- Key at a_cursor position

-- (From DS_SPARSE_TABLE)

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_cursorv: STRING)

-- 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_cursorv: STRING)

-- 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 -- Compare

less_than (other: like Current; a_key: STRING): BOOLEAN

-- Is this entry less than the other? (when sorted with 'a_key')
-- Sort integers non-alphanumerically

require
other /= voidhas (a_key)other.has (a_key)

feature {DS_ARRAYED_SPARSE_TABLE_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): STRING

-- Item at position i in items

-- (From DS_SPARSE_CONTAINER)

require
i_large_enough: i >= 1
i_small_enough: i <= capacity
items_put (v: STRINGi: 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): STRING

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


items_not_void: items /= Void
items_count: items.count = capacity + 1
keys_not_void: keys /= Void
keys_count: keys.count = capacity + 1
clashes_not_void: clashes /= Void
clashes_count: clashes.count = capacity + 1
slots_not_void: slots /= Void
slots_count: slots.count = modulus + 1

-- 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_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_RESIZABLE
count_constraint: count <= capacity
full_definition: is_full = (count = capacity)

end