XQuery 1.0 and XPath 2.0 Formal Semantics

2.1.1 Notations from grammar productions

Grammar productions are used to describe "objects" (values, types, [XPath/XQuery] expressions, etc.) manipulated by the Formal Semantics. The Formal Semantics makes use of several kinds of grammar productions: productions from the [XPath/XQuery] grammar itself, productions for a subset of the [XPath/XQuery] language called the XQuery core which is used throughout this document, and other productions used for formal specification only such as for the XQuery type system.

XQuery grammar productions describe the XQuery language and expressions. XQuery productions are identified by a number, which corresponds to their number in the [XQuery 1.0: A Query Language for XML] document, and are marked with "(XQuery)". For instance, the following production describes FLWOR expressions in XQuery.

[For/FLWR] Expressions

For the purpose of this document, the differences between the XQuery 1.0 and the XPath 2.0 grammars are mostly irrelevant. By default, this document uses XQuery 1.0 grammar productions. Whenever the grammar for XPath 2.0 differs from the one for XQuery 1.0, the corresponding XPath 2.0 productions are also given. XPath productions are identified by a number, which corresponds to their number in [XML Path Language (XPath) 2.0], and are marked with "(XPath)". For instance, the following production describes for expressions in XPath.

[For/FLWR] Expressions

XQuery Core grammar productions describe the XQuery Core. The Core grammar is given in [A Normalized core grammar]. Core productions are identified by a number, which corresponds to their number in [A Normalized core grammar], and are marked with "(Core)". For instance, the following production describes the simpler form of the "FLWOR" expression in the XQuery Core.

Core FLWOR Expressions

The Formal Semantics manipulates "objects" (values, types, expressions, etc.) for which there is no existing grammar production in the [XQuery 1.0: A Query Language for XML] document. In these cases, specific grammar productions are introduced. Notably, additional productions are used to describe values in the [Data Model], and to describe the [XPath/XQuery] type system. Formal Semantics productions are identified by a number, and are marked by "(Formal)". For instance, the following production describes global type definitions in the [XPath/XQuery] type system.

Type Definitions

Note that grammar productions that are specific to the Formal Semantics (i.e., marked with "(Formal)") are not part of [XPath/XQuery]. They are not accessible to the user and are only used in the course of defining the languages' semantics.

Grammar non-terminals are used extensively in this document to represent objects in inference rules (see the next section). As a convenience, non-terminals used in inference rules link to the appropriate grammar production.

2.1.2 Notations for judgments

The basic building block of the formal specification is called a judgment. A judgment expresses whether a property holds or not.

For example:

Notation

The judgment

holds if the object Painting is beautiful.

Notation

Here are three judgments that are used extensively in this document.

The judgment

holds if the expression Expr yields (or evaluates to) the value Value.

The judgment

holds when the expression Expr has the type Type.

Most other judgments used in this document are short english sentences intended to reflect their meaning, and written in bold fonts. For instance, the judgment

holds when the expression Expr raises the error Error.

A judgment can contain symbols and patterns.

Symbols are purely syntactic and are used to write the judgment itself. In general, symbols in a judgment are chosen to reflect its meaning. For example, 'is beautiful', '=>' and ':' are symbols, the second and third of which should be read "yields", and "has type" respectively.

Patterns are written with italicized words. The name of a pattern is significant: each pattern name corresponds to an "object" (a value, a type, an expression, etc.) that can be substituted legally for the pattern. By convention, all patterns in the Formal Semantics correspond to grammar non-terminals, and are used to represent entities that can be constructed through application of the corresponding grammar production. For example, Expr represents any [XPath/XQuery] expression, and Value represents any value in the [XPath/XQuery] data model.

When applying the judgment, each pattern must be instantiated to an appropriate sort of "object" (value, type, expression, etc). For example, '3 => 3' and '$x+0 => 3' are both instances of the judgment 'Expr => Value'. Note that in the first judgment, '3' corresponds to both the expression '3' (on the left-hand side of the => symbol) and to the the value '3' (on the right-hand side of the => symbol).

Patterns may appear with subscripts (e.g. Expr₁, Expr₂) to distinguish different instances of the same sort of pattern. Each distinct pattern must be instantiated to a single "object" (value, type, expression, etc.). If the same pattern occurs twice in a judgment description then it should be instantiated with the same "object". For example, '3 => 3' is an instance of the judgment 'Expr₁ => Expr₁' but '$x+0 => 3' is not since the two expressions '$x+0' and '3' cannot be both instance of the pattern Expr₁. The judgment'$x+0 => 3' is an instance of the judgment 'Expr₁ => Expr₂'.

