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

structure.table

Class DS_TABLE


Direct ancestors

DS_CONTAINER, KL_VALUES

Known direct descendants

DS_SPARSE_TABLE

Features

Invariants

indexing

description

Data structures whose items are accessible through keys

library

Gobo Eiffel Structure Library

copyright

Copyright (c) 2000-2004, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2004/04/18 17:17:54 $

revision

$Revision: 1.9 $

deferred class

DS_TABLE [G, K]

inherit

DS_CONTAINER
KL_VALUES

feature -- Access

infix "@" (k: K): G

-- Item associated with k

require
has_k: has (k)
item (k: K): G

-- Item associated with k

require
has_k: has (k)
value (k: K): G

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

count: INTEGER

-- Number of items in container

-- (From DS_CONTAINER)

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

has (k: K): BOOLEAN

-- Is there an item associated with k?

ensure
valid_key: Result implies valid_key (k)
is_empty: BOOLEAN

-- Is container empty?

-- (From DS_CONTAINER)

valid_key (k: K): BOOLEAN

-- Is k a valid key?

feature -- Element change

put (v: G; k: K)

-- Associate v with key k.

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)
put_new (v: G; k: K)

-- Associate v with key k.

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
replace (v: G; k: K)

-- Replace item associated with k by v.

require
has_k: has (k)
ensure
replaced: item (k) = v
same_count: count = old count
swap (k, l: K)

-- Exchange items associated with k and l.

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

-- Remove item associated with k.

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

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