XML Schema: Formal Description

Abstract

XML Schema: Formal Description is a formal description of XML types and validity as specified by XML Schema Part 1: Structures.

Status of this document

This is a W3C Working Draft for review by members of the W3C and other interested parties in the general public.

It has been reviewed by the XML Schema Working Group and the Working Group has agreed to its publication. Note that not that all sections of the draft represent the current consensus of the WG. Different sections of the specification may well command different levels of consensus in the WG. Public comments on this draft will be instrumental in the WG's deliberations.

Please review and send comments to www-xml-schema-comments@w3.org (archive).

This specification of the formal description of XML Schema is a working draft of the XML Schema Working Group and has been adopted by the working group as the formalization of the XML Schema Definition Language, in fulfillment of its commitment to provide such a formalization at the conclusion of the Candidate Recommendation phase for XML Schema. This material is current with the Proposed Recommendation draft but not perfectly aligned with it. In the foreseeable future, work on this document will focus on improving the alignment with the normative parts of XML Schema and resolving the issues on the current issues list (http://www.w3.org/2001/03/xmlschema-fd-issues.html).

As with all working drafts, the reader is advised that all the material within is subject to change. The reader is advised that material found here may change drastically from draft to draft. In particular, future versions will incorporate some or all of the XML Schema Part 2: Datatypes specification, the key/keyref facility, and a bidirectional mapping between the XML Schema component model and the corresponding part of this formalization. Parts of this specification, such as the normalization of names, may eventually find a broader use. However the reader should be advised that these features will probably undergo revision before the working group warrants them for such uses.

The Schema Working Group expects this work to be of use to other Working Groups within the W3C as well as to others building tools and systems hoping to leverage XML Schemas.

A list of current W3C working drafts can be found at http://www.w3.org/TR/. They may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use W3C Working Drafts as reference material or to cite them as other than "work in progress".

Table of contents

1 Introduction

2 Overview
  2.1 Normalization
  2.2 Components
  2.3 Documents and Forests

3 Structures
  3.1 Names
  3.2 Wildcards
  3.3 Atomic datatypes
  3.4 Content groups
  3.5 Components
  3.6 Constraints
  3.7 Ordered Forests
  3.8 Inference rules

4 Normalization

5 Derivation
  5.1 Base chain
  5.2 Extension
  5.3 Restriction
  5.4 Constraints

6 Validation
  6.1 Content validation
  6.2 ID/IDREF validation

7 XML Schema to Formalization Mapping
  7.1 Conversions for content model particles
  7.2 Correspondences from XML Schema to sorts

8 Index of notations

Appendix A Infidelities in the current formalization of XML Schema

Appendix BBibliography

1  Introduction

This formalization is a formal, declarative system for describing and naming XML Schema information, specifying XML instance type information, and validating instances against schemas. The goals of the formalization are to:

• Provide a semantic framework for software systems that use the W3C XML Schema specification, such as the W3C XML Query Algebra.
• Specify names for all components of an XML Schema, so that they can be uniquely identified by URIs. Such unique identifiers may be useful to XML Query, RDF, and topic maps, among others.
• Formally define validation at a declarative level.
• Define the mapping from the current XML Schema syntax onto the structures described here, as well as the mapping between the XML Schema component mode and our component model.

Many potential applications of XML Schema may benefit from the definition of a formal model. We have focused on the material in Part I (Structures), as this is the most complex.

A basic understanding of first-order predicate logic, which is part of most computer science curricula, is adequate to understand this document. Where other notations are used, they are explained before use. Though the mathematical notation used in this formalization may be somewhat daunting for those not accustomed to formalisms, it should be possible to prepare a prose description directly from this formalism, which may be more approachable than a description based on an ad hoc understanding of XML Schema [11,3].

The approach followed here follows the best practices currently used in the programming languages community, although somewhat adapted for XML.  The hallmark of this approach is the use of context free grammars to provide syntactic checking and the use of inference rules to provide the semantics associated with each piece of syntax.  This means there is, essentially, one inference rule per context free grammar production.   This set of inference rules is not intended to be in any way minimal, but it is helpful from both a pedagogical and implementation standpoint - for each syntactic construct it is straightforward to identify its underlying semantics.

The remainder of this document is organized as follows.

• Section 2 gives an overview of the formalism.
• Section 3 defines the basic structures used in the formalization including names, groups, and components.
• Section 4 describes normalization.
• Section 5 describes refinement.
• Section 6 describes validation.
• Section 7 describes the mapping from the XML Schema concrete syntax into our structures. (A mapping from XML Schema components to these components will appear in a later draft.)
• Section 8 indexes the notations used.
• Appendix A lists lacunae in the current articulation of the formalism relative to XML Schema

2  Overview

This section uses a running example to introduce our representation of a schema, which uses a mathematical notation that is easier to manipulate formally than the XML syntax of Schema. This formalism divides a schema into a set of components, where each component can match against a particular fragment of XML in an instance.  Particular attention will be given to the use of normalization to provide a unique name for each component of a schema.

Here is a sample schema written in W3C XML Schema syntax. 

<xsi:schema targetns = "http://www.example.com/baz.xsd"
    xmlns = "http://www.example.com/baz.xsd"
    xmlns:xsi = "http://www.w3.org/2001/XMLSchema">
  <xsi:element name="a" type="t"/>
  <xsi:simpleType name="b"/>
    <xsi:list base="xsi:integer"/>
  </xsi:simpleType>
  <xsi:complexType name="t">
    <xsi:attribute name="b" type="xsi:string"/>
    <xsi:attribute name="c" type="b" use="optional"/>
  </xsi:complexType>
  <xsi:complexType name="u">
    <xsi:complexContent>
      <xsi:extension base="t">
        <xsi:choice>
          <xsi:element name="d">
            <xsi:complexType>
              <xsi:sequence>
                <xsi:element name="a"
                    type="xsi:string"
                    minOccurs="1"
                    maxOccurs="unbounded"/>

              </xsi:sequence>
            </xsi:complexType>
          </xsi:element>
          <xsi:element name="e" type="xsi:string"/>
        </xsi:choice>
      </extension>
    </complexContent>
  </xsi:complexType>
</xsi:schema> 

And here is an XML document which matches the above schema

<baz:a xmlns:baz="http://www.example.com/baz.xsd"
    xsi:type="baz:u"
    b="zero"
    c="1 2">
  <d>
    <a>three</a>
    <a>four</a>
  </d>
</baz:a> 

2.1  Normalization

We use a normalized form of a schema, which assigns a unique universal name to each component of a schema, and "flattens" the structure. (A component is anything which may be defined or declared: an element, an attribute, a simple type, a complex type, a group, an attribute group, or an identity constraint.)

Here are the normalized (universal) names of the components in our sample schema. For each name, we list two forms: the long form is the name proper, while the short form is an abbreviated version we use in examples to improve readability.

The normalized names reflect the nesting structure of the original schema. Note that the nesting of declarations in W3C XML Schema also determines their scope. In the representation of a Schema, the names of nested components are constructed by appending their schema names to the normalized names of their parents; if a component is anonymous, it is given the name *. The syntax of names is chosen to be similar to XPath [5,12], but unlike XPath, * does not function as a wildcard in normalized names.

These normalized names clearly distinguish local names from global names. Where previously it might be possible to confuse the global a element with the local a element, now these are given distinct names, a and u/d/*/a respectively. The latter indicates that the global type u contains a local element d which contain an anonymous type * which contains a local element a. Each attribute or element contains at most one anonymous type, so using the name * for such types leads to no confusion.

2.2  Components

Next, we show how components are represented in this notation. Each component is one of six sorts: element, attribute, simple type, complex type, attribute group, or model group. Regardless of sort, each component is represented uniformly as a constructor (one of attribute, element, simpleType, complexType, attributeGroup, modelGroup, or identityConstraint) of a record with six fields:

name

is the name of the component;

base

is the name of the base component of the structure;

derivation

specifies how the component is derived from the base,
it is one of restriction or extension;

refinement

is the set of permitted derivations from this component as base,
it is a subset of {restriction, extension};

abstract

is a boolean, representing whether this type is abstract;

content

is the content of the component, describing the instance information which can match this component, following the context free grammar below.

Note that all seven sorts have a very consistent structure consisting of six properties, which have the same interpretation regardless of the sort.

2.2.1  Component content

The formalism uses standard regular expression notation [2] for component content.   Component content corresponds roughly to a union of both model groups and attributes groups.  In what follows, g stands for a content group (as does g₁, g₂, and so on). The constructors for groups include the following:

ε       

empty sequence

Ø       

empty choice

g₁,g₂    

sequence, g₁ followed by g₂

g₁ | g₂    

choice, g₁ or g₂

g₁ & g₂  

all, g₁ and g₂ in either order

g{m,n}

repetition, g repeated between minimum m and maximum n times   (m is a natural number, n is a natural number or ∞)

mixed(g)   

mixed content in group g

a[g]   

attribute, with name a and content in group g

e[g]   

element, with name e and content in group g

w           

wildcard, with name in wildcard w

p           

atomic datatype (such as xsi:string or xsi:integer)

t             

complex type name

x           

component name 

EDITOR'S NOTE: The grammar above does not distinguish between the precedence of the various connectors ("|", "&", and ","). This will not be a concern as in our examples we will always parenthesize appropriately. Rather than significantly expanding the grammar, we will provide a full grammar with parentheses in an appendix in a future version.

Here is an example of a group in our notation, which corresponds to an a element with content of type u in our running example

a[
    (t/@b[xsi:string] & t/@c[xsi:integer{0,∞}]{0,1}),
    (u/d[u/d/*/a[xsi:string]{1,∞}] | u/d/*/e[xsi:string])
] 

Note that the group constructors are used uniformly in several contexts. Repetition (g{m,n}) is used for lists of atomic datatypes, to indicate whether an attribute is optional, and for elements. Similarly, all (g₁ & g₂) is used for attributes and for elements.

2.2.2 Example Schema Components

Here are the components of the normalized schema represented in this notation

element(
  name = a,
  base = xsi:UrElement,
  derivation = restriction,
  refinement = {restriction,extension},
  abstract = false,
  content = a[t]
) 

simpleType(
  name = s,
  base = xsi:UrSimpleType,
  derivation = restriction,
  refinement = {restriction},
  abstract = false,
  content = xsi:integer{0,∞}
) 

complexType(
  name = t,
  base = xsi:UrType,
  derivation = restriction,
  refinement = {restriction,extension},
  abstract = false,
  content = t/@b & t/@c
) 

attribute(
  name = t/@b,
  base = xsi:UrAttribute,
  derivation = restriction,
  refinement = {restriction},
  abstract = false,
  content = t/@b[xsi:string]
) 

attribute(
  name = t/@c,
  base = xsi:UrAttribute,
  derivation = restriction,
  derivation = {restricition},
  abstract = false,
  content = t/@c[s]{0,1}
)

complexType(
  name = u,
  base = t,
  derivation = extension,
  refinement = {restriction,extension},
  abstract = false,
  content = (t/@b t/@c),
  (u/d | u/e)
) 

element(
  name = u/d,
  base = xsi:UrElement,
  derivation = restriction,
  refinement = {},
  abstract = false,
  content = u/d[u/d/*]
) 

complexType(
  name = u/d/*,
  base = xsi:UrType,
  derivation = restriction,
  refinement = {},
  abstract = false,
  content = u/d/*{0,∞}
) 

element(
  name = u/d/*/a,
  base = xsi:UrElement,
  derivation = restriction,
  refinement = {},
  abstract = false,
  content = u/d/*/a[xsi:string]
) 

element(
  name = u/e,
  base = xsi:UrElement,
  derivation = restriction,
  refinement = {},
  abstract = false,
  content = u/e[xsi:string]
) 

Note that we do not nest declarations to express their scope. The scope of a declaration is reflected in its normalized name.

2.3  Documents and Forests

There is also a compact notation for representing XML, both before and after normalization. This notation is not intended in any way to be used as a replacement for traditional XML syntax.  Having a more compact, but equally expressive, equivalent notation will aid significantly in the exposition below (in particular it keeps the inference rules to a reasonable size).  Here is the original document in this notation:

a[
  @xsi:type["u"],
  @b["zero"],
  @c[1,2],
  d[
    a["three"],
    a["four"]
    ]
  ] 

Note that attributes and elements are represented uniformly, as are sequences of attributes, sequences of elements, and lists of atomic datatypes. Note also that from this perspective a document is just a element without a parent. Therefore we will drop the term "document" and simply use the term element. The term "this document" will continue to refer to the document you are reading.

Here is the normalized element:

a[
  @xsi:type["u"],
  t/@b["zero"],
  t/@c[1,2],
  u/d[
    u/d/*/a["three"],
    u/d/*/a["four"]
    ]
  ] 

Finally, here is the normalized element with type information added

a[
  u types t/@b[xsi:string types "zero"],
  t/@c[s types 1,2],
  u/d[
    u/d/* types u/d/*/a[xsi:string types "three"],
    u/d/*/a[xsi:string types "four"]
    ]
  ] 

Unlike the xsi:type convention, this notation allows one to uniformly express information about element and attribute types. The type of an element or attribute is indicated by writing x[t types d] where x is an attribute or element name, t is a type name, and d is the content of the attribute or element.

We will use the term forest or ordered forest when referring to lists of attributes and elements, as in the content of a element. For example, while the above is an element its content:

  u types t/@b[xsi:string types "zero"],
  t/@c[s types 1,2],
  u/d[
    u/d/* types u/d/*/a[xsi:string types "three"],
    u/d/*/a[xsi:string types "four"]
    ]

3  Structures

This section defines the structures used in formalism: names, wildcards, atomic datatypes, model groups, components, and forests.

3.1  Names

A namespace is a URI reference, and a local name is an NCName, as in the Namespace recommendation. We let i range over namespaces and the "non-namespace" (where items not in a namespace reside) and j range over local names.  In order to cover the case of naming components that are not in a namespace, i may be empty.  Using these names we can create unique identifiers for the components of a schema.  These names are for the abstract components of the schema and ultimately are not dependent on the XML Schema transfer syntax or any configuration of files the schema may be stored in.

A symbol space is one of the six symbol spaces in XML Schema. We let ss range over symbol spaces.

A symbol name consists of a symbol space paired with a local name or with * (the latter names an anonymous component). A name consists of a URI reference followed by a sequence of one or more symbol names. We let sn range over symbol names, and x range over names.

Here l ≥ 1 is the scope length of the name.

An example of a name is:

The scope length of this name is 4.

In this document we've found it convenient to use a short form of names.  Symbol names in the attribute symbol space are written @j, all other symbol names are written j (or * for anonymous names) - in our examples we've ensured our local names are unique across all symbol spaces. The URI reference may be dropped when it is obvious from context. For example, the short form of the name above is u/d/*/a. Additional examples of names and short forms appear in Section 2.1.