Patterns may have a name that is not exactly the name of a grammar production but is based on it. For instance, a BaseTypeName is a pattern that stands for a type name, as would TypeName, or TypeName₂. This usage is limited, and only occurs to improve the readability of some of the inference rules.

In some cases, inference rules may need to use the fact that a certain judgment does not hold. We may write not(Judgment) the judgment which holds iff Judgment does not hold.

In some cases, an "object" may take a value within a finite set of pre-determined values. We may write those set of possible value using the in judgment. For instance, the judgment

which holds, if the object Color has either the value blue or the value green.

2.1.3 Notations for inference rules

Inference rules are used to specify whether a judgment holds or not. Inference rules express the logical relation between judgments and describe how complex judgments can be concluded from simpler premise judgments.

A logical inference rule is written as a collection of premises and a conclusion, written respectively above and below a dividing line:

All premises and the conclusion are judgments. The interpretation of an inference rule is: if all the premise judgments above the line hold, then the conclusion judgment below the line must also hold.

Here is a simple example of inference rule, which uses the example judgment 'Expr => Value' from above:

This inference rule expresses the following property of the judgment 'Expr => Value': if the variable expression '$x' yields the value '0', and the literal expression '3' yields the value '3', then the expression '$x + 3' yields the value '3'.

An inference rule may have no premises above the line, which means that the expression below the line always holds:

This inference rule expresses the following property of the judgment 'Expr => Value': evaluating the literal expression '3' always yields the value '3'.

The two above rules are expressed in terms of specific variables and values, but usually rules are more abstract. That is, the judgments they relate contain patterns. Here is a rule that says that for any variable Variable that yields the integer value Integer, adding '0' yields the same integer value:

As in a judgment, each pattern in a particular inference rule must be instantiated to the same "object" within the entire rule. This means that one can talk about "the value of Variable" instead of the more precise "what Variable is instantiated to in (this particular instantiation of) the inference rule".

2.1.4 Notations for environments

Logical inference rules use environments to record information computed during static type analysis or dynamic evaluation so that this information can be used by other logical inference rules. For example, the type signature of a user-defined function in a [expression/query] prolog can be recorded in an environment and used by subsequent rules. Similarly, the value assigned to a variable within a "let" expression can be captured in an environment and accessed later on during evaluation when that variable is accessed.

An environment is a dictionary that maps a symbol (e.g., a function name or a variable name) to an "object" (e.g., a function body, a type, a value). One can access information in an environment or update the environment.

If "env" is an environment, then "env(symbol)" denotes the "object" to which symbol is mapped. The notation is intentionally similar to function application, because an environment can be considered a function from the argument symbol to the "object" to which the symbol is mapped.

This document uses environment groups that group related environments. If "group" is an environment group with the environment component "env", then that environment is denoted "group.env" and the value that symbol is mapped to is denoted "group.env(symbol)".

The two main environment groups used in the Formal Semantics are: a dynamic environment group (dynEnv), which models to the [XPath/XQuery]'s dynamic context, and a static environment group (statEnv), which models the [XPath/XQuery]'s static context. Both are defined in [3.1 Expression Context].

For example, dynEnv.varValue denotes the dynamic environment that maps variables to values and dynEnv.varValue(Variable) denotes the value of the variable Variable in the dynamic context.

Environment groups are used in a judgment to capture some of the context in which the judgment is computed, and most judgments are computed assuming that some environment is given. This assumption is denoted by prefixing the judgment with "env |-". The "|-" symbol is called a "turnstile" and is used in almost all inference rules.

For instance, the judgment

is read as: Assuming the dynamic environment group dynEnv, the expression Expr yields the value Value.

Environment groups can be updated, using the following notation:

• "group + env(symbol => object) " denotes the new environment group that is identical to group except that the env environment has been updated to map symbol to object. The notation symbol => object indicates that symbol is mapped to object in the new environment.

• The following shorthand is also allowed: "group + env( symbol₁ => object₁ ; ... ; symbol_n => object_n ) " in which each symbol is mapped to a corresponding object in the new environment.

  This notation is equivalent to nested updates, as in " (group + env( symbol₁ => object₁) + ... ) + env(symbol_n => object_n)".

