Eiffeldoc: XML_DTD

Helps the parser to validate an XML file using a DTD

Direct parents: Inherit list: BACKTRACKING, XML_VALIDATOR; Insert list: RECYCLABLE, XML_DTD_MEMORY

Class invariant

not root_name.is_empty
current_continuation = Void or current_continuation = top_sequence
top_sequence = Void implies current_continuation = Void

Overview

Creation features

make (root_node_name: UNICODE_STRING)

Features

attributes: HASHED_DICTIONARY[UNICODE_STRING, UNICODE_STRING]
root: XML_DTD_NODE
point: XML_DTD_NODE
with_attribute (attribute_name: UNICODE_STRING, attribute_value: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

Called by the parser to add an attribute of a node BEFORE calling open_node
is_valid_open_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

When the parser reads an opening node
is_valid_close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

When the parser reads a closing node
is_valid_open_close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

When the parser reads a node that opens and closes immediately (syntax "<node/>")
current_node: UNICODE_STRING

The current node
open_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

When the parser reads an opening node
close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

When the parser reads a closing node
open_close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

When the parser reads a node that opens and closes immediately (syntax "<node/>")
entity (a_entity: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): UNICODE_STRING

When the parser reads an &entity;'.
entity_url (a_entity: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): UNICODE_STRING

When the parser reads an &entity;'.
is_valid_data (a_data: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

Called by the parser when the node contains raw data
data (a_data: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

Called by the parser when the node contains raw data
the_end

Called when the xml is totally parsed; usually it is used to recycle memory resources

Nodes management, for validation

{}

nodes_pool: RECYCLING_POOL[XML_DTD_NODE]
new_node (element: XML_DTD_ELEMENT, parent: XML_DTD_NODE): XML_DTD_NODE
free_node (a_node: XML_DTD_NODE)

Attributes string management

{}

clear_attributes

parse_done

Called when done parsing the DTD

<!ELEMENT . . .>

elements: HASHED_DICTIONARY[XML_DTD_ELEMENT, UNICODE_STRING]
current_element: XML_DTD_ELEMENT
element_built (element_name: UNICODE_STRING): BOOLEAN
adding_element (element_name: UNICODE_STRING): BOOLEAN
building_element: BOOLEAN
add_element (element_name: UNICODE_STRING)
commit_element (element_name: UNICODE_STRING)
close_fix
close_exactly_one
close_zero_or_one
close_zero_or_more
close_one_or_more
add_list
add_alt
child_pcdata
child_any
child_empty
child_one_or_more (node: UNICODE_STRING)
child_zero_or_more (node: UNICODE_STRING)
child_zero_or_one (node: UNICODE_STRING)
child_exactly_one (node: UNICODE_STRING)

{}

root_element: XML_DTD_ELEMENT
get_element (element_name: UNICODE_STRING): XML_DTD_ELEMENT
elements_pool: RECYCLING_POOL[XML_DTD_ELEMENT]

<!ATTLIST . . .>

attlist_element: XML_DTD_ELEMENT
building_attlist: BOOLEAN
has_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING): BOOLEAN
adding_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING): BOOLEAN
add_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING)
commit_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING)
addlist_list_value (value: UNICODE_STRING)
attlist_cdata
attlist_id
attlist_idref
attlist_idrefs
attlist_nmtoken
attlist_nmtokens
attlist_entity
attlist_entities
attlist_notation
attlist_required
attlist_implied
attlist_valid_fixed (value: UNICODE_STRING): BOOLEAN
attlist_fixed (value: UNICODE_STRING)
attlist_default_value (value: UNICODE_STRING)

<!ENTITY . . .>

entities: HASHED_DICTIONARY[UNICODE_STRING, UNICODE_STRING]
entity_urls: HASHED_DICTIONARY[UNICODE_STRING, UNICODE_STRING]
has_entity (entity_name: UNICODE_STRING): BOOLEAN
add_entity (entity_name: UNICODE_STRING, entity_value: UNICODE_STRING, entity__url: UNICODE_STRING)

backtrack_valid_data (a_children: FAST_ARRAY[XML_DTD_NODE], a_node: BACKTRACKING_NODE, a_data: UNICODE_STRING): BOOLEAN
backtrack_is_valid (a_children: FAST_ARRAY[XML_DTD_NODE], a_node: BACKTRACKING_NODE, a_next: UNICODE_STRING): BOOLEAN

backtrack_valid_child (elt: XML_DTD_ELEMENT)

{XML_DTD_PCDATA_NODE}

backtrack_valid_pcdata

{XML_DTD_ANY_NODE}

backtrack_valid_any

{XML_DTD_EMPTY_NODE}

backtrack_valid_empty

{XML_DTD_END_NODE}

backtrack_valid_end

Backtracking internals

{}

backtrack_pcdata: UNICODE_STRING
backtrack_children: FAST_ARRAY[XML_DTD_NODE]
backtrack_index: INTEGER_32
backtrack_ok: BOOLEAN
backtrack_next: UNICODE_STRING
context: FAST_ARRAY[INTEGER_32]
context_clear

Clear any saved context.
context_push

Push the current context.
context_restore

Restore the context to the last saved one.
context_restore_and_pop

Restore the context to the last saved one and drop it.
context_cut

Remove the last saved context.

{ABSTRACT_BACKTRACKING_SEQUENCE}

root_name: UNICODE_STRING
make (root_node_name: UNICODE_STRING)

{RECYCLING_POOL}

recycle

Do whatever needs to be done to free resources or recycle other objects when recycling this one

{}

recycle_elements
recycle_entity_urls
backtrack_next_pcdata_marker: UNICODE_STRING

{ANY}

set_current_node (node: BACKTRACKING_NODE)

Sets the next node of the BACKTRACKING_NODE graph to evaluate.
push_and (node: BACKTRACKING_NODE)

Pushes node in front of the continuation path.
push_and_list (list: BACKTRACKING_NODE_AND_LIST)

Pushes list in front of the continuation path.
push_or (node: BACKTRACKING_NODE)

Pushes node in front of the possible alternatives.
push_or_list (list: BACKTRACKING_NODE_OR_LIST)

Pushes list in front of the possible alternatives.

internal

{}

evaluate_current_state

That feature is called to evaluate the current state

Common client features

{ANY}

search_first

Resets all and searches the first solution.
search_next

Searches the next solution.
search_is_success: BOOLEAN

True when search is successful
is_off: BOOLEAN

True when search is finished
clear

Clears the current state to nothing.
is_cleared: BOOLEAN

True if no partial data remain in the current state

Control of the exploration

{ANY}

push_sequence (sequence: ABSTRACT_BACKTRACKING_SEQUENCE)