Before normalization, all names in a forest have scope length equal to one. It is helpful to define functions to extract the namespace from a name, and to extract the symbol space and local name of the last symbol name. We define namespace(x) = i, symbol(x) = ss, and local(x) = j when x = i#sn₁/…/sn_l and sn_l = ss::j.

We also introduce several subclasses of names. An attribute name is the name of an attribute component, and similarly for element, simple type, and complex type names. We let a, e, s, k range over attribute, element, simple type, and complex type names.

A type name is a simple or complex type name. We let t range over type names.

The class of a name must be consistent with its symbol space.

3.2  Wildcards

A wildcard denotes a set of qualified names. A wildcard item is of the form *:* denoting any name in any namespace, i:* denoting any name in namespace i, or i:j denoting just the name with namespace i and local name j. A wildcard consists of wildcard items, union of wildcards, or difference of wildcards. We let v range over wildcard items, and w range over wildcards.

For example, the wildcard *:*!(baz:*+xsi:string)%strict denotes any name in any namespace, except for names in namespace baz, and local name string in namespace xsi. Since it will be convenient to write wildcards with minimal parentheses, we will assume the precedence + > ! > %.

3.3  Atomic datatypes

We take as given the atomic datatypes from XML Schema Part 2. We let p range over atomic datatypes, and c range over constants of such datatypes.