Updating an environment creates a copy of the original environment and overrides any previous binding that might exist for the same name and the same group in that environment. Updating the environment is used to capture the scope of a symbol (e.g., for variables, namespace prefixes, etc). For instance, in the following expression

  let $x := 1 return
  let $x := $x + 2 return
  $x - 3

each let expression changes the dynamic context by binding a new variable to a new value. Each different context is represented by a different environment. The original environment, in which the expression 1 is evaluated, does not contain any binding for variable $x. This environment is updated a first time with a binding of variable $x to the value 1, and this environment is used for the evaluation of the expression $x + 2. Then it is updated a second time with a binding of variable $x to the value 3, and this environment is used for the evaluation of the expression$x - 3.

Also, note that there are no operations to remove entries from environments. This is never necessary as updating an environment effectively creates a new extended copy of the original environment, leaving the original environment accessible wherever it is in scope along with the updated copy.

2.1.5 Putting it together

Putting the above notations together, here is an example of an inference rule that occurs later in this document:

This rule is read as follows: if two expressions Expr₁ and Expr₂ are known to have the static types types Type₁ and Type₂ (the two premises above the line), then it is the case that the expression below the line "Expr₁ , Expr₂" must have the static type "Type₁, Type₂", which is the sequence of types Type₁ and Type₂. The above inference rule does not modify the (static) environment.

The following rule defines the static semantics of a "let" expression. The binding of the new variable is captured by an update to the varType component of the original static environment.

This rule is read as follows: First, because the variable is a QName, it is first expanded into an expanded QName. Second, the type Type₁ for the "let" input expression Expr₁ is computed. Then the "let" variable with expanded name, expanded-QName with type Type₁ is added into the varType component of the static environment group statEnv. Finally, the type Type₂ of Expr₂ is computed in that new environment.

Each inference rule describes a fragment of the semantics for a given expression. Here is how those rules are combined. Consider the following expression.

  let $x := 1 return ($x,$x)

We have just seen the static typing rule for the let clause and sequence construction. To handle this expression completely, we need inference rules for integer literals and variable access. Those two rules are as follows.

With this set of rules, we can compute the type of the expression above in a bottom-up fashion, i.e., starting with the sub-expressions. The resulting type inference proceeds as follows.

  statEnv0 = ()

  statEnv0 |- 1 : xs:integer

  statEnv1 = ($x -> 1)

     statEnv1 |- $x : xs:integer
     statEnv1 |- $x : xs:integer
     statEnv1 |- ($x,$x) : xs:integer,xs:integer

  statEnv0 |- let $x := 1 return ($x,$x) : xs:integer,xs:integer

This example illustrates how each rule is applied to individual sub-expressions, and how the environment is used to maintain the relevant context information.

2.3.1 Formal values

A value is a sequence of zero or more items. An item is either an atomic value or a node.

An atomic value is a value in the value space of an atomic type, labeled with the name of that atomic type. An atomic type is either a primitive or derived atomic type according to XML Schema [Schema Part 2], xdt:untypedAtomic, or xdt:anyAtomicType.

A node is either an element, an attribute, a document, a text, a comment, or a processing-instruction node.

Element nodes have a type annotation^XQ and contain a complex value or a simple value. Attribute nodes have a type annotation^XQ and contain a simple value. Text nodes always contain one string value of type xdt:untypedAtomic, therefore the corresponding type annotation is omitted in the formal notation of a text node. Document nodes do not have a type annotation and contain a sequence of element, text, comment, or processing-instruction nodes.

A simple value is a sequence of atomic values.

A complex value is a sequence of attribute nodes followed by a sequence of element, text, comment, or processing-instruction nodes.

A type annotation^XQ can be either the QName of a declared type or an anonymous type. An anonymous type corresponds to an XML Schema type for which the schema writer did not provide a name. Anonymous type names are not visible to the user, but are generated during schema validation and used to annotate nodes in the data model. By convention, anonymous type names are written using the fs: Formal Semantics prefix: fs:anon₀, fs:anon₁, etc.

Formal values are defined by the following grammar.

Values

Notation

In that grammar, "String" indicates the value space of xs:string, "Decimal" indicates the value space of xs:decimal, etc.

Element (resp. attributes) without type annotations, are assumed to have the type annotation xs:anyType (resp. xs:anySimpleType). Atomic values without type annotations, are assumed to have a type annotation which is the base type for the corresponding value. For instance, "Hello, World!" is equivalent to "Hello, World!" of type xs:string.

