XMLDocument

% $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.