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

xml.tree

Class XM_NAMESPACE_TABLE


Direct ancestors

DS_HASH_TABLE, XM_UNICODE_STRUCTURE_FACTORY, XM_MARKUP_CONSTANTS

Creation

Features

Invariants

indexing

description

Mappings between namespace prefixes and namespace URIs

library

Gobo Eiffel XML Library

copyright

Copyright (c) 2001, Andreas Leitner and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 19:49:04 $

revision

$Revision: 1.14 $

class

XM_NAMESPACE_TABLE

inherit

DS_HASH_TABLE

create

make

-- Create a new empty namespace table.

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

-- Default namespace

require
has_default: has_default
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)
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)
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_default: BOOLEAN

-- Has table a default namespace?
-- (Note: in any given table there must be at most one
-- default namespace)

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
override_with_list (l: DS_BILINEAR [XM_NAMESPACE])

-- Add namespace declarations listed in l.
-- If l has an entry with a prefix that is already
-- in current table, override it with the entry from
-- the list.

require
l_not_void: l /= Void
no_void_namespace: not l.has (Void)
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
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 {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