\documentclass{article}
\usepackage{fuzz}
\usepackage[pdftitle={Formal Specification of WSDL 2.0}, pdfauthor={Arthur Ryman}]{hyperref}

\title{Formal Specification of WSDL 2.0}
\author{Arthur Ryman}
\date{\today}

\begin{document}

\maketitle

\section*{Abstract}

This document is a formal specification of 
\href{http://www.w3.org/TR/wsdl20/}{WSDL 2.0}.
The main goal of this document is to ensure that the text of the W3C
specification for WSDL 2.0 is complete, precise, and unambiguous. 
By translating the English statements of the W3C specification into formal
mathematical statements, problems in the English text will be exposed and corrected.

The formal specification language, Z Notation, is used for the mathematical statements.
One advantage of Z Notation is that it can be automatically type checked, a process
which eliminates many common specification errors, thereby improving the quality
of the specification.

Another goal of this document is to serve as a Test Assertion Document (TAD)
which will be used by software that validates WSDL documents. 
A test assertion is a constraint or rule that a WSDL document must satisfy in order to be
compliant with the specification.
Test assertions can be manually translated into an executable programming language
such as Java or C\#.

\clearpage

\section{Introduction}

This document is a formal specification of WSDL 2.0. 
Its purpose is to help improve the quality of the informal specification and to provide a set
of precise test assertions that can be checked by WSDL validators.

\subsection{Component Models, Infosets, and Documents}

The WSDL specification is organized into two levels of abstraction: Component Model and XML Infoset. 
The most abstract level is the Component Model which describes a set of Web services in terms of abstract components
such as interface, binding, and service.
The Component Model is almost completely independent of XML, the only exception being the use of XML data types such as NCName.

The XML Infoset level introduces a more concrete representation of the Component Model as a set of interrelated infosets.
The use of infosets retains a level of abstraction above that of concrete XML documents, however we will abuse language
a little and use the terms infoset and document interchangeably. 
No confusion will result since the WSDL specification only deals with infosets.

\subsection{Intradocument and Interdocument Constraints}

The correctness of a WSDL 2.0 document can only be determined by examining both the document itself
and any other documents that it includes or imports.
It is therefore natural to divide the set of rules that must be satisfied into those that define the internal
consistency of documents and those that define the mutual consistency of sets of related documents.
We will refer to rules that define the internal consistency of documents as {\em intradocument rules} and
those that define the consistency of mutually related documents as {\em interdocument rules}.

Furthermore, when considering intradocument rules, it is natural to divide them into those that can be
readily expressed using XML Schema and those that cannot.
These will be refered to as intradocument schema rules and intradocument nonschema rules.

The formal specification will be built up as follows.
First we will define the abstract Component Model.
Next, we will describe the XML infoset that corresponds to a single WSDL document.
The intradocument schema rules will be defined as a set of test assertions on the infoset.
In practice, these rules will be checked by a validating XML parser using the normative WSDL schema.
However, the test assertions will serve as a useful check on the correctness of the normative WSDL schema.

Next, we will define how a set of schema valid infosets defines a component model.
We will define the intradocument nonschema rules and the interdocument rules 
as a set of test assertions on the abstract component model.

\section{Component Model}

The WSDL specification describes the abstract component model for a Web servce description as a set of components
with properties.

\begin{axdef}
	NamespaceURI, AbsoluteURI : \power URI
\end{axdef}

\begin{schema}{QName}
	localName : NCName \\
	namespaceName : NamespaceURI
\end{schema}

\begin{zed}
	OptionalQName ::= \\
	\t1	noValueQName | \\
	\t1	valueQName \ldata QName \rdata
\end{zed}

\subsection{Type System Components}

\begin{schema}{ElementDeclarationComponent}
	qName : QName
\end{schema}

\begin{schema}{FeatureComponent}
	name : AbsoluteURI \\
	required : Boolean
\end{schema}

\begin{axdef}
	XsAnyType : \power String
\end{axdef}

\begin{zed}
	OptionalXsAnyType ::= \\
	\t1	noValueXsAnyType | valueXsAnyType \ldata XsAnyType \rdata
\end{zed}

\begin{schema}{PropertyComponent}
	name : AbsoluteURI \\
	required : Boolean \\
	valueConstraint : QName \\
	value : OptionalXsAnyType
\end{schema}

\subsection{The Interface Component}

\subsubsection{InterfaceComponent}

\begin{schema}{InterfaceFaultComponent}
	name : NCName \\
	element : QName
\end{schema}

\begin{zed}
	Direction ::= in | out
\end{zed}

\begin{zed}
	MessageContentModel ::= none | any | element
\end{zed}

\begin{schema}{MessageReferenceComponent}
	messageLabel : NCName \\
	direction : Direction \\
	messageContentModel : MessageContentModel \\
	element : OptionalQName
\end{schema}

\begin{schema}{FaultReferenceComponent}
	messageLabel : NCName \\
	direction : Direction \\
	faultReference : QName
\end{schema}

\begin{schema}{InterfaceOperationComponent}
	name : NCName \\
	targetNamespace : NamespaceURI \\
	messageExchangePattern : AbsoluteURI \\
	messageReferences : \finset MessageReferenceComponent \\
	faultReferences : \finset FaultReferenceComponent \\
	style : AbsoluteURI \\
	safety : OptionalBoolean \\
	features : \finset FeatureComponent \\
	properties : \finset PropertyComponent
\end{schema}

\begin{schema}{InterfaceComponent}
	name : NCName \\
	targetNamespace : URI \\
	extendedInterfaces : \finset QName \\
	faults : \finset InterfaceFaultComponent \\
	operations : \finset InterfaceOperationComponent \\
	features : \finset FeatureComponent \\
	properties : \finset PropertyComponent
\end{schema}

\begin{schema}{BindingFaultComponent}
	faultReference : QName
\end{schema}

\begin{schema}{BindingMessageReferenceComponent}
	messageLabel : NCName \\
	direction : Direction
\end{schema}

\begin{schema}{BindingOperationComponent}
	operationReference : QName \\
	messageReferences : \finset BindingMessageReferenceComponent \\
	features : \finset FeatureComponent \\
	properties : \finset PropertyComponent
\end{schema}

\begin{schema}{BindingComponent}
	name : NCName \\
	targetNamespace : NamespaceURI \\
	interface : OptionalQName \\
	type : AbsoluteURI \\
	faults : \finset BindingFaultComponent \\
	operations : \finset BindingOperationComponent \\
	features : \finset FeatureComponent \\
	properties : \finset PropertyComponent
\where
	\forall f1, f2 : faults @ \\
	\t1	f1.faultReference = f2.faultReference \implies f1 = f2
\end{schema}
There is at most one binding for each fault.

\begin{schema}{EndpointComponent}
	name : NCName \\
	binding : QName \\
	address : OptionalURI
\where
	address = noValueURI \lor \\
	\t1	(\exists uri : AbsoluteURI @ address = valueURI~uri)
\end{schema}
If the address is present it must be an absolute URI.

\begin{schema}{ServiceComponent}
	name : NCName \\
	targetNamespace : NamespaceURI \\
	interface : QName \\
	endpoints : \finset EndpointComponent
\where
	\forall e1, e2 : endpoints @ \\
	\t1	e1.name = e2.name \implies e1 = e2
\end{schema}
Each endpoint has a unique name.

\subsection{The Definitions Component}

\subsubsection{DefinitionsComponent}

\begin{schema}{DefinitionsComponent}
	interfaces : \finset InterfaceComponent \\
	bindings : \finset BindingComponent \\
	services : \finset ServiceComponent \\
	elementDeclarations : \finset ElementDeclarationComponent
\end{schema}

\subsection{Comments on the WSDL Specification}

Several components, such as Service, Interface, have a property named targetNamespace. 
However, I think this is a misnomer because the property is really the namespace name of the component.
The term target namespace makes sense in the context of an XML document that is defining components, but after the
components have been defined, the target namespace of the document becomes the namespace name of the defined component.
A better name would be namespace name.

Similarly, several components have a name property, but this is really the local name of the QName used to identify the component.

\section{Intradocument Schema Rules}

This section defines the rules that a well-formed XML infoset must satisify to be a schema valid WSDL document.

\subsection{XML Schema Types}

This section introduces XML Schema types that are used in the WSDL schema.

\subsubsection{XsAnyURI}

Let $XsAnyURI$ be the set of values that correspond to the XML Schema type anyURI:
\begin{axdef}
	XsAnyURI : \power String
\end{axdef}

\subsection{The WSDL Namespace}

This section defines rules that apply to the WSDL namespace.

\subsubsection{WsdlNamespaceURI}

Let $WsdlNamespaceURI$ be the WSDL namespace URI:
\begin{axdef}
	WsdlNamespaceURI : URI
\end{axdef}

\subsubsection{WSDL Element Local Names}

Let the following be the local names of the WSDL element information items:
\begin{axdef}
	definitions, documentation, include, import, types, \\
	\t1 operation, interface, binding, service : NCName
\end{axdef}

Let $WsdlElementNames$ be the set of element local names that belong
to the WSDL namespace:
\begin{zed}
	WsdlElementNames == \\
	\t1	\{definitions, documentation, include, import, \\
	\t1	types, operation, interface, binding, service\}
\end{zed}

The local names are distinct:
\begin{zed}
	\# WsdlElementNames = 9
\end{zed}

\subsubsection{WSDL Attribute Local Names}

Let the following be the local names of the WSDL attribute information items:
\begin{axdef}
	targetNamespace : NCName
\end{axdef}

\subsubsection{AnyItem}

An infoset cursor is an infoset with a distinguished item identifier within that infoset.
Let $AnyItem$ be the set of all infoset cursors where the item is any item:
\begin{itemize}

\item Let $infoset$ be an infoset.

\item Let $id$ be an item identifier in the infoset.

\end{itemize}
\begin{schema}{AnyItem}
	infoset : Infoset \\
	id : II
\where
	id \in infoset.ids
\end{schema}
The identifier is in the infoset.

In the following sections we'll define infoset cursors that match progressively more specific types of item,
leading up to the XML Schema definitions of elements and attributes.
These definitions sometimes extend the base definition of infoset cursor with additional variables.
We can hide the additonal variables using the technique of projection onto the set of base infoset cursors.

\subsubsection{AnyElement1}

Let $AnyElement1$ be the set of all extended infoset cursors where the item is any element:

Let $item$ be the element item.
\begin{schema}{AnyElement1}
	AnyItem \\
	item : ElementItem
\where
	item.id = id
\end{schema}
The element item is the distinguished item.

\subsubsection{WsdlNamespaceElement1}

Let $WsdlNamespaceElement1$ be the set of all extended infoset cursors where the item is an element in the WSDL namespace:
\begin{schema}{WsdlNamespaceElement1}
	AnyElement1
\where
	item.namespaceName = valueURI~WsdlNamespaceURI
\end{schema}
The item is in the WSDL namespace.

\subsubsection{OtherNamespaceElement1}

Let $OtherNamespaceElement1$ be the set of all extended infoset cursors where the item is an element in a namespace other than
the WSDL namespace:

Let $uri$ be the element item namespace URI.
\begin{schema}{OtherNamespaceElement1}
	AnyElement1 \\
	uri : URI
\where
	item.namespaceName = valueURI~uri \\
	uri \neq WsdlNamespaceURI
\end{schema}
\begin{itemize}

\item The item is in a namespace.

\item The namespace is not the WSDL namespace.

\end{itemize}

\subsubsection{OtherNamespaceElement}

Let $OtherNamespaceElement$ be the set of all base other namespace element infoset cursors:
\begin{zed}
	OtherNamespaceElement \defs OtherNamespaceElement1 \project AnyItem
\end{zed}

\subsubsection{AnyAttribute1}

Let $AnyAttribute1$ be the set of all extended infoset cursors where the distinguished item is an attribute:

Let $item$ be the attribute item.
\begin{schema}{AnyAttribute1}
	AnyItem \\
	item : AttributeItem
\where
	item.id = id
\end{schema}
The attribute item is the distinguised item.

\subsubsection{NoNamepaceAttribute1}

Let $NoNamepaceAttribute1$ be the set of all extended attribute infoset cursors where the attribute does not have a namespace:
\begin{schema}{NoNamespaceAttribute1}
	AnyAttribute1
\where
	item.namespaceName = noValueURI
\end{schema}
The attribute has no namespace.

\subsubsection{OtherNamespaceAttribute1}

Let $OtherNamespaceAttribute1$ be the set of all extended attribute infoset cursors where the attribute has a namespace
other than the WSDL namespace:

Let $uri$ be the attribute namespace URI.
\begin{schema}{OtherNamespaceAttribute1}
	AnyAttribute1 \\
	uri : URI
\where
	item.namespaceName = valueURI~uri \\
	uri \neq WsdlNamespaceURI
\end{schema}
\begin{itemize}

\item The item has a namespace.

\item The namespace is not the WSDL namespace.

\end{itemize}

\subsubsection{OtherNamespaceAttribute}

Let $OtherNamespaceAttribute$ be the set of base other namespace attribute infoset cursors:
\begin{zed}
	OtherNamespaceAttribute \defs OtherNamespaceAttribute1 \project AnyItem
\end{zed}

\subsection{The documentation Element Information Item}

\subsubsection{DocumentationElement1}

Let $DocumentationElement1$ be the set of extended WSDL namespace infoset cursors that satisfy the
XML Schema rules for a documentation element:
\begin{schema}{DocumentationElement1}
	WsdlNamespaceElement1
\where
	item.localName = documentation \\
\also
	\ran item.children \subseteq infoset.elementIds \cup infoset.characterIds
\end{schema}
\begin{itemize}

\item The local name is documentation.

\item The children are either elements or characters.

\end{itemize}

\subsubsection{DocumentationElement}

Let $DocumentationElement$ be the set of base documentation element infoset cursors:
\begin{zed}
	DocumentationElement \defs DocumentationElement1 \project AnyItem
\end{zed}

\subsection{The include Element Information Item}

\subsubsection{IncludeElement1}

Let $IncludeElement1$ be the set of extended WSDL element infoset cursors that satisfy the
XML Schema rules for an include element:
\begin{schema}{IncludeElement1}
	WsdlNamespaceElement1
\where
	item.localName = include
\end{schema}
The local name is include.

\subsubsection{IncludeElement}

Let $IncludeElement$ be the set of all base include element infoset cursors:
\begin{zed}
	IncludeElement \defs IncludeElement1 \project AnyItem
\end{zed}

\subsection{The import Element Information Item}

\subsubsection(ImportElement1)

Let $ImportElement1$ be the set of all extended WSDL element infoset cursors that satisfy the
XML Schema rules for an import element:
\begin{schema}{ImportElement1}
	WsdlNamespaceElement1
\where
	item.localName = import
\end{schema}
The local name is import.

\subsubsection{ImportElement}

Let $ImportElement$ be the set of all base import element infoset cursors:
\begin{zed}
	ImportElement \defs ImportElement1 \project AnyItem
\end{zed}

\subsection{The types Element Information Item}

\subsubsection{TypesElement1}

Let $TypesElement1$ be the set of all extended WSDL element infoset cursors that satisfy the
XML Schema rules for a types element:
\begin{schema}{TypesElement1}
	WsdlNamespaceElement1
\where
	item.localName = types
\end{schema}
The local name is types.

\subsubsection{TypesElement}

Let $TypesElement$ be the set of all base types element infoset cursors:
\begin{zed}
	TypesElement \defs TypesElement1 \project AnyItem
\end{zed}

\subsection{The interface Element Information Item}

\subsubsection{InterfaceElement1}

Let $InterfaceElement1$ be the set of all extended WSDL infoset cursors that satify the
XML Schema rules for an interface element:
\begin{schema}{InterfaceElement1}
	WsdlNamespaceElement1
\where
	item.localName = interface
\end{schema}
The local name is interface.

\subsubsection{InterfaceElement}

Let $InterfaceElement$ be the set of all base interface element cursors:
\begin{zed}
	InterfaceElement \defs InterfaceElement1 \project AnyItem
\end{zed}

\subsection{The binding Element Information Item}

\subsubsection{BindingElement1}

Let $BindingElement1$ be the set of all extended WSDL element infoset cursors that satisfy the
XML Schema rules for a binding element:
\begin{schema}{BindingElement1}
	WsdlNamespaceElement1
\where
	item.localName = binding
\end{schema}
The local name is binding.

\subsubsection{BindingElement}

Let $BindingElement$ be the set of all base binding element infoset cursors:
\begin{zed}
	BindingElement \defs BindingElement1 \project AnyItem
\end{zed}

\subsection{The service Element Information Item}

\subsubsection{ServiceElement1}

Let $ServiceElement1$ be the set of all extended WSDL element infoset cursors that satisfy the
XML Schema rules for a service element:
\begin{schema}{ServiceElement1}
	WsdlNamespaceElement1
\where
	item.localName = service
\end{schema}
The local name is service.

\subsubsection{ServiceElement}

Let $ServiceElement$ be the set of all base service element infoset cursors:
\begin{zed}
	ServiceElement \defs ServiceElement1 \project AnyItem
\end{zed}

\subsection{The definitions Element Information Item}

\subsubsection{TargetNamespaceAttribute1}

Let $TargetNamespaceAttribute1$ be the set of extended non namespace attribute infoset cursors that satisfy the 
XML Schema rules for the targetNamespace attribute:
\begin{schema}{TargetNamespaceAttribute1}
	NoNamespaceAttribute1
\where
	item.localName = targetNamespace \\
	item.normalizedValue \in XsAnyURI
\end{schema}
\begin{itemize}

\item The local name is targetNamespace.

\item The normalized value of the attribute has the type xs:anyURI.

\end{itemize}

\subsubsection{TargetNamespaceAttribute}

Let $TargetNamespaceAttribute$ be the set of all base target namespace attribute infoset cursors:
\begin{zed}
	TargetNamespaceAttribute \defs TargetNamespaceAttribute1 \project AnyItem
\end{zed}

\subsubsection{DefinitionsElement1}

Let $DefinitionsElement1$ be the set of all extended WSDL element infoset cursors that satisfy the
XML Schema rules for a definitions element:
\begin{schema}{DefinitionsElement1}
	WsdlNamespaceElement1 \\
	targetNamespaceAttribute : TargetNamespaceAttribute \\
	otherAttributeIds : \finset AII \\
	documentationIds, fileIds, typesIds, componentIds : \iseq EII
\where
	item.localName = definitions
\also
	item.attributes = \\
	\t1 \{targetNamespaceAttribute.id\} \cup otherAttributeIds
\also
	\forall id : otherAttributeIds @ OtherNamespaceAttribute
\also
	item.children = \\
	\t1 documentationIds \cat fileIds \cat typesIds \cat componentIds
\also
	\# documentationIds \leq 1 \\
	\forall id : \ran documentationIds @ DocumentationElement
\also
	\forall id : \ran fileIds @ \\
	\t1	IncludeElement \lor \\
	\t1	ImportElement \lor \\
	\t1	OtherNamespaceElement
\also
	\# typesIds \leq 1 \\
	\forall id : \ran typesIds @ TypesElement
\also
	\forall id : \ran componentIds @ \\
	\t1	InterfaceElement \lor \\
	\t1	BindingElement \lor \\
	\t1	ServiceElement \lor \\
	\t1	OtherNamespaceElement
\end{schema}
\begin{itemize}

\item The local name is definitions.

\item There is a required target namespace attribute and zero or more other attributes.

\item The other attributes are from other namespaces.

\item The children consist of four subsequences. 

\item The first subsequence consists of an optional documentation element.

\item The second subsequence consists of zero or more include and import elements, and elements from other namespaces.

\item The third subsequence consists of an optional types element.

\item The fourth subsequence consists of zero or more interface, binding, and service elements, and elements from other namespaces.

\end{itemize}

\subsubsection{DefinitionsElement}

Let $DefinitionsElement$ be the set of all base definitions element infoset cursors:
\begin{zed}
	DefinitionsElement \defs DefinitionsElement1 \project AnyItem
\end{zed}

\subsubsection{WsdlInfoset}

The document element of a valid WSDL document must be a definitions element.

Let $WsdlInfoset$ be the set of all infosets that have a definitions element as the document element:
\begin{schema}{WsdlInfoset}
	Infoset
\where
	\LET infoset == \theta Infoset; id == documentElementItem.id @ \\
	\t1	DefinitionsElement
\end{schema}
The document element is a valid defintions element.

\end{document}
