% $Id: XMLElement.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%

References

  1. XML Information Set
    Working Draft of August 30, 1999
    Editors: John Cowan, David Megginson

XMLElement: trait
    includes
        XMLInfoSetBasics,
        XMLDocument,
        XMLEntity,

        Set(AttributeItem, FiniteSet[AttributeItem] for Set[E])

% 2.3 Attribute Items
        AttributeType enumeration of ID, IDREF, IDREFS, ENTITY,
                                     ENTITIES, NMTOKEN, NMTOKENS, NOTATION,
                                     CDATA, ENUMERATED

    introduces
% 2.2. Element Information Items
        name: ElementItem → Name
        attributes: ElementItem → FiniteSet[AttributeItem] %@@REVIEW: bogus:
% "Namespace declarations are not represented
% as attribute information items."
% check against DOM 1.0 etc.

        baseURI: ElementItem → absoluteURI
        eStack: List[Item] → List[EntityItem]
        externals: List[EntityItem] → List[EntityItem]

% 2.3. Attribute Information Items
        name: AttributeItem → Name
        specified: AttributeItem → Bool

        default: AttributeItem → Value %@@REVIEW default is what?
% sequence of char?
        type: AttributeItem → AttributeType


% 2.5. Reference to Skipped Entity Information Items
        name: RSEItem → Name
        referent: RSEItem → Entity %@@REVIEW: huh? (example/max)


% 2.6. Character Information Items
        code: CharacterItem → Int

        elementContentWhitespace: CharacterItem → Bool
        predefinedEntity: CharacterItem → Bool %@@REVIEW: "included"???
% source

    asserts
        ∀ d: Document,
                i, i1, i2: Item,
                li, li1, li2: List[Item],
                elti: ElementItem,
                ei: EntityItem, eli: List[EntityItem],
                ai: AttributeItem, sai: FiniteSet[AttributeItem]


% 2.2. Element Information Items
        tag(i1) = element
        ∧ i ∈ children(i1) ⇒ tag(i) = element
                                 ∨ tag(i) = pi
                                 ∨ tag(i) = rse
                                 ∨ tag(i) = comment
                                 ∨ tag(i) = entityStart
                                 ∨ tag(i) = entityEnd;

% comments, entity start/end markers are optional
        tag(i) = element
        ∧ (i \< descendant \> documentItem(infosetMin(d)))
        ⇒ len(filter(children(i), comment)) = 0
           ∧ len(filter(children(i), entityStart)) = 0
           ∧ len(filter(children(i), entityEnd)) = 0;

% If an entity start marker is present, the
% corresponding entity end marker must also be present ...
        tag(i) = element
        ∧ tag(i1) = entityStart
        ⇒ entityEnd(end(i1.entityStart)) ∈ children(i);
% ... and vice versa
        tag(i) = element
        ∧ tag(i1) = entityEnd
        ⇒ entityStart(start(i1.entityEnd)) ∈ children(i);

%@@specify that no two attributes have the same name?

% The absolute URI of the external entity in which
% this element appears.
        tag(i) = element
        ⇒ baseURI(i.element) = systemIdentifier(source(i));
%@@REVIEW: s/absolute URI of external/system identifer of external/
%@@REVIEW: note that this is unspecified in the case of a document
% with no URI, e.g. stdin

% A reference to the entity information item for the entity
% in which this element begins and ends.
% Note we only specify this for the maximal infoset case.@@
        i ∈ flatten({documentItem(infosetMax(d))})
        ∧ children(i) = li1 || {i1} || li2
        ⇒ source(i1) = (if externals(eStack(li1)) = empty
                         then source(i)
                         else head(externals(eStack(li1))));

        eStack(empty) = empty;
        eStack(li |- i)= (if (tag(i) = entityStart)
                             then entity(i.entityStart) -| eStack(li)
                             else if tag(i) = entityEnd
                             then tail(eStack(li))
                             else eStack(li));
        externals(empty) = empty;
        externals(ei -| eli) = (if type(ei).external
                                    then ei -| externals(eli)
                                    else externals(eli));


% 2.3. Attribute Information Items
        tag(i1) = attribute
        ∧ i ∈ children(i1) ⇒ tag(i) = char
                                 ∨ tag(i) = entityStart
                                 ∨ tag(i) = entityEnd;

% markers are optional
        tag(i1) = element
        ∧ (i1 \< descendant \> documentItem(infosetMin(d)))
        ∧ tag(i2) = attribute
        ∧ i2.attribute ∈ attributes(i1.element)
        ⇒ len(filter(children(i2), entityStart)) = 0
           ∧ len(filter(children(i2), entityEnd)) = 0;


        ai ∈ attributes(elti)
        ⇒ source(attribute(ai)) = source(element(elti));

[Index]

HTML generated using lsl2html.