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₁ | g₂

Interleave:

d |→_inter d'₁;d"₂    d₁ in g₁    d₂ in g₂

d in g₁ & g₂

Repetition 1:

d₁ in g    d₂ in g{m,n}

d₁ ,d₂  in g{m +1,n+1}

Repetition 2:

d₁ in g    d₂ in g{0,n}

d₁ ,d₂  in g{0,n+1}

Repetition 3:

ε  in g{0,n}

Attribute:

d  in g

a[d]  in a[g]

Element:

d  in g

e[d]  in e[g]

Mixed Group:

d  |→_unmix d'  d'  in g

d  in mixed(g}

Typed Attribute:

d  in s

e[s types d]  in e[s]

Typed Element:

d  in t    t <: t'

e[t types d]  in e[t']

Wildcard:

d  in e    e in_W w

d  in w

Atomic Datatype:

c in_p p

c  in p

Element Refinement:

d  in e    e <: e'

d  in e'

Component Name:

d  in g    g = deref(x).content

d  in x

The (Typed Element) and (Element Derivation) rules use the relation x  < :x′, which is defined in Section 5.1. The check that t  < :t′ in the (Typed Element) rule is redundant, as it is also performed during normalization.

When processing a normalized document with types, the ( Attribute) and (Element) rules are not required, the (Typed Attribute) and ( Typed Element) rules are used instead. However, we will write td in g whenever |- d ⇒td and d in g.

6.2  ID/IDREF validation

We write nc in IDREFs(td) if nmtoken constant nc appears as the content of an attribute or element of type IDREF with typed forest td. We write nc in IDs(td) if nmtoken constant nc appears as the content of an attribute or element of type ID somewhere with typed forest td. We write nc in ! IDs(td) if nmtoken constant nc appears exactly once as the content of an attribute or element of type ID somewhere with typed forest td. We write nc in IDs!(td) if nc in! IDs(td). We write td OK if typed forest td is valid with respect to ID and IDREF, that is, if no ID is defined twice, and every IDREF has a corresponding ID.

IDREFs(d) ⊆ IDREFs(td)    IDs(td) ⊆ IDs!(tc)

td OK

A value nc counts as a reference whenever there is an element or attribute of type IDREF in an instance having nc as its value:

A-Refs:

nc in IDREFs(a[IDREF types nc])

E-Refs:

nc in IDREFs(e[IDREF types nc])

A value nc counts as a referenece whenever there is an element among whose children nc counts as a referenece:

Child-Refs:

nc in IDREFs(td')

nc in IDREFs(e[t' types td'])

A value nc counts as a reference among a sequence of instances whenever it counts as a reference among a subsequence of those instances:

Subref 1:

nc in IDREFs(td₁)

nc in IDREFs(e[td₁ , td₂])

Subref 2:

nc in IDREFs(td₂)

nc in IDREFs(e[td₁ , td₂])

The notation in!   indicates that a structure of a given shape occurs uniquely within another. An instance td satisfies the id-uniqueness criterion whenever any NCNAME that is among the IDs of td is also among its uniquely occurring IDs:

Not-ID:

nc notin IDs(td)

nc in IDs(td) → nc in!  IDs(td)

ID:

nc in! IDs(td)

nc in IDs(td) → nc in!  IDs(td)

A value nc counts as an ``id'' whenever there is an element or attribute of type ID in an instance having nc as its value::

A-ID:

nc in! IDs(a[ID types nc])

E-ID:

nc in! IDs(e[ID types nc])

A value nc counts as an ``id'' among a sequence of instances whenever it counts as an ``id'' among a subsequence of those instances, and does not count as an ``id'' among the remaining subsequence of those instances:

ID 1:

nc in IDs(td₁)

nc in IDs(td₁ , td₂)

ID 2:

nc in IDs(td₂)

nc in IDs(td₁ , td₂)

A value nc counts as a unique ``id'' among a sequence of instances whenever it counts as an ``id'' among a subsequence of those instances, and does not count as an ``id''among the remaining subsequence of those instances:

UN-ID 1:

nc in! IDs(td₁)    nc notin IDs(td₂)

nc in! IDs(td₁ , td₂)

UN-ID 2:

nc in! IDs(td₂)    nc notin IDs(td₁)

nc in IDs(td₁ , td₂)

Lastly, we have the following obvious relationship between occurrence in IDs and unique occurrence in IDs:

InnIDs-InIDs:

nc in! IDs(td)

nc in IDs(td)

7  XML Schema to Formalization Mapping

EDITOR'S NOTE:  Future versions of this document will contain a mapping from the XML Schema components described in [11] to sorts.  Both XML Schema and models make a distinction between the underlying model (components in the case of XML Schema, sorts in the current case) and the surface syntax (the set of valid <schema> elements accepted for either).  In both cases, the underlying model is considered more significant.

This section will describe the mapping from XML Schema instance syntax to sorts. This requires performing two mutually recursive activities:

• converting from XML Schema surface syntax into a set of sorts
• for each sort, building its contents (note that component contents do not nest, the content of one component contains only references to other components).

To do so, we also introduce two new relations:

• d -→ g (eg writes as g) takes the xsdl syntax represented by eg and returns a content description fragment, valid according to the grammar production rules enumerated previously. Generally, f is the name (or names, if eg is a sequence) of the sort corresponding to eg.
• e[d] =⇒ cmp (e corresponds to cmp) takes an xsdl structure definition, such as a complexType definition, and maps it into an sort, such as a complex.

In any language of the complexity of XML Schema, there are both syntactic constraints expressible directly in the syntax of the language, and semantic constraints which further limit allowed expressions. In the following we enumerate those fragments of XML Schema which correspond to semantically valid expressions. While this could be done by enumerating all such sequences, that would include enumerating all the different cases of optionality and order - a daunting task. Instead, we reuse the grammars for content models developed above to specify fragments of XML and then pattern match against portions of this. The goal is to cover all fragments of XML Schema which are semantically coherent - other fragments may be syntactically valid, but not correspond to useable constructs. In each of the inference rules, the left hand side will be a string in this grammar. Strings in bold match strings in the XML instance. Strings in italics pattern match as variables to be used in the inference rule. As these represent fragments of schemas valid against the Schema for Schemas, we assume they have been validated and all default/fixed values for attributes are present. The only particular addition to this is to consider ``*'' as the default value for the name attribute of a nested complexType.

The following fragment gives an example:

anElem[@attr1[val1], @attr2[val2], nest[eg], ev]

Here we have:

• An element with GI anElem with a required attribute named attr1 whose value is assigned to the variable val1, and a second attribute named attr2 whose value is assigned to the variable val2.
• Within anElem another element named nest whose contents is assigned to the variable eg.
• And finally, another nested element whose value is assigned to the variable ev.

Note that we provide a sequence for the attributes. This is purely for the convenience of the reader - in an actual instance these would appear in any order.

We also make the following additions to the grammar specified up to this point:

This formalism extends derivation to cover all sorts. Therefore, every kind of sort has a base sort from which all user-defined sorts must, ultimately, be derived. Of these, only two, for complex and simple types, are currently available from XML Schema. For the time being, the rest (such as for elements and attributes) are restricted to sorts and are not available to users.

7.1  Conversions for content model particles

Write All:

x |- ev₁ -→ e_1
...
x |- ev_n -→ e_n

x |- all[ev₁...ev_n] -→ (e₁&...&e_n)

If there is an idall element with content ev₁,...,ev_n and each ev_i converts to e_i in the context of x, then the element converts to (e₁,...,e_n).

Write Sequence:

x |- ev₁ -→ e_1
...
x |- ev_n -→ e_n

x |- sequence[@minOccurs[m] , @maxOccurs[k], ev₁...ev_n] -→ (e₁&...&e_n){m.k}

Write Choice:

x |- ev₁ -→ e_1
...
x |- ev_n -→ e_n

x |- choice[@minOccurs[m] , @maxOccurs[k], ev₁...ev_n] -→ (e₁|...|e_n){m.k}

For a sequence or choice with minOccurs or maxOccurs, where one or the other has a value other than 1, that sequence or choice converts to a representation with min and max values indicated at the end.

Write Complex:

x |- complexType[t] =⇒ c

x |- complexType[t]  -→ c.name

If a complexType corresponds to some sort, c, then it writes as the name of that sort.

Write Attribute:

x |- attribute[@name[s] , ag , eg] =⇒ c

x |- attribute[@name[s] , ag , eg] -→ c.name

If an attribute corresponds to some sort, c, then it writes as the name of that sort.

Write Attribute Ref:

x |- attribute[@ref[s] , ag ,  ev₁,...,ev_n] → deref(x |> s).name

If an attribute (in a content model) refers to some other attribute, c, then it writes as the name of the sort corresponding to that attribute.

Write Element Ref 1:

x |- element[@name[s] , ag , eg] =⇒ c

x |- element[@name[s] , ag , eg] -→ c.name

If an element corresponds to some sort, then it writes as the name of that sort.

Write Occurs:

x |- element[ag , eg] -→ y

x |- element[@minOccurs[m] , @maxOccurs[k] , ag , eg] -→ y{m, k}

If an element has minOccurs or maxOccurs attributes, one of which has a value other than 1, and the element without the attributes writes as y, then the element with the attributes writes as y{m, n}, where m and n are the values of the attributes.

Write Element Ref 2:

x |- element[@ref[s] , ag ,  eg] -→ deref( x |> s).name

If an element (in a content model) refers to some other element, c, then it writes as the name of the sort corresponding to that attribute.

7.2  Correspondences from XML Schema to sorts

Valid Schema Doc:

x|- e₁=⇒srt₁
...
x|- e_k =⇒ srt_k

|- schema[@targetNamespace[x], e₁, ..., e_k]

A schema element is accepted if all of its children convert to components in the context of its targetNamespace.

Map Complex A:

y = x |> n
y |-  cm -→ elems    y |-  am -→ atts

x  |- complexType[@abstract[a] , @final[f] , @block[b] ,
@mixed[m] , @name[n] , cm , am]
=⇒ complex(name = y, base = xsi:AnyType,
derivation = restriction,
refinement = if (f == ##all) then {restriction, extension} else f,
abstract  = a
content = (atts, if (m == true) then mixed(elems) else elems))

Given a complex type which is not a derivation, we determine its name and convert its attribute and content definitions into component content (within the context of the name). We then use these to create a complex sort for the complex type.

Map Restriction 1:

y = x |> n
z = deref(x |> p)
x.content = (am₂ ,cm₂)
y |-  cm -→ cont y |-  am -→ atts

x  |- complexType[@abstract[a] , @final[f] , @block[b] ,
@mixed[m] , @name[n] , 
complexContent[restriction[@base[p],cm , am]]
=⇒ complex(name = y, base = x.name,
derivation = restriction,
refinement = if (f == ##all) then {restriction, extension} else f,
abstract  = a
content = (((am₂ - attrs), attrs), if (m == true) then mixed(cont) else cont))

If a complex type is a restriction of another type, then we proceed as above, except we retrieve the contents of the super type and the set of attributes of the derived type is a combination of its own and those of the parent. In this case, am₂ - attrs represents the attributes defined in am₂ less any attributes in attrs with the same name. (Note, this definition may require more work.)

Map Complex Extension:

y = x |> n
z = deref( x |> p)
x.content = (am₂ ,cm₂)
y |-  cm -→ cont y   |-  am -→ atts

x  |- complexType[@abstract[a] , @final[f] , @block[b] ,
@mixed[m] , @name[n] , 
complexContent[extension[@base[p],cm , am]]
=⇒ complex(name = y, base = z.name,
derivation = extension,
refinement = if (f == ##all) then {restriction, extension} else f,
abstract  = a
content = (((am₂ - attrs), attrs), if (m == true) then mixed(cm₂, cont) else cm₂ , cont))

If the complex type is an extension of the complex type, then we retrieve the contents of the super type. The attributes of the derived type is the union of its attributes and those of the supertype. Its content model is a sequence consisting of the content model of the supertype followed by that of the subtype declaration.

Map Restriction 2:

y = x |> n
z = deref( x |> p)
x.content = (st₂ ,am₂)
y |- st -→ simp    y |- am -→ attrs

x  |- complexType[@abstract[a] , @final[f , @block[b] ,
@mixed[m] , @name[n] , 
simpleContent[restriction[@base[p],st , am]]
=⇒ complex(name = y, base = z.name,
derivation = extension,
refinement = if (f == ##all) then {restriction, extension} else f,
abstract  = a
content = ((am₂ , attrs), if (m == true) then mixed(simp) else cm₂ , simp))

If a complex type is a restriction with simple content, then the base type refers to a complex type with simple content. The content of that type (z, above) must be a simple type and 0 or more attributes. We convert the simple type description and create a new complex sort.

Map Global Element 1:

y = x |> n
z = x |> s
c = deref( x |> t)
c in complex

x  |- element[@abstract[a] , @final[f , @block[b] , @name[n] , 
@nillable[u], @substitutionGroup[s] , @type[t]]
=⇒ element(name = y,
base = if (z |- null) then z else AnyElement,
derivation = c.derivation,
refinement = {restriction, extension},
abstract  = a
content = c.name)

To create an element sort using a type reference to a complex type.

Map Global Element 2:

y = x |> n
z = x |> s
y  |- t ⇒ c

x  |- element[@abstract[a] , @final[f , @block[b] , @name[n] ,  @form[o] , default[d] ,
@fixed[i] , @nillable[u], @substitutionGroup[s] , @type[t]]
=⇒ element(name = y,
base = if (z |- null) then z else AnyElement,
derivation = c.derivation,
refinement = {restriction, extension},
abstract  = a
content = c.name)

To create an element containing an inlined type definition, find the sort corresponding to the type definition and create the element sort using the name of the type definition for the content.

Map Local Element 1:

y = x |> n
c = x |> t

x  |- element[@default[d], @fixed[i] , @name[n] ,  @form[o] , 
@maxOccurs[m] , @minOccurs[n] , @nullable[u], @type[t]]
=⇒ element(name = y,
base =  AnyElement,
derivation = restriction,
refinement = {},
abstract  = false
content = c.name)

A local element which references a type creates a new element structure, whose content is the name of the referenced type.

Map Local Element 2:

y = x |> n
y  |- t ⇒ c

x  |- element[@default[d], @fixed[i] , @name[n] ,  @form[o] , 
@maxOccurs[m] , @minOccurs[n] , @nullable[u], t]
=⇒ element(name = y,
base =  AnyElement,
derivation = restriction,
refinement = {},
abstract  = false
content = c.name)

A local element with an inlined type declaration.

Map Attribute 1:

y = x |> n
c  = x |> t

x  |- attribute[@name[nd], @form[o] , @type[tn] ,  @use[u] , @value[v]]
=⇒ attribute(name = y,
base =  AnyAttribute,
derivation = restriction,
refinement = {},
abstract  = false
content = c)

An attribute declaration referencing a type.

Map Attribute 2:

y = x |> n
y |- s  ⇒ c

x  |- attribute[@name[nd], @form[o] ,  @use[u] , @value[v], s]
⇒ attribute(name = y,
base =  AnyAttribute,
derivation = restriction,
refinement = {},
abstract  = false
content = c.name)

An attribute with an inlined type definition.

8  Index of notations

∞

infinity (§3.4)

ε

empty sequence (§3.4), empty forest (§3.7)

Ø

empty choice (§3.4), empty set

g₁ , g₂

sequence group (§3.4)

g₁|g₂

choice group (§3.4)

g₁ &g₂

all group (§3.4)

g{m,n}

repetition group (§3.4)

a[g]

attribute group (§3.4)

e[g]

element group (§3.4)

d₁ ,d₂

sequence forest (§3.7)

a[d]

attribute forest (§3.7)

e[d]

element forest (§3.7)

a[s types td]

typed attribute forest (§3.7)

e[t types td]

typed element forest (§3.7)

d in g

forest d matches group g (§6)

|-

 

turnstile (§4)

x₁ |> x₂

x1 extends x2 (§4)

x |- d ⇒dt

d normalizes to dt in context x (§4)

c in_p p

c matches datatype p (§6.1)

e in_v v

e matches wildcard item v (§6.1)

e in_w w

e matches wildcard w (§6.1)

d |→_unmix d′

d unmixes to d' (§6.1)

d |→_inter d';d''

d interleaves d' and d'' (§6.1)

d ⊆ d'

d is a subset of d' (§6.2)

nc in IDREFs(td)

nc is in the set of IDREFs in td (§6.2)

d -→ g

d writes as g (§7)

e[d] =⇒ cmp

e corresponds to cmp (§7)

x  < :x′

derivation (§5.1)

g  < :_extg′

extension (§5.2)

g  < :_resg′

restriction (§5.2)

x  < :_der x′

extension or restriction (§5.4)

a

attribute name (§3.1)

b

boolean (§3.5)

c

constant of atomic datatype (§3.3)

d

forest (§3.7)

e

element name (§3.1)

g

model group (§3.4)

i

namespace (§3.1)

j

local identifier (§3.1)

k

complex type name (§3.1)

l

scope length of name (§3.1)

m

minimum in repetition (§3.4)

n

maximum in repetition (§3.4)

p

atomic datatype (§3.3)

s

simple type name (§3.1)

t

type name (§3.1)

u

union datatype (§3.6)

v

wildcard item (§§3.2)

u

wildcard expression (§§3.2)

w

wildcard (§§3.2)

x

name (§3.1)

ag

attribute group (§3.6)

eg

element group (§3.6)

ac

attribute content (§3.6)

ec

element content (§3.6)

kc

complex type content (§3.6)

sc

simple type content (§3.6)

uc

union type content (§3.6)

der

derivation (§3.5)

srt

sort (§3.5)

deref(x)

dereferencing (§3.5)

local(x)

local name (§3.1)

namespace(x)

namespace (§3.1)

symbol(x)

symbol space (§3.1)

Appendix A Infidelities in the current formalization of XML Schema

This document is based on the syntax of XML Schema in the proposed recommendation draft. The Formalization Taskforce will continue in operation until XML Schema becomes a recommendation.

Also, in a few places the specification is not quite equivalent to that in XML Schema, notably for the definition of derivation. We believe that with extra time it should be possible to model all or most of XML Schema.

• Restriction. This document allows one type to be a subtype of another if the content group of the subtype validates a subset of the forests validated by the content of the base type. XML Schema places several further restrictions on this relationship which are not currently modelled.
• Content models. Impose additional constraints on content models until they are exactly like XML Schema.
  • mixed element content is not fully integrated;
  • unambiguity constraint on content models;
  • checking that abstract components are not instantiated;
  • subtyping permissions such as final and block;
  • null elements;
  • formal model of atomic datatypes.
  • support for form and form default
  • support for block, use, and value
  • mapping from sorts to XML Schema components and coverage of the post-schema-validation Infoset
• Identity constraints. Due to the drastic changes in the identity constraints at the London WG face-to-face, identity constraints have been dropped from this version.
• Schema composition.
  • schema import is not considered
  • schema include is not considered
  • schema redefine is not considered

Appendix B Bibliography

[1] Serge Abiteboul and Peter Buneman and Dan Suciu, Data on the Web : From Relations to Semistructured Data and XML Morgan Kaufmann, 1999

[2] Alfred V. Aho, "Algorithms for Finding Patterns in Strings", Handbook of Theoretical Computer Science, Jan van Leeuwen, MIT Press Elsevier, Cambridge, Massachusetts, 1990

[3] Paul V. Biron and Ashok Malhotra, XML Schema Part 2: Datatypes, , World Wide Web Consortium, 2000

[4] Tim Bray and Jean Paoli and C. M. Sperberg-McQueen, Extensible Markup Language (XML) 1.0, , World Wide Web Consortium, 1998

[5] James Clark and Steve DeRose, XML path language (XPath) version 1.0, , World Wide Web Consortium, 1999

[6] David C. Fallside, XML Schema Part 0: Primer , World Wide Web Consortium, 2000

[7] Gottlob Frege, "Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought (1879)", From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931, ed. Jan van Heijenoort, , Harvard University Press, Cambridge, Massachusetts, 1967

[8] Haruo Hosoya and Jerome Vouillon and Benjamin C. Pierce, "Regular Expression Types for XML", Proceedings of the International Conference on Functional Programming (ICFP), 2000

[9] Tova Milo and Dan Suciu, "Type Inference for Queries on Semistructured Data", Proceedings of the ACM Symposium on Principles of Database Systems, 1999

[10] John C. Mitchell, Foundations for Programming Languages, , MIT Press, 1996, Cambridge, Massachusetts

[11] Henry S. Thompson and David Beech and Murray Maloney and Noah Mendelsohn, XML Schema Part 1: Structures, , World Wide Web Consortium, 2000

[12] Philip Wadler, "A formal semantics of patterns in XSLT", Proceedings of Markup Technologies, ed. B. Tommie Usdin and Deborah A. Lapeyre and C. M. Sperberg-McQueen, Philadelphia, 1999

[13] Philip Wadler, "New Language, Old Logic", Dr Dobbs Journal, December, 2000

[14] Brown, Jr., Allen L., "Derivation, tolerance and validity: a formal model of type definition in XML Schemas", Proceedings of XML Europe 2000, ed. Pamela Gennusa, Paris, 2000

[15] Gaisi Takeuti, Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 81, North-Holland/American Elsevier, Amsterdam, 1975

[16] Dag Prawitz, Natural Deduction: A Proof-Theoretical Study, , Almqvist & Wiksell, Stockholm, 1965,

[17] Solomon Feferman, "Theories of Finite Type Related to Mathematical Practice", Handbook of Mathematical Logic, ed. Jon Barwise, Elsevier North Holland, Amsterdam, 1977