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

structure.container

Class DS_INDEXABLE


Direct ancestors

DS_SORTABLE, DS_EXTENDIBLE

Known direct descendants

DS_LIST

Features

Invariants

indexing

description

Data structures that can be traversed and %
%modified through integer access

library

Gobo Eiffel Structure Library

copyright

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

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2003/02/07 12:58:08 $

revision

$Revision: 1.6 $

deferred class

DS_INDEXABLE [G]

inherit

DS_SORTABLE
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

require
not_empty: not is_empty
ensure
definition: Result = item (1)
infix "@" (i: INTEGER): G

-- Item at index i

require
valid_index: 1 <= i and i <= count
item (i: INTEGER): G

-- Item at index i

require
valid_index: 1 <= i and i <= count
last: G

-- Last item in container

require
not_empty: not is_empty
ensure
definition: Result = item (count)

feature -- Measurement

count: INTEGER

-- Number of items in container

-- (From DS_CONTAINER)

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

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)

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

-- Is container empty?

-- (From DS_CONTAINER)

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)

sorted (a_sorter: DS_SORTER [G]): BOOLEAN

-- Is container sorted according to a_sorter's criterion?

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void

feature -- Element change

append (other: DS_LINEAR [G]; i: INTEGER)

-- Add items of other at i-th position.
-- Keep items of other in the same order.

require
other_not_void: other /= Void
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
append_first (other: DS_LINEAR [G])

-- Add items of other to beginning of container.
-- Keep items of other in the same order.

require
other_not_void: other /= Void
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
append_last (other: DS_LINEAR [G])

-- Add items of other to end of container.
-- Keep items of other in the same order.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
extend (other: DS_LINEAR [G]; i: INTEGER)

-- Add items of other at i-th position.
-- Keep items of other in the same order.

require
other_not_void: other /= Void
extendible: extendible (other.count)
valid_index: 1 <= i and i <= (count + 1)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (i) = other.first)
extend_first (other: DS_LINEAR [G])

-- Add items of other to beginning of container.
-- Keep items of other in the same order.

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (first = other.first)
extend_last (other: DS_LINEAR [G])

-- Add items of other to end of container.
-- Keep items of other in the same order.

-- (From DS_EXTENDIBLE)

require
other_not_void: other /= Void
extendible: extendible (other.count)
ensure then
new_count: count = old count + other.count
same_order: (not other.is_empty) implies (item (old count + 1) = other.first)
force (v: G; i: INTEGER)

-- Add v at i-th position.

require
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
force_first (v: G)

-- Add v to beginning of container.

ensure
one_more: count = old count + 1
inserted: first = v
force_last (v: G)

-- Add v to end of container.

-- (From DS_EXTENDIBLE)

ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
put (v: G; i: INTEGER)

-- Add v at i-th position.

require
extendible: extendible (1)
valid_index: 1 <= i and i <= (count + 1)
ensure
one_more: count = old count + 1
inserted: item (i) = v
put_first (v: G)

-- Add v to beginning of container.

require
extendible: extendible (1)
ensure
one_more: count = old count + 1
inserted: first = v
put_last (v: G)

-- Add v to end of container.

-- (From DS_EXTENDIBLE)

require
extendible: extendible (1)
ensure
added: has (v)
ensure then
one_more: count = old count + 1
inserted: last = v
replace (v: G; i: INTEGER)

-- Replace item at i-th position by v.

require
valid_index: 1 <= i and i <= count
ensure
same_count: count = old count
replaced: item (i) = v
swap (i, j: INTEGER)

-- Exchange items at indexes i and j.

require
valid_i: 1 <= i and i <= count
valid_j: 1 <= j and j <= count
ensure
same_count: count = old count
new_i: item (i) = old item (j)
new_j: item (j) = old item (i)

feature -- Removal

keep_first (n: INTEGER)

-- Keep n first items in container.

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
keep_last (n: INTEGER)

-- Keep n last items in container.

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = n
prune (n: INTEGER; i: INTEGER)

-- Remove n items at and after i-th position.

require
valid_index: 1 <= i and i <= count
valid_n: 0 <= n and n <= (count - i + 1)
ensure
new_count: count = old count - n
prune_first (n: INTEGER)

-- Remove n first items from container.

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
prune_last (n: INTEGER)

-- Remove n last items from container.

require
valid_n: 0 <= n and n <= count
ensure
new_count: count = old count - n
remove (i: INTEGER)

-- Remove item at i-th position.

require
not_empty: not is_empty
valid_index: 1 <= i and i <= count
ensure
one_less: count = old count - 1
remove_first

-- Remove first item from container.

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
remove_last

-- Remove last item from container.

require
not_empty: not is_empty
ensure
one_less: count = old count - 1
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)

feature -- Sort

sort (a_sorter: DS_SORTER [G])

-- Sort container using a_sorter's algorithm.

-- (From DS_SORTABLE)

require
a_sorter_not_void: a_sorter /= Void
ensure
sorted: sorted (a_sorter)

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