Untyped elements (e.g., from well-formed documents) have the type annotation^XQ xdt:untyped, untyped attributes have the type annotation^XQ xdt:untypedAtomic, and untyped atomic values have the type annotation^XQ xdt:untypedAtomic.

An element has an optional "nilled" marker. This marker can only be present if the element has been validated against an element type in the schema which is "nillable", and the element has no content and an attribute xsi:nil set to "true".

An element also has a sequence of namespace bindings, which are the set of in-scope namespaces for that element. Each namespace binding is a prefix, URI pair. Elements without namespace bindings are assumed to have an empty set of in-scope namespaces.

In examples, we omit the namespace bindings when they are empty. For example, the following two values are the same (note that the xs and xdt prefixes are built-in):

  element weight of type xs:integer { text { "42" } } {}
  element weight of type xs:integer { text { "42" } } 

The same rule about constructing sequences apply to the values described by that grammar. Notably sequences are automatically flattened. For example, the sequence (10, (1, 2), (), (3, 4)) is equivalent to the sequence (10, 1, 2, 3, 4).

When the context is clear, we may omit the type annotation^XQ on literal values. For instance:

  "Hello World!"   instead of   "Hello World!" of type xs:string
  10               instead of   10 of type xs:integer

2.3.2 Examples of values

A well-formed document

  <fact>The cat weighs <weight units="lbs">12</weight> pounds.</fact>

In the absence of a Schema, this document is represented as

  element fact of type xdt:untyped {
    text { "The cat weighs " },
    element weight of type xdt:untyped {
      attribute units of type xdt:untypedAtomic {
        "lbs" of type xdt:untypedAtomic
      }
      text { "12" }
    },
    text { " pounds." }
  }

A document before and after validation.

  <weight xsi:type="xs:integer">42</weight>

The formal model for values can represent values before and after validation. Before validation, this element is represented as:

  element weight of type xdt:untyped {
    attribute xsi:type of type xdt:untypedAtomic {
      "xs:integer" of type xdt:untypedAtomic
    },
    text { "42" }
  }

After validation, this element is represented as:

  element weight of type xs:integer {
    attribute xsi:type of type xs:QName {
      "xs:integer" of type xs:QName
    },
    42 of type xs:integer
  }

An element with a list type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 2 3" }
  }

Assume the following Schema.

  <xs:element name="sizes" type="sizesType"/>
  <xs:simpleType name="sizesType">
    <xs:list itemType="sizeType"/>
  </xs:simpleType>
  <xs:simpleType name="sizeType">
    <xs:restriction base="xs:integer"/>
  </xs:simpleType>

After validation against this Schema, the element is represented as:

  element sizes of type sizesType {
    1 of type sizeType,
    2 of type sizeType,
    3 of type sizeType
  }

An element with an anonymous type

  <sizes>1 2 3</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 2 3" }
  }

Assume the following Schema.

  <xs:element name="sizes">
    <xs:simpleType>
      <xs:list itemType="xs:integer"/>
    </xs:simpleType>
  </xs:element>

After validation, this element is represented as:

  element sizes of type fs:anon1 {
    1 of type xs:integer,
    2 of type xs:integer,
    3 of type xs:integer
  }

where fs:anon₁ stands for the internal anonymous name generated by the system for the sizes element.

An nillable element with xsi:type set to true:

  <sizes xsi:nil="true"/>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    attribute xsi:nil of type xdt:untypedAtomic { "true" as xdt:untypedAtomic }
  }

Assume the following Schema.

  <xs:element name="sizes" type="sizesType" nillable="true"/>

After validation against this Schema, the element is represented as:

  element sizes nilled of type sizesType {
    attribute xsi:nil of type xs:boolean { true as xs:boolean }
  }

An element with a union type

  <sizes>1 two 3 four</sizes>

Before validation, this element is represented as:

  element sizes of type xdt:untyped {
    text { "1 two 3 four" }
  }

Assume the following Schema:

  <xs:element name="sizes" type="sizesType"/>
  <xs:simpleType name="sizesType">
    <xs:list itemType="sizeType"/>
  </xs:simpleType>
  <xs:simpleType name="sizeType">
    <xs:union memberType="xs:integer xs:string"/>
  </xs:simpleType>

After validation against this Schema, the element is represented as:

  element sizes of type sizesType {
    1 of type xs:integer,
    "two" of type xs:string,
    3 of type xs:integer,
    "four" of type xs:string
  }