Pushes the sequence in front of the continuation path.
push_alternative (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

Pushes the alternative before the continuation path.
continue

Continues the exploration of the current path.
backtrack

Stops the exploration of the current path and tries to explore the next alternative path.
push_cut_point

Inserts a cut point into the continuation path.
cut

Removes the alternatives until the one recorded by the next cut point in the continuation path.
cut_all

Cuts all alternatives.

Internal

{}

stop_search_loop: BOOLEAN

True if at the end of a search.
search

Common search loop to search_first and search_next
cut_until (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

Cut all alternatives until 'alternative'.

Specific to sequences

top_sequence: ABSTRACT_BACKTRACKING_SEQUENCE

Stack of sequences represented by its top (can be Void)
current_continuation: ABSTRACT_BACKTRACKING_SEQUENCE

The current continuation path
pop_sequence

Removes the current sequence and replace it by the next sequence in the continuation path.

Specific to alternatives

{ABSTRACT_BACKTRACKING_ALTERNATIVE}

top_alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE

Stack of alternatives represented by its top (can be Void)
continue_alternative

Returns to the alternative on the top of the stack and put its saved continuation path as the current continuation path.
pop_alternative

Returns to the alternative on the top of the stack and put its saved continuation path as the current continuation path.

internal: allocation and collection

{}

remove_top_sequence

Removes the top sequence.
remove_top_alternative

Removes the top alternative.

{ANY}

pool_of_cut_points: ABSTRACT_BACKTRACKING_POOL_OF_CUT_POINT

Bank of cut points

the pools

{ANY}

Memory management

{}

dtd_validators_pool: RECYCLING_POOL[XML_DTD_VALIDATOR]
new_dtd_validator (root_node_name: UNICODE_STRING): XML_DTD_VALIDATOR
recycle_dtd_validator (a_validator: XML_DTD_VALIDATOR)
string_pool: RECYCLING_POOL[UNICODE_STRING]
new_empty_string: UNICODE_STRING
new_string (s: UNICODE_STRING): UNICODE_STRING
free_string (a_string: UNICODE_STRING)
url_pool: RECYCLING_POOL[URL]
buffer_pool: RECYCLING_POOL[UNICODE_PARSER_BUFFER]

attributes: HASHED_DICTIONARY[UNICODE_STRING, UNICODE_STRING]

writable attribute

root: XML_DTD_NODE

writable attribute

point: XML_DTD_NODE

writable attribute

with_attribute (attribute_name: UNICODE_STRING, attribute_value: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

effective procedure

Called by the parser to add an attribute of a node BEFORE calling open_node

require

not attribute_name.is_empty
not attribute_value.is_empty

is_valid_open_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

effective function

When the parser reads an opening node

require

not node_name.is_empty

is_valid_close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

effective function

When the parser reads a closing node

require

not node_name.is_empty
current_node.is_equal(node_name)

is_valid_open_close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

effective function

When the parser reads a node that opens and closes immediately (syntax "<node/>")

require

not node_name.is_empty

current_node: UNICODE_STRING

effective function

The current node

open_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

effective procedure

When the parser reads an opening node

require

is_valid_open_node(node_name, line, column)

ensure

current_node.is_equal(node_name)

close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

effective procedure

When the parser reads a closing node

require

is_valid_close_node(node_name, line, column)

open_close_node (node_name: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

effective procedure

When the parser reads a node that opens and closes immediately (syntax "<node/>")

require

is_valid_open_close_node(node_name, line, column)

entity (a_entity: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): UNICODE_STRING

effective function

When the parser reads an &entity;'.

entity_url (a_entity: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): UNICODE_STRING

effective function

When the parser reads an &entity;'.

Returns the entity URL if it is a SYSTEM entity.

is_valid_data (a_data: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32): BOOLEAN

effective function

Called by the parser when the node contains raw data

require

not a_data.is_empty

data (a_data: UNICODE_STRING, line: INTEGER_32, column: INTEGER_32)

effective procedure

Called by the parser when the node contains raw data

require

not a_data.is_empty

the_end

effective procedure

Called when the xml is totally parsed; usually it is used to recycle memory resources

nodes_pool: RECYCLING_POOL[XML_DTD_NODE]

once function

{}

new_node (element: XML_DTD_ELEMENT, parent: XML_DTD_NODE): XML_DTD_NODE

effective function

{}

ensure

Result.is_empty
Result.element = element
Result.parent = parent

free_node (a_node: XML_DTD_NODE)

effective procedure

{}

clear_attributes

effective procedure

{}

parse_done

effective procedure

Called when done parsing the DTD

elements: HASHED_DICTIONARY[XML_DTD_ELEMENT, UNICODE_STRING]

writable attribute

current_element: XML_DTD_ELEMENT

writable attribute

element_built (element_name: UNICODE_STRING): BOOLEAN

effective function

adding_element (element_name: UNICODE_STRING): BOOLEAN

effective function

ensure

Result implies not element_built(element_name)
Result implies building_element

building_element: BOOLEAN

effective function

add_element (element_name: UNICODE_STRING)

effective procedure

require

not element_built(element_name)
not building_element

ensure

adding_element(element_name)

commit_element (element_name: UNICODE_STRING)

effective procedure

require

adding_element(element_name)

ensure

element_built(element_name)
not building_element

close_fix

effective procedure

require

building_element

close_exactly_one

effective procedure

require

building_element

close_zero_or_one

effective procedure

require

building_element

close_zero_or_more

effective procedure

require

building_element

close_one_or_more

effective procedure

require

building_element

add_list

effective procedure

require

building_element

add_alt

effective procedure

require

building_element

child_pcdata

effective procedure

require

building_element

child_any

effective procedure

require

building_element

child_empty

effective procedure

require

building_element

child_one_or_more (node: UNICODE_STRING)

effective procedure

require

building_element

child_zero_or_more (node: UNICODE_STRING)

effective procedure

require

building_element

child_zero_or_one (node: UNICODE_STRING)

effective procedure

require

building_element

child_exactly_one (node: UNICODE_STRING)

effective procedure

require

building_element

root_element: XML_DTD_ELEMENT

effective function

{}

get_element (element_name: UNICODE_STRING): XML_DTD_ELEMENT

effective function

{}

ensure

Result.name.is_equal(element_name)

elements_pool: RECYCLING_POOL[XML_DTD_ELEMENT]

once function

{}

attlist_element: XML_DTD_ELEMENT

writable attribute

building_attlist: BOOLEAN

effective function

has_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING): BOOLEAN

effective function

ensure

Result implies building_attlist

adding_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING): BOOLEAN

effective function

ensure

Result implies building_attlist

add_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING)

effective procedure

require

element_built(element_name)
not building_element
not building_attlist

ensure

building_attlist

commit_attlist (element_name: UNICODE_STRING, attribute_name: UNICODE_STRING)

effective procedure

require

adding_attlist(element_name, attribute_name)

ensure

not building_attlist

addlist_list_value (value: UNICODE_STRING)

effective procedure

require

building_attlist

attlist_cdata

effective procedure

require

building_attlist

attlist_id

effective procedure

require

building_attlist

attlist_idref

effective procedure

require

building_attlist

attlist_idrefs

effective procedure

require

building_attlist

attlist_nmtoken

effective procedure

require

building_attlist

attlist_nmtokens

effective procedure

require

building_attlist

attlist_entity

effective procedure

require

building_attlist

attlist_entities

effective procedure

require

building_attlist

attlist_notation

effective procedure

require

building_attlist

attlist_required

effective procedure

require

building_attlist

attlist_implied

effective procedure

require

building_attlist

attlist_valid_fixed (value: UNICODE_STRING): BOOLEAN

effective function

require

building_attlist

attlist_fixed (value: UNICODE_STRING)

effective procedure

require

building_attlist
attlist_valid_fixed(value)

attlist_default_value (value: UNICODE_STRING)

effective procedure

require

building_attlist

entities: HASHED_DICTIONARY[UNICODE_STRING, UNICODE_STRING]

writable attribute

entity_urls: HASHED_DICTIONARY[UNICODE_STRING, UNICODE_STRING]

writable attribute

has_entity (entity_name: UNICODE_STRING): BOOLEAN

effective function

add_entity (entity_name: UNICODE_STRING, entity_value: UNICODE_STRING, entity__url: UNICODE_STRING)

effective procedure

require

not has_entity(entity_name)

ensure

has_entity(entity_name)
entity(entity_name, 0, 0) = entity_value
entity_url(entity_name, 0, 0) = entity__url

backtrack_valid_data (a_children: FAST_ARRAY[XML_DTD_NODE], a_node: BACKTRACKING_NODE, a_data: UNICODE_STRING): BOOLEAN

effective function

require

a_node /= Void

backtrack_is_valid (a_children: FAST_ARRAY[XML_DTD_NODE], a_node: BACKTRACKING_NODE, a_next: UNICODE_STRING): BOOLEAN

effective function

require

a_node /= Void

backtrack_valid_child (elt: XML_DTD_ELEMENT)

effective procedure

require

elt /= Void

backtrack_valid_pcdata

effective procedure

{XML_DTD_PCDATA_NODE}

backtrack_valid_any

effective procedure

{XML_DTD_ANY_NODE}

backtrack_valid_empty

effective procedure

{XML_DTD_EMPTY_NODE}

backtrack_valid_end

effective procedure

{XML_DTD_END_NODE}

backtrack_pcdata: UNICODE_STRING

writable attribute

{}

backtrack_children: FAST_ARRAY[XML_DTD_NODE]

writable attribute

{}

backtrack_index: INTEGER_32

writable attribute

{}

backtrack_ok: BOOLEAN

writable attribute

{}

backtrack_next: UNICODE_STRING

writable attribute

{}

context: FAST_ARRAY[INTEGER_32]

writable attribute

{}

context_clear

effective procedure

{}

Clear any saved context.

Called by the features clear and search_first.

context_push

effective procedure

{}

Push the current context.

Called each time that an alternative begins.

context_restore

effective procedure

{}

Restore the context to the last saved one.

The saved context MUST remain available for future use. Called each time that a new alternative (of the previous alternative point) is starting.

context_restore_and_pop

effective procedure

{}

Restore the context to the last saved one and drop it.

The saved context MUST be removed. Called each time that the last alternative (of the previous alternative point) is starting. Should be similar to context_restore followed by context_cut.

context_cut

effective procedure

{}

Remove the last saved context.

Called by cut, cut_all or cut_until.

root_name: UNICODE_STRING

writable attribute

make (root_node_name: UNICODE_STRING)

effective procedure

require

not root_node_name.is_empty

ensure

root_name = root_node_name

recycle

effective procedure

{RECYCLING_POOL}

Do whatever needs to be done to free resources or recycle other objects when recycling this one

recycle_elements

effective procedure

{}

ensure

elements.is_empty

recycle_entity_urls

effective procedure

{}

ensure

entity_urls.is_empty

backtrack_next_pcdata_marker: UNICODE_STRING

once function

{}

set_current_node (node: BACKTRACKING_NODE)

effective procedure

{ANY}

Sets the next node of the BACKTRACKING_NODE graph to evaluate.

ensure

definition: current_node = node

push_and (node: BACKTRACKING_NODE)

effective procedure

{ANY}

Pushes node in front of the continuation path.

require

node_not_void: node /= Void

push_and_list (list: BACKTRACKING_NODE_AND_LIST)

effective procedure

{ANY}

Pushes list in front of the continuation path.

require

list_not_void: list /= Void

push_or (node: BACKTRACKING_NODE)

effective procedure

{ANY}

Pushes node in front of the possible alternatives.

require

node_not_void: node /= Void

push_or_list (list: BACKTRACKING_NODE_OR_LIST)

effective procedure

{ANY}

Pushes list in front of the possible alternatives.

require

list_not_void: list /= Void

evaluate_current_state

effective procedure

{}

That feature is called to evaluate the current state

search_first

effective procedure

{ANY}

Resets all and searches the first solution.

The current state must be set. It is the first state, the root of the search. When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False, it means that there is no solution at all. Conversely, if search_is_success=True, then the first solution is found and 'search_next' can be called to get the next solution if it exists.

ensure

success_or_off: search_is_success and not is_off or is_off and not search_is_success

search_next

effective procedure

{ANY}

Searches the next solution.

When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False at the end, it means that there is no more solution. Conversely, if search_is_success=True, then a solution is found and 'search_next' can be called again to get the next solution.

require

last_search_was_a_success: search_is_success

ensure

success_or_off: search_is_success and not is_off or is_off and not search_is_success

search_is_success: BOOLEAN

writable attribute

{ANY}

True when search is successful

is_off: BOOLEAN

effective function

{ANY}

True when search is finished

ensure

definition: Result = not search_is_success

clear

effective procedure

{ANY}

Clears the current state to nothing.

ensure

cleared: is_cleared
no_solution: is_off

is_cleared: BOOLEAN

effective function

{ANY}

True if no partial data remain in the current state

ensure

no_solution_when_cleared: Result implies is_off

push_sequence (sequence: ABSTRACT_BACKTRACKING_SEQUENCE)

effective procedure

{ANY}

Pushes the sequence in front of the continuation path.

require

sequence_not_void: sequence /= Void

ensure

is_on_top: top_sequence = sequence
is_first_continuation: current_continuation = sequence
previous_top_linked: top_sequence.previous = old top_sequence
previous_continuation_linked: top_sequence.continuation = old current_continuation

push_alternative (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

effective procedure

{ANY}

Pushes the alternative before the continuation path.

require

alternative_not_void: alternative /= Void

ensure

is_on_top: top_alternative = alternative
previous_top_linked: top_alternative.previous = old top_alternative
top_sequence_recorded: top_alternative.top_sequence = old top_sequence
continuation_recorded: top_alternative.continuation = old current_continuation

continue

effective procedure

{ANY}

Continues the exploration of the current path.

backtrack

effective procedure

{ANY}

Stops the exploration of the current path and tries to explore the next alternative path.

push_cut_point

effective procedure

{ANY}

Inserts a cut point into the continuation path.

The inserted cut point records the current top of the alternatives.

cut

effective procedure

{ANY}

Removes the alternatives until the one recorded by the next cut point in the continuation path.

cut_all

effective procedure

{ANY}

Cuts all alternatives.

stop_search_loop: BOOLEAN

writable attribute

{}

True if at the end of a search.

This occurs if either a solution is found (and then search_is_success=True) or no solution is found (and then search_is_success=False). That feature should be modified only by continue and backtrack.

effective procedure

{}