Typically, an atomic datatype is either a primitive datatype, or is derived from another atomic datatype by specifying a set of facets. Note lists of atomic datatypes are specified using repetition while unions are specified using alternation, as defined below.

An example of an atomic datatype is xsi:string, and a constant of that datatype is "zero".

3.4  Content groups

Let g range over content groups.

An example of a group appears in Section 2.2.1.

The empty sequence matches only the empty forest; it is an identity for sequence and all. The empty choice matches no forest; it is an identity for choice.

For use with repetitions, we extend arithmetic to include ∞ in the obvious way. For any n we have n + ∞ = ∞+ n = ∞ and n ≤ ∞ is always true, and ∞ < n is always false.

3.5  Components

A sort is one of the six sorts of component in XML Schema. We let srt range over sorts.

(Shortcoming: we make no further use of attributeGroup or modelGroup in this document.)

A derivation specifies how a component is derived from its base. We let der range over derivations, and ders range over sets of derivations.

We let b range over booleans.

A component is a record consisting of a constructor (srt) with six fields.

name

is the name of the component (x);

base

is the name of the base component of the structure (x);

derivation

specifies how the component is derived from the base (der);

refinement

is the set of permitted derivations from this component as base (ders);

abstract

is a boolean, representing whether this type is abstract (b);