2.4.1 XML Schema and the [XPath/XQuery] Type System

The [XPath/XQuery] type system is based on [Schema Part 1] and [Schema Part 2]. [Schema Part 1] and [Schema Part 2] specify normatively the type information available in [XPath/XQuery]. We define the formal notation that is used in this document to describe and manipulate types in inference rules. Formal types are used for specification purposes only and are not exposed to the [XPath/XQuery] user.

Representation of content models. For the purpose of static typing, the [XPath/XQuery] type system only describes minOccurs, maxOccurs, and minLength, maxLength on list types for the occurrences that correspond to the DTD operators +, *, and ?. Choices are represented using the DTD operator |. All groups are represented using the interleaving operator (&).

Representation of anonymous types. To clarify the semantics, the [XPath/XQuery] type system makes all anonymous types explicit.

Representation of XML Schema simple type facets and identity constraints. For simplicity, XML Schema simple type facets and identity constraints are not formally represented in the [XPath/XQuery] type system. However, an [XPath/XQuery] implementation supporting XML Schema import and validation must must take simple type facets and identity constraints into account.

The mapping from XML Schema into the [XPath/XQuery] type system is given in [C Importing Schemas]. The rest of this section is organized as follows. [2.4.2 Item types] describes types items, [2.4.3 Content models] describes content models, and [2.4.4 Top level definitions] describe top-level type declarations.

2.4.2 Item types

An item type is either an atomic type, an element type, an attribute type, a document node type, a text node type, a comment node type, or a processing instruction type. We distinguish between document nodes, attribute nodes, and nodes that can occur in element content (elements, comments, processing instructions, and text nodes), as we need to refer to element content types later in the formal semantics.

Item Types

An element or attribute type has an optional name and an optional type reference. A name alone corresponds to a reference to a global element or attribute declaration. A name with a type reference corresponds to a local element or attribute declaration. The word "element" or "attribute" alone refers to the wildcard types for any element or any attribute. In addition, an element type has an optional nillable flag that indicates whether the element can be nilled or not.

A document type has an optional content type. If no content type is given, then the type is treated as being the wildcard type for documents, i.e., a sequence of text and element nodes. For consistency with element nodes, PIs and comments are not indicated in that wildcard type, but may occur in instances.

Note

Generic node types (e.g., node()) such as used in the SequenceType production, are interpreted in the type system as union types (e.g., element | attribute | text | comment | processing-instruction) and therefore do not appear here. The semantics of sequence types is described in [3.5.4 SequenceType Matching].

Examples

The following is a text node type

  text

The following is a type for all elements

  element

The following is a type for all elements of type string

  element of type xs:string

The following is a type for a nillable element of type string and with name size

  element size nillable of type xs:string

The following is a reference to a global attribute declaration

  attribute sizes

The following is a type for elements with anonymous type fs:anon₁:

  element sizes of type fs:anon1

2.4.3 Content models

Following XML Schema, types in [XPath/XQuery] are composed from item types by optional, one or more, zero or more, all group, sequence, choice, empty sequence (written empty), or empty choice (written none).

The type empty matches the empty sequence. The type none matches no values. none is the identity for choice, that is (Type | none) = Type)). The type none is the static type for [7.2.9 The fn:error function].

Types

The [XPath/XQuery] type system includes three binary operators on types: ",", "|" and "&", corresponding respectively to sequence, choice and all groups in Schema. The [XPath/XQuery] type system includes three unary operators on types: "*", "+", and "?", corresponding respectively to zero or more instances of the type, one or more instances of the type, or an optional instance of the type.

The "&" operator builds the "interleaved product" of two types. The type Type₁ & Type₂ matches any sequence that is an interleaving of a sequence that matches Type₁ and a sequence that matches Type₂. The interleaved product captures the semantics of all groups in XML Schema, but it more general has it applies to arbitrary types. All groups in XML Schema are restricted to apply only on global or local element declarations with minOccurs 0 or 1, and maxOccurs 1.

The "&" operator builds the "interleaved product" of two types. The type Type₁ & Type₂ matches any sequence that is an interleaving of two sequences of items, the first one matching Type1 and the second matching Type2. Where the interleaving of two sequences of items Value₁ and Value₂ is any sequence Value₀ such that there is an ordered partition of Value₀ into the two sub-sequences Value₁ and Value₂.

