% $Id: XMLDocument.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
References
- XML Information Set
Working Draft of August 30, 1999
Editors: John Cowan, David Megginson
XMLDocument: trait
includes
XMLInfoSetBasics,
XMLEntity,
CoerceContainer(List[Item], FiniteSet[Item],
Item for E, asSet for coerce) %@@need to specify that insert on lists is precat
introduces
% 2.1. The Document Information Item
documentItem: InformationSet → Item % aka root in XSL???
notations: DocumentItem → FiniteSet[NotationItem]
entities: DocumentItem → FiniteSet[Item] %@@REVIEW: change this to
% a document entity plus properties of the DTD:
entity: DocumentItem → Item
% 2.4. Processing Instruction Information Items
target: PIItem → Name
content: PIItem → Value %@@REVIEW: sequence of characters? char items?
baseURI: PIItem → URI
%@@REVIEW: baseURI is redundant w.r.t. source
% 2.7. Comment Information Items
content: CommentItem → Value %@@REVIEW: sequence of character(item)?
% source
% 2.8. The Document Type Declaration Information Item
externalDTD: DTDItem → FiniteSet[Item] % "if any" → possibly null set
% children @@ including EntityItems
asserts
∀ d: Document,
is: InformationSet,
i, i1, i2: Item,
li, li1, li2: List[Item],
doci: DocumentItem,
dtdi: DTDItem
% 2.1. The Document Information Item
tag(documentItem(is)) = document;
% children of document are either PI, comment, element, or DTD:
tag(i1) = document
∧ i ∈ children(i1) ⇒ tag(i) = element
∨ tag(i) = pi
∨ tag(i) = comment
∨ tag(i) = dtd;
% list of children must contain exactly one element item
tag(i) = document ⇒ len(filter(children(i), element)) = 1;
% ... and at most one DTD info item @@REIVEW: 2.1.2 says "exactly one"
tag(i) = document ⇒ len(filter(children(i), dtd)) <= 1;
% no DTDs nor comments in the minimal infoset
len(filter(children(documentItem(infosetMin(d))), dtd)) = 0;
len(filter(children(documentItem(infosetMin(d))), comment)) = 0;
i ∈ entities(doci) ⇒ tag(i) = entity;
% if there's no DTD, the set of entities is just the document entity
i = documentItem(infosetMax(d))
∧ len(filter(children(i), dtd)) = 0
⇒ entities(i.document) = {entity(doci)};
% ... otherwise, it also includes the external subset etc.
% @@Hmm... need to model shadowing of entity names?
dtd(dtdi) ∈ children(document(doci))
⇒ entities(doci) = {entity(doci)}
∪ externalDTD(dtdi)
∪ asSet(filter(children(dtd(dtdi)), entity));
source(document(doci)) = entity(doci).entity;
% @@specification of required entities(iDoc) w.r.t. d:
% "one for each unparsed entity declaration in the DTD."
% @@REVIEW entities - other: why not parameter entities?
% 2.8. The Document Type Declaration Information Item
size(externalDTD(dtdi)) <= 1;
i ∈ externalDTD(dtdi) ⇒ tag(i) = entity;
tag(i1) = dtd
∧ i2 ∈ children(i1)
⇒ tag(i2) = pi
∨ tag(i2) = comment
∨ tag(i2) = entity %@@REVIEW: I added these; hmm... start/end markers?
∨ tag(i2) = notation;
[Index]
HTML generated using lsl2html.