content

is the content of the structure, a model group (g).

We let cmp range over components.

Examples of components appear in Section 2.2.2.

For a given schema, we assume a fixed dereferencing map that takes names to the corresponding components. We write deref(x) = cmp if name x corresponds to component cmp.

The dereferencing map must map attribute names to attribute components, and similarly for elements, simple types, and complex types.

3.6  Constraints

Recall that the group constructs are used uniformly in several contexts. Repetition (g{m,n}) is used for lists of atomic datatypes, to indicate whether an attribute is optional, and for elements. Similarly, all (g₁ & g₂) is used for attributes and for elements. The advantage of this approach is that the semantics of groups is uniform, and need be given only once. Thus, for instance, how repetition acts is defined once, not separately for attributes and elements.

The group grammar is rather more accommodating than that implicit in XML schemas. It permits attributes to have complex local type definitions, multiple occurrences of the declaration of a given attribute name, and the mentioning of an attribute anywhere in the defintion of a group. As we do not generally translate our group grammars back into XML schemas, this permissiveness is of little consequence. We can, nonetheless, define various sub-grammars of the group grammar to constrain matters in so as to be consistent with the XML schemas specification.

However, it is helpful to define additional syntactic categories that specify various subsets of groups. These syntactic classes are then used to constrain the content of components, for instance, to indicate that the content of an element component should be an element, and that the content of a type component should consist of attributes followed by elements.

An attribute group contains only attribute names, combined using the all connector (&). An element group contains no attribute names. (Shortcoming: all groups in element groups should be further constrained as in Schema Part 1, Section 5.7, All Group Limited.)

Given the above, we can specify the allowed contents of the four sort of component as follows. An attribute content is either an attribute or an optional attribute, where the content is a simple type name. An element content is an element where the content is a type name. A simple type content is an atomic datatype or a list of atomic datatype. A complex type content is an attribute group followed by either a simple type content or an element group.

The content of each sort of component corresponds to the syntax above. That is, the content of an attribute component is always an attribute content ac; the content of an element component is always an element content ec; the content of a simple type component is always a simple content sc; and the content of a complex type component is always a complex content kc. Further, for an attribute or element component the name of the component is the same as the name of the attribute or element in its content.

It is easy to confirm that the example components in Section 2.2.2 satisfy these constraints.

3.7  Ordered Forests

A forest is a sequence of items, where each item is either an atomic datatype, or an attribute (with an atomic datatype as content), or an element (with a forest as content). We let d range over forests.

Examples of forests appear in Section 2.3.

A typed forest is an ordered forest with added type information for each element and attribute. We let td range over typed ordered forests.

3.8  Inference rules

Operations such as normalization and matching are described with an inference rule notation. Originally developed by logicians [15,16,7], this notation is now widely used for describing type systems and semantics of programming languages [10]. In this notation, when all judgements above the line hold, then the judgement below the line holds as well. Here is an example of a rule used later on. We write d in g if forest d matches group g. 

Sequence:

d₁ in g₁                   d₂ in g₂

d₁ ,d₂ in g₁

The rule says that if both d₁ in g₁ and d₂ in g₂ hold, then d₁ ,d₂ in g₁ , g₂ holds as well. For instance, take d₁ = a[1], d₂ = b["two"], g₁ = a[xsi:integer], and g₂ = b[xsi:string]. Then since both

hold, we may conclude that

holds.

4  Normalization

Normalization of a forest replaces each name by the corresponding normalized name, and adds type information to the forest. Normalization is performed with respect to a given schema; in our formalism the schema is determined by the dereferencing map, deref(). Section 2.3 gives an example of a document before and after normalization.

Prior to normalization, all names in the forest have exactly one symbol name. We build normalized names by extending a name with an additional symbol name. Let x₁ and x₂ be two names, with namespace(x₁) = namespace(x₂), and where the second forest has only one symbol name. We write x₁ |> x₂ for the operation that extends x₁ by adding the symbol name of x₂, defined as follows.

On the other hand, if x₁ and x₂ are from different namespaces (namespace(x₁ ) = i, namespace(x₂) = j and i ≠ j), then x₁ |> x₂ is defined as:

Finally, for each sort there is a root type (AnyType, AnyElement, etc.) These are fixed points, i.e.,

(Since these constants will eventually be defined in a fixed namespace, this is really subsumed by the previous rule.)

We write x |- a ⇒a′ and x |- e ⇒e′ to indicate that in the context specified by name x that attribute name a normalizes to a′ or that element name e normalizes to e′. To normalize an attribute or element we extend the context (if the extended name is in the domain of deref(); these are the `extend' rules), or use the element name directly (otherwise; these are the `reset' rules). We write x in dom(deref()) and x notin deref() to indicate whether or not x is in the domain of the dereferencing map; that is, whether or not deref(x) is defined. If x₁ and x₂ are in different namespaces, then x₁ |> x₂ is undefined, and we say x notin deref() holds.

Extend Attribute Transitive:

y  |> a in dom(deref())
x <: y

x  |- a  ⇒ y  |> a

If the attribute name does not appear for the current type, check for that name among supertypes.

Extend Element Transitive:

y  |> e in dom(deref())
x <: y

x |- e  ⇒ y   |> e

If the element name does not appear for the current type, check for that name among supertypes.

Extend Attribute Base:

a in dom(deref())

x  |- a  ⇒ a

An attribute name can be normalized if it corresponds to a known name.

Extend Element Base:

e in dom(deref())

x  |- e  ⇒ e

An attribute name can be normalized if it corresponds to a known name.

EDITORS NOTE:  These inference rules will need to be revisited with regards to the typing of wildcards.

We write x |- d ⇒dt to indicate that in the context specified by name x that forest d normalizes to typed forest td. We write @xsi:type notin d if d does not contain an xsi:type attribute. Note that the type names in xsi:type attributes always refer to global types and need not be normalized.

Constant:

x |- c  ⇒ c'

Empty Document:

x |- ε  ⇒ ε

Sequence:

x |- d₁ ⇒ td₁      y |- d₂ ⇒ td₂

x |- d₁,d₁ ⇒ td₁ , td₂

Attribute:

x |- a ⇒ a'
deref(a').content = a'[s] or deref(a').content = a'[s]{0,1}
s |- d ⇒ td

x |- a[d]  ⇒ a'[s types td]

Untyped Element:

x |- e ⇒ e'
@xsi:type notin d
deref(e').content = e'[t]
t |- d ⇒ td

x |- e[d]  ⇒ e'[t types td]

Typed Element:

x |- e ⇒ e'
deref(e').content = e'[t]
t <: t'
t |- d ⇒ td

x |- e[@xsi:type[t], d]  ⇒ e'[t types td]

The (Typed Element) rule uses the relation x  < :x′, which is defined Section 5.1.

5  Derivation

5.1  Base chain

We write x <: :x′ if starting from the component with name x one can reach the component with name x′ by successively following base links.

Reflexive:

x <: x

Transitive:

x <: x'    x' <: x''

x <: x''

Base:

deref(x).base = x'

x <: x'

5.2  Extension

We write g  < :_extg′ if group g is derived from group g′ by adding attributes and elements. It is specified using attribute groups ag and element groups ag as defined in Section 3.6.

Extend:

ag , eg < :_ext (ag & ag') , eg , eg'

5.3  Restriction

We write g < :_res g′ if the instances of group g are a subset of the instance of group g′. That is, g < :_res g′ if for every forest d such that d in g it is also the case that d in g′.

5.4  Constraints

A schema must satisfy certain constraints on derivation to be well-formed. Define x  < :_der x′ to be x  < :_resx′ if der = restriction and x  < :_extx′ if der = extension. We write |- x to indicate that the component with name x is well-formed with respect to derivation. (N.B. This use of turnstile differs from that in normalization.)

Refinement:

x' = deref(x).base
der = deref(x').derivation
deref(x).content < :_der deref(x').content

|- x

6  Validation

6.1  Content validation

We write c in_p p if constant c matches atomic datatype p. We do not specify this relation further, but simply assume it is as defined in XML Schema Part 2.

We write e in_v v and e in_w w if element name e matches wildcard item v or wildcard w. We write e notin_w w if it is not the case that e in_w w. While these rules are expressed for elements, the exact same rules apply to attributes if we substitute attribute name for element name in the following rules.

Any Namespace, Any Local:

e in_w*:*

Given Namespace, Any Local:

namespace(x) = i

e in_w i:*

Given Namespace, Given Local:

namespace(e) = i
local(e) = j

e in_w i:j

Wildcard Item:

e in_W v

e in_W v

Wildcard Sum 1:

e in_W w₁

e in_W w₁ + w₂

Wildcard Sum 2:

e in_W w₂

e in_W w₁ + w₂

Wildcard Difference:

e in_W w₁    e notin_W w₂

e in_W w₁ ! w₂

We write d |→_unmix d′ (read ``d unmixes to d′'') if d is a sequence of elements and characters and d′ is the same sequence with all character data removed. This is used for processing mixed content.

Unmix Empty:

ε  |→_unmix ε

Unmix Sequence:

d₁  |→ _unmixd'₁     d₂  |→_unmix d'₂

d₁ , d₂  |→_unmix d'₁ , d'₂

Unmix Element:

e[d]  |→_unmix e[d']

Unmix Character Data:

c  |→_unmix ε

We write d |→_inter d';d'' (read "d interleaves d' and d'' ") if some interleaving of d' and d'' yields d.  This relates one sequence to many pairs of sequences.  This is used for processing g₁ &g₂.

Interleave Empty:

ε  |→_inter ε;ε

Interleave Sequence:

d₁  |→ _interd'₁;d"₁      d₂  |→_inter d'₂;d"₂

d₁ , d₂  |→_inter d'₁ , d'₂ ;d"₁,d"₂

Interleave Item 1:

d  |→_inter d;ε

Interleave Item 2:

d  |→_inter ε;d

We write d in g if forest d matches group g.

Empty:

ε  in e

Sequence:

d₁  in g₁     d₂  in g₂

d₁ , d₂  in g₁ , g₂

Choice 1:

d  in g₁

d  in g₁ | g₂

Choice 2:

d  in g₂

d  in g₁