For example, consider the types Type₁ = xs:integer,xs:integer,xs:integer and Type₂ = xs:string,xs:string. Value₁ = (1,2,3) matches the type Type₁ and Value₂ = ("a","b") matches the type Type₂. Any of the following Value₀ are interleavings of Value₁ and Value₂, and therefore match the type (Type₁ & Type₂):

Value0 = (1,2,3,"a","b")
Value0 = (1,2,"a",3,"b")
Value0 = (1,2,"a","b",3)
Value0 = (1,"a",2,3,"b")
Value0 = (1,"a",2,"b",3)
Value0 = (1,"a","b",2,3)
Value0 = ("a",1,2,3,"b")
Value0 = ("a",1,2,"b",3)
Value0 = ("a",1,"b",2,3)
Value0 = ("a","b",1,2,3)

Types precedence order. To improve readability when writing types, we assume the following precedence order between operators on types.

Parenthesis can be used to enforce precedence. For instance

  xs:string | xs:integer, xs:float*

is equivalent to

  xs:string | (xs:integer, (xs:float*))

and a different precedence can be obtained by writing

  ((xs:string | xs:integer), xs:float)*

Examples

A sequence of elements

The "," operator builds the "sequence" of two types. For example,

  element title of type xs:string, element year of type xs:integer

is a sequence of an element title of type string followed by an element year of type integer.

The union of two element types

The "|" operator builds the "union" of two types. For example,

  element editor of type xs:string | element bib:author

means either an element editor of type string, or a reference to the global element bib:author.

An all group of two elements

The "&" operator builds the "interleaved product" of two types. For example,

  (element a & element b) =
    element a, element b
  | element b, element a

which specifies that the a and b elements can occur in any order.

An empty type

The following type matches the empty sequence.

  empty

A sequence of zero or more elements

The following type matches zero or more elements each of which can be a surgeon or a plumber.

  (element surgeon | element plumber)*

2.4.4 Top level definitions

Top level definitions correspond to global element declarations, global attribute declarations and type definitions in XML Schema.

Type Definitions

A type definition has a name (possibly anonymous) and a type derivation. In the case of a complex type, or a simple type derived by list or union, derivation indicates if the type is derived by extension or restriction from its base type, gives its content model, and an optional flag indicating if it has mixed content. In the case of an atomic type, it just indicates from which type it is derived. When the type derivation is omitted, the type derives by restriction from xs:anyType, as in:

  define type Bib { element book* } =
  define type Bib restricts xs:anyType { element book* }

Empty content can be indicated with the explicit empty sequence, or omitted, as in:

  define type Bib { } =
  define type Bib { empty }

Global element and attribute declarations always have a name and a reference to a (possibly anonymous) type. A global element declaration also may declare a substitution group for the element and whether the element is nillable.

Examples

A type declaration with one element name of type xs:string follows by one or more elements street of type xs:string.

  define type Address {
    element name of type xs:string,
    element street of type xs:string*
  }

A type declaration with complex content derived by extension

  define type USAddress extends Address {
    element zip name of type xs:integer
  }

A type declaration with mixed content

  define type Section mixed {
    (element h1 of type xs:string |
     element p of type xs:string |
     element div of type Section)*
  }

A type declaration with simple content derived by restriction

  define type SKU restricts xs:string

An element declaration

  define element address of type Address

An element declaration with a substitution group

  define element usaddress substitutes for address of type USAddress

An element declaration which is nillable

  define element zip nillable of type xs:integer

2.4.5 Example of a complete Schema

Here is a schema describing purchase orders from [XML Schema Part 0].

  <xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
  
   <xsd:annotation>
    <xsd:documentation xml:lang="en">
     Purchase order schema for Example.com.
     Copyright 2000 Example.com. All rights reserved.
    </xsd:documentation>
   </xsd:annotation>
  
   <xsd:element name="purchaseOrder" type="PurchaseOrderType"/>
  
   <xsd:element name="comment" type="xsd:string"/>
  
   <xsd:complexType name="PurchaseOrderType">
    <xsd:sequence>
     <xsd:element name="shipTo" type="USAddress"/>
     <xsd:element name="billTo" type="USAddress"/>
     <xsd:element ref="comment" minOccurs="0"/>
     <xsd:element name="items"  type="Items"/>
    </xsd:sequence>
    <xsd:attribute name="orderDate" type="xsd:date"/>
   </xsd:complexType>
  
   <xsd:complexType name="USAddress">
    <xsd:sequence>
     <xsd:element name="name"   type="xsd:string"/>
     <xsd:element name="street" type="xsd:string"/>
     <xsd:element name="city"   type="xsd:string"/>
     <xsd:element name="state"  type="xsd:string"/>
     <xsd:element name="zip"    type="xsd:decimal"/>
    </xsd:sequence>
    <xsd:attribute name="country" type="xsd:NMTOKEN" fixed="US"/>
   </xsd:complexType>
  
   <xsd:complexType name="Items">
    <xsd:sequence>
     <xsd:element name="item" minOccurs="0" maxOccurs="unbounded">
      <xsd:complexType>
        <xsd:sequence>
         <xsd:element name="productName" type="xsd:string"/>
         <xsd:element name="quantity">
          <xsd:simpleType>
           <xsd:restriction base="xsd:positiveInteger">
            <xsd:maxExclusive value="100"/>
           </xsd:restriction>
          </xsd:simpleType>
         </xsd:element>
         <xsd:element name="USPrice"  type="xsd:decimal"/>
         <xsd:element ref="comment"   minOccurs="0"/>
         <xsd:element name="shipDate" type="xsd:date" minOccurs="0"/>
        </xsd:sequence>
        <xsd:attribute name="partNum" type="SKU" use="required"/>
      </xsd:complexType>
     </xsd:element>
    </xsd:sequence>
   </xsd:complexType>
  
   <!-- Stock Keeping Unit, a code for identifying products -->
   <xsd:simpleType name="SKU">
    <xsd:restriction base="xsd:string">
     <xsd:pattern value="\d{3}-[A-Z]{2}"/>
    </xsd:restriction>
   </xsd:simpleType>
  
  </xsd:schema>

Here is the mapping of the above schema into the [XPath/XQuery] type system.

  declare namespace xsd = "http://www.w3.org/2001/XMLSchema";

  define element purchaseOrder of type PurchaseOrderType;
 
  define element comment of type xsd:string;
  
  define type PurchaseOrderType {
    attribute orderDate of type xsd:date?,
    element shipTo of type USAddress,
    element billTo of type USAddress,
    element comment?,
    element items of type Items
  };

  define type USAddress {
    attribute country of type xsd:NMTOKEN,
    element name of type xsd:string,
    element street of type xsd:string,
    element city of type xsd:string,
    element state of type xsd:string,
    element zip of type xsd:decimal
  };

  define type Items {
    attribute partNum of type SKU,
    element item of type fs:anon1*
  };

  define type fs:anon1 {
    element productName of type xsd:string,
    element quantity of type fs:anon2,
    element USPrice of type xsd:decimal,
    element comment?,
    element shipDate of type xsd:date?
  };

  define type fs:anon2 restricts xsd:positiveInteger;

  define type SKU restrict xsd:string;

Note that the two anonymous types in the item element declarations are mapping to types with names fs:anon₁ and fs:anon₂.

The following additional definitions illustrate how more advanced XML Schema features (a complex type derived by extension, an anonymous simple type derived by restriction, and substitution groups) are represented in the [XPath/XQuery] type system.

  <complexType name="NYCAddress">
    <complexContent>
     <extension base="USAddress">
      <sequence>
       <element ref="apt"/>
      </sequence>
     </extension>
    </complexContent>
  </complexType>

  <element name="apt">
    <xsd:simpleType>
     <xsd:restriction base="xsd:positiveInteger">
      <xsd:maxExclusive value="10000"/>
     </xsd:restriction>
    </xsd:simpleType>
  </element>

  <element name="usaddress" substitutionGroup="address" type="USAddress"/>
  <element name="nycaddress" substitutionGroup="usaddress" type="NYCAddress"/>

The above definitions are mapped into the [XPath/XQuery] type system as follows:

  define type NYCAddress extends USAddress {
    element apt
  }

  define element apt of type fs:anon3

  define type fs:anon3 restricts xsd:positiveInteger

  define element usaddress  substitutes for address of type USAddress
  define element nycaddress substitutes for usaddress of type NYCAddress

3.1.1 Static Context

The environment group statEnv denotes the environments that are available during static analysis. Static analysis may extend parts of the static environment. The static environment is also available during dynamic evaluation.

If analysis of an expression relies on some component of the static context that has not been assigned a value, a static error is raised. This constraint is formalized in [3.3 Error Handling].

The following environments are part of the static environment group: