- From: Arthur Ryman <aryman@dev.w3.org>
- Date: Fri, 12 Nov 2004 01:30:50 +0000
- To: public-ws-desc-eds@w3.org
Update of /sources/public/2002/ws/desc/wsdl20
In directory hutz:/tmp/cvs-serv24416
Modified Files:
.cvsignore
Added Files:
zml2latex.xsl wsdl20.tex
Log Message:
Added stylesheet to generate tex from xml.
Index: .cvsignore
===================================================================
RCS file: /sources/public/2002/ws/desc/wsdl20/.cvsignore,v
retrieving revision 1.4
retrieving revision 1.5
diff -C2 -d -r1.4 -r1.5
*** .cvsignore 9 Nov 2004 17:53:37 -0000 1.4
--- .cvsignore 12 Nov 2004 01:30:48 -0000 1.5
***************
*** 13,17 ****
*.aux
*.log
! *.out
! *.tex
! zml2latex.xsl
--- 13,15 ----
*.aux
*.log
! *.out
\ No newline at end of file
--- NEW FILE: zml2latex.xsl ---
<?xml version="1.0" encoding="UTF-8"?>
<!-- Version: $Id: zml2latex.xsl,v 1.1 2004/11/12 01:30:48 aryman Exp $ -->
<!-- Stylesheet for Z Markup Language (ZML) -->
<!-- Author: Arthur Ryman <ryman@ca.ibm.com> -->
<!-- Date Created: 2004-09-23 -->
<!--
This stylesheet is copyright (c) 2004 by its authors. Free
distribution and modification is permitted, including adding to
the list of authors and copyright holders, as long as this
copyright notice is maintained.
-->
<!--
This stylesheet transforms Z Notation to LaTeX.
The document must be marked up using ZML
which is in the namespace http://www.w3.org/2004/zml.
These tags correspond closely to the LaTeX commands
defined in the fuzz 2000 document style developed
by Mike Spivey and which is available at
http://spivey.oriel.ox.ac.uk/~mike/fuzz/.
-->
<!--
ChangeLog:
2004-10-16: Arthur Ryman <ryman@ca.ibm.com>
- modified to support W3C XML specification format
-->
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform" xmlns:z="http://www.w3.org/2004/zml">
<xsl:output method="text" encoding="UTF-8" indent="no" />
<xsl:preserve-space elements="*" />
<xsl:variable name="nl">
<xsl:text>
</xsl:text>
</xsl:variable>
<xsl:variable name="title">
<xsl:choose>
<xsl:when test="/html/head/title">
<xsl:value-of select="/html/head/title" />
</xsl:when>
<xsl:otherwise>
<xsl:text>Untitled</xsl:text>
</xsl:otherwise>
</xsl:choose>
</xsl:variable>
<xsl:variable name="author">
<xsl:choose>
<xsl:when test="/html/head/meta[@name='author']/@content">
<xsl:value-of select="/html/head/meta[@name='author']/@content" />
</xsl:when>
<xsl:otherwise>
<xsl:text>Anonymous</xsl:text>
</xsl:otherwise>
</xsl:choose>
</xsl:variable>
<xsl:variable name="date">
<xsl:choose>
<xsl:when test="/html/head/meta[@name='date']/@content">
<xsl:value-of select="/html/head/meta[@name='date']/@content" />
</xsl:when>
<xsl:otherwise>
<xsl:text>\today</xsl:text>
</xsl:otherwise>
</xsl:choose>
</xsl:variable>
<xsl:template match="/">
<xsl:text>\documentclass{article}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:text>\usepackage{fuzz}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:text>\usepackage[pdftitle={</xsl:text>
<xsl:value-of select="$title" />
<xsl:text>}, pdfauthor={</xsl:text>
<xsl:value-of select="$author" />
<xsl:text>}, pdfstartview=FitBH]{hyperref}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:text>\begin{document}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:apply-templates select="//z:notation"/>
<xsl:text>\end{document}</xsl:text>
<xsl:value-of select="$nl" />
</xsl:template>
<xsl:template match="z:notation">
<xsl:text>\section{</xsl:text><xsl:value-of select="@name"/><xsl:text>}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:apply-templates/>
</xsl:template>
<xsl:template match="text()">
<xsl:call-template name="escape-lbrace">
<xsl:with-param name="text" select="." />
</xsl:call-template>
</xsl:template>
<xsl:template name="escape-lbrace">
<xsl:param name="text" />
<xsl:choose>
<xsl:when test="contains($text,'{')">
<xsl:call-template name="escape-rbrace">
<xsl:with-param name="text" select="substring-before($text,'{')" />
</xsl:call-template>
<xsl:text>\{</xsl:text>
<xsl:call-template name="escape-lbrace">
<xsl:with-param name="text" select="substring-after($text,'{')" />
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="escape-rbrace">
<xsl:with-param name="text" select="$text" />
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<xsl:template name="escape-rbrace">
<xsl:param name="text" />
<xsl:choose>
<xsl:when test="contains($text,'}')">
<xsl:call-template name="escape-hash">
<xsl:with-param name="text" select="substring-before($text,'}')" />
</xsl:call-template>
<xsl:text>\}</xsl:text>
<xsl:call-template name="escape-rbrace">
<xsl:with-param name="text" select="substring-after($text,'}')" />
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
<xsl:call-template name="escape-hash">
<xsl:with-param name="text" select="$text" />
</xsl:call-template>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<xsl:template name="escape-hash">
<xsl:param name="text" />
<xsl:choose>
<xsl:when test="contains($text,'#')">
<xsl:value-of select="substring-before($text,'#')" />
<xsl:text>\#</xsl:text>
<xsl:call-template name="escape-hash">
<xsl:with-param name="text" select="substring-after($text,'#')" />
</xsl:call-template>
</xsl:when>
<xsl:otherwise>
<xsl:value-of select="$text"/>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<xsl:template match="html">
<xsl:apply-templates />
</xsl:template>
<xsl:template match="head">
<xsl:text>\title{</xsl:text>
<xsl:value-of select="$title" />
<xsl:text>}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:text>\author{</xsl:text>
<xsl:value-of select="$author" />
<xsl:text>}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:text>\date{</xsl:text>
<xsl:value-of select="$date" />
<xsl:text>}</xsl:text>
</xsl:template>
<xsl:template match="body">
<xsl:text>\begin{document}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:value-of select="$nl" />
<xsl:text>\maketitle</xsl:text>
<xsl:value-of select="$nl" />
<xsl:value-of select="$nl" />
<xsl:text>\section*{Abstract}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:apply-templates select="/html/head/div[@id='Abstract']" />
<xsl:value-of select="$nl" />
<xsl:text>\clearpage</xsl:text>
<xsl:apply-templates />
<xsl:text>\end{document}</xsl:text>
<xsl:value-of select="$nl" />
</xsl:template>
<xsl:template match="a">
<xsl:if test="@href">
<xsl:text>\href{</xsl:text>
<xsl:value-of select="@href" />
<xsl:text>}{</xsl:text>
<xsl:apply-templates />
<xsl:text>}</xsl:text>
</xsl:if>
</xsl:template>
<xsl:template match="h2">
<xsl:text>\section{</xsl:text>
<xsl:value-of select="." />
<xsl:text>}</xsl:text>
</xsl:template>
<xsl:template match="h3">
<xsl:text>\subsection{</xsl:text>
<xsl:value-of select="." />
<xsl:text>}</xsl:text>
</xsl:template>
<xsl:template match="h4">
<xsl:text>\subsubsection{</xsl:text>
<xsl:value-of select="." />
<xsl:text>}</xsl:text>
</xsl:template>
<xsl:template match="ul">
<xsl:text>\begin{itemize}</xsl:text>
<xsl:apply-templates />
<xsl:text>\end{itemize}</xsl:text>
</xsl:template>
<xsl:template match="ol">
<xsl:text>\begin{enumerate}</xsl:text>
<xsl:apply-templates />
<xsl:text>\end{enumerate}</xsl:text>
</xsl:template>
<xsl:template match="li">
<xsl:value-of select="'\item '" />
<xsl:apply-templates />
</xsl:template>
<xsl:template match="dl">
<xsl:text>\begin{description}</xsl:text>
<xsl:apply-templates />
<xsl:text>\end{description}</xsl:text>
</xsl:template>
<xsl:template match="dt">
<xsl:text>\item[</xsl:text>
<xsl:apply-templates />
<xsl:text>]</xsl:text>
</xsl:template>
<xsl:template match="dd">
<xsl:apply-templates />
</xsl:template>
<xsl:template match="table">
<xsl:text>\begin{table}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:text>\begin{tabular}{</xsl:text>
<!-- |l|l|l|l -->
<xsl:for-each select="col">
<xsl:text>|</xsl:text>
<xsl:choose>
<xsl:when test="@align='right'">
<xsl:text>r</xsl:text>
</xsl:when>
<xsl:when test="@align='center'">
<xsl:text>c</xsl:text>
</xsl:when>
<xsl:otherwise>
<xsl:text>l</xsl:text>
</xsl:otherwise>
</xsl:choose>
</xsl:for-each>
<xsl:text>|}</xsl:text>
<xsl:value-of select="$nl" />
<xsl:text>\hline</xsl:text>
<xsl:value-of select="$nl" />
<xsl:apply-templates select="thead | tfoot | tbody | tr" />
<xsl:text>\end{tabular}</xsl:text>
<xsl:apply-templates select="caption | z:label" />
<xsl:text>\end{table}</xsl:text>
</xsl:template>
<xsl:template match="caption">
<xsl:text>\caption{</xsl:text>
<xsl:apply-templates />
<xsl:text>}</xsl:text>
</xsl:template>
<xsl:template match="tr">
<xsl:apply-templates />
<xsl:value-of select="'\\ \hline '" />
</xsl:template>
<xsl:template match="th">
<xsl:choose>
<xsl:when test="following-sibling::th">
<xsl:value-of select="'\multicolumn{1}{|c}{\bf '" />
<xsl:apply-templates />
<xsl:value-of select="'}&'" />
</xsl:when>
<xsl:otherwise>
<xsl:value-of select="'\multicolumn{1}{|c|}{\bf '" />
<xsl:apply-templates />
<xsl:value-of select="'}'" />
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<xsl:template match="td">
<xsl:apply-templates />
<xsl:if test="local-name(following-sibling::*[1])='td'">
<xsl:text>&</xsl:text>
</xsl:if>
</xsl:template>
<!-- `` and '' -->
<xsl:template match="z:lquot">
<xsl:text>``</xsl:text>
</xsl:template>
<xsl:template match="z:rquot">
<xsl:text>''</xsl:text>
</xsl:template>
<!-- ` and ' -->
<xsl:template match="z:lapos">
<xsl:text>`</xsl:text>
</xsl:template>
<xsl:template match="z:rpos">
<xsl:text>'</xsl:text>
</xsl:template>
<!-- \ref{key} -->
<xsl:template match="z:ref">
<xsl:value-of select="concat('\ref{', @key, '}')" />
</xsl:template>
<!-- \label{key} -->
<xsl:template match="z:label">
<xsl:value-of select="concat('\label{', @key, '}')" />
</xsl:template>
<!-- Inline expressions
$Expression$
-->
<xsl:template match="z:math">
<xsl:text>$</xsl:text>
<xsl:apply-templates />
<xsl:text>$</xsl:text>
</xsl:template>
<xsl:template match="z:i">
<xsl:choose>
<xsl:when test="namespace-uri(..)='http://www.w3.org/2004/zml'">
<xsl:apply-templates />
</xsl:when>
<xsl:otherwise>
<xsl:text>$</xsl:text>
<xsl:apply-templates />
<xsl:text>$</xsl:text>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
<!-- Specifications -->
<!-- Schema box
\begin{schema}{Name}{Params}
Declarations
\where
Predicates
\end{schema}
-->
<xsl:template match="z:schema">
<xsl:text>\begin{schema}{</xsl:text>
<xsl:value-of select="@name" />
<xsl:text>}</xsl:text>
<xsl:if test="@params">
<xsl:text>[</xsl:text>
<xsl:value-of select="@params" />
<xsl:text>]</xsl:text>
</xsl:if>
<xsl:apply-templates />
<xsl:text>\end{schema}</xsl:text>
</xsl:template>
<!-- Axiomatic description
\begin{axdef}
Declarations
\where
Predicates
\end{axdef}
-->
<xsl:template match="z:axdef">
<xsl:text>\begin{axdef}</xsl:text>
<xsl:apply-templates />
<xsl:text>\end{axdef}</xsl:text>
</xsl:template>
<!-- Generic definition
\begin{gendef}{Params}
Declarations
\where
Predicates
\end{schema}
-->
<xsl:template match="z:gendef">
<xsl:text>\begin{gendef}[</xsl:text>
<xsl:value-of select="@params" />
<xsl:text>]</xsl:text>
<xsl:apply-templates />
<xsl:text>\end{gendef}</xsl:text>
</xsl:template>
<!-- \where, \also -->
<xsl:template match="z:also | z:where">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!-- \\ -->
<xsl:template match="z:nl">
<xsl:text>\\</xsl:text>
</xsl:template>
<!-- \t1, \t2, ... -->
<xsl:template match="z:t1 | z:t2 | z:t3 | z:t4 | z:t5 | z:t6 | z:t7 | z:t8 | z:t9">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!--
\begin{zed}
...
\end{zed}
-->
<xsl:template match="z:zed">
<xsl:text>\begin{zed}</xsl:text>
<xsl:apply-templates />
<xsl:text>\end{zed}</xsl:text>
</xsl:template>
<!-- Schema definition \defs -->
<xsl:template match="z:defs">
<xsl:value-of select="concat('\defs',' ')" />
</xsl:template>
<!-- Free type definition \ldata, \rdata -->
<xsl:template match="z:ldata | z:rdata">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!-- Logic and schema calculus -->
<xsl:template match="z:lnot | z:land | z:lor | z:implies | z:iff | z:forall | z:exists | z:exists_1">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!-- Special schema operators -->
<xsl:template match="z:hide | z:project | z:pre | z:semi | z:pipe">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!-- Basic expressions -->
<xsl:template match="z:neq | z:IF | z:THEN | z:ELSE | z:theta | z:mu | z:LET">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!-- Sets -->
<xsl:template match="z:in | z:notin | z:emptyset | z:subseteq | z:subset">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:power | z:power_1">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:cross | z:cup | z:cap | z:setminus | z:bigcup | z:bigcap | z:finset | z:finset_1">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:first | z:second">
<xsl:value-of select="concat(' ', local-name(),' ')" />
</xsl:template>
<!-- Relations -->
<xsl:template match="z:rel | z:mapsto | z:dom | z:ran | z:id | z:comp | z:circ | z:dres | z:rres | z:ndres | z:nrres">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:inv | z:limg | z:rimg | z:oplus | z:plus | z:star">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:sup">
<xsl:text>^{</xsl:text>
<xsl:apply-templates />
<xsl:text>}</xsl:text>
</xsl:template>
<xsl:template match="z:iter">
<xsl:value-of select="concat(' ', local-name(),' ')" />
</xsl:template>
<!-- Functions -->
<xsl:template match="z:lambda | z:pfun | z:fun | z: pinj | z:inj | z:psurj | z:surj | z:bij | z:ffun | z:finj">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!-- Numbers and arithmetic -->
<xsl:template match="z:nat | z:num | z:div | z:mod | z:leq | z:geq | z:nat_1 | z:upto">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:succ | z:min | z:max">
<xsl:value-of select="concat(' ', local-name(),' ')" />
</xsl:template>
<!-- Sequences -->
<xsl:template match="z:seq | z:seq_1 | z:iseq | z:langle | z:rangle | z:cat | z:extract | z:filter">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:rev | z:head | z:last | z:tail | z:front | z:squash">
<xsl:value-of select="concat(' ', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:prefix | z:suffix | z:inseq | z:dcat | z:disjoint | z:partition">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<!-- Bags -->
<xsl:template match="z:bag | z:lbag | z:rbag | z:bcount | z:otimes | z:inbag | z:subbageq | z:uplus | z:uminus">
<xsl:value-of select="concat('\', local-name(),' ')" />
</xsl:template>
<xsl:template match="z:count | z:items">
<xsl:value-of select="concat(' ', local-name(),' ')" />
</xsl:template>
</xsl:stylesheet>
--- NEW FILE: wsdl20.tex ---
\documentclass{article}
\usepackage{fuzz}
\usepackage[pdftitle={Untitled}, pdfauthor={Anonymous}, pdfstartview=FitBH]{hyperref}
\begin{document}
\section{ZNotation}
This specification uses Z Notation (see )
to formalize the WSDL component model.
The Z Notation in this specification has been verified using the
Fuzz 2000 type-checker (see ).
\section{Component}
Let $Component$ be the set of all components:
\begin{zed}
Component ::= \\
\t1 description\ldata Description\rdata | \\
\t1 elementDecl\ldata ElementDeclaration\rdata | \\
\t1 typeDef\ldata TypeDefinition\rdata | \\
\t1 interface\ldata Interface\rdata | \\
\t1 interfaceFault\ldata InterfaceFault\rdata | \\
\t1 interfaceOp\ldata InterfaceOperation\rdata | \\
\t1 messageRef\ldata MessageReference\rdata | \\
\t1 faultRef\ldata FaultReference\rdata | \\
\t1 feature\ldata Feature\rdata | \\
\t1 property\ldata Property\rdata | \\
\t1 binding\ldata Binding\rdata | \\
\t1 bindingFault\ldata BindingFault\rdata | \\
\t1 bindingOp\ldata BindingOperation\rdata | \\
\t1 bindingMessageRef\ldata BindingMessageReference\rdata | \\
\t1 service\ldata Service\rdata | \\
\t1 endpoint\ldata Endpoint\rdata
\end{zed}
\section{ID}
When a component property is described as containing another component or a set of other components,
the intended meaning is that the component property contains a reference to another component
or a set of references to other components.
Every component contains
an implicit property that uniquely identifies itself and that can be used
to express references.
Let $ID$ be the set of all component identifier values:
\begin{zed}
[ID]
\end{zed}
\section{ComponentId}
A component is an identified, typed collection of properties.
Let Identifier denote the set of component identifiers:
Let id be the identifier of the component.
\begin{schema}{Identifier}
id : ID
\end{schema}
\begin{axdef}
Id : Component \fun ID
\where
\forall x : Description @ Id(description(x)) = x.id \\
\forall x : ElementDeclaration @ Id(elementDecl(x)) = x.id \\
\forall x : TypeDefinition @ Id(typeDef(x)) = x.id \\
\forall x : Interface @ Id(interface(x)) = x.id \\
\forall x : InterfaceFault @ Id(interfaceFault(x)) = x.id \\
\forall x : InterfaceOperation @ Id(interfaceOp(x)) = x.id \\
\forall x : MessageReference @ Id(messageRef(x)) = x.id \\
\forall x : FaultReference @ Id(faultRef(x)) = x.id \\
\forall x : Feature @ Id(feature(x)) = x.id \\
\forall x : Property @ Id(property(x)) = x.id \\
\forall x : Binding @ Id(binding(x)) = x.id \\
\forall x : BindingFault @ Id(bindingFault(x)) = x.id \\
\forall x : BindingOperation @ Id(bindingOp(x)) = x.id \\
\forall x : BindingMessageReference @ Id(bindingMessageRef(x)) = x.id \\
\forall x : Service @ Id(service(x)) = x.id \\
\forall x : Endpoint @ Id(endpoint(x)) = x.id
\end{axdef}
\section{ComponentModel}
A component model is a set of uniquely identified components.
Let $ComponentModel$ be the set of component models:
Let $components$ be the finite set of components in the component model.
\begin{schema}{ComponentModel}
components : \finset Component
\where
\forall x, y : components @ \\
\t1 Id(x) = Id(y) \implies x = y
\end{schema}
No two components have the same identifier.
\section{Components}
\begin{schema}{Components}
ComponentModel \\
descriptionComps : \finset Description \\
elementDeclComps : \finset ElementDeclaration \\
typeDefComps : \finset TypeDefinition \\
interfaceComps : \finset Interface \\
interfaceFaultComps : \finset InterfaceFault \\
interfaceOpComps : \finset InterfaceOperation \\
messageRefComps : \finset MessageReference \\
faultRefComps : \finset FaultReference \\
featureComps : \finset Feature \\
propertyComps : \finset Property \\
bindingComps : \finset Binding \\
bindingFaultComps : \finset BindingFault \\
bindingOpComps : \finset BindingOperation \\
bindingMessageRefComps : \finset BindingMessageReference \\
serviceComps : \finset Service \\
endpointComps : \finset Endpoint
\where
descriptionComps = \{~x : Description | \\
\t1 description(x) \in components~\}
\also
elementDeclComps = \{~x : ElementDeclaration | \\
\t1 elementDecl(x) \in components~\}
\also
typeDefComps = \{~x : TypeDefinition | \\
\t1 typeDef(x) \in components~\}
\also
interfaceComps = \{~x : Interface | \\
\t1 interface(x) \in components~\}
\also
interfaceFaultComps = \{~x : InterfaceFault | \\
\t1 interfaceFault(x) \in components~\}
\also
interfaceOpComps = \{~x : InterfaceOperation | \\
\t1 interfaceOp(x) \in components~\}
\also
messageRefComps = \{~x : MessageReference | \\
\t1 messageRef(x) \in components~\}
\also
faultRefComps = \{~x : FaultReference | \\
\t1 faultRef(x) \in components~\}
\also
featureComps = \{~x : Feature | \\
\t1 feature(x) \in components~\}
\also
propertyComps = \{~x : Property | \\
\t1 property(x) \in components~\}
\also
bindingComps = \{~x : Binding | \\
\t1 binding(x) \in components~\}
\also
bindingFaultComps = \{~x : BindingFault | \\
\t1 bindingFault(x) \in components~\}
\also
bindingOpComps = \{~x : BindingOperation | \\
\t1 bindingOp(x) \in components~\}
\also
bindingMessageRefComps = \{~x : BindingMessageReference | \\
\t1 bindingMessageRef(x) \in components~\}
\also
serviceComps = \{~x : Service | \\
\t1 service(x) \in components~\}
\also
endpointComps = \{~x : Endpoint | \\
\t1 endpoint(x) \in components~\}
\end{schema}
The component model has additional constraints which are described in the following sections.
These additonal constraints often refer to the sets of ids that are associated which each type of component.
It is therefore convenient to define these sets.
Let $ComponentIds$ be the component model augmented with the sets of ids associated
with each type of component:
\begin{schema}{ComponentIds}
Components \\
descriptions, elementDecls, \\
typeDefs, interfaces, \\
interfaceFaults, interfaceOps, \\
messageRefs, faultRefs, \\
features, properties, \\
bindings, bindingFaults, \\
bindingOps, bindingMessageRefs, \\
services, endpoints : \finset ID
\where
descriptions = \{~x : descriptionComps @ x.id~\} \\
elementDecls = \{~x : elementDeclComps @ x.id~\} \\
typeDefs = \{~x : typeDefComps @ x.id~\} \\
interfaces = \{~x : interfaceComps @ x.id~\} \\
interfaceFaults = \{~x : interfaceFaultComps @ x.id~\} \\
interfaceOps = \{~x : interfaceOpComps @ x.id~\} \\
messageRefs = \{~x : messageRefComps @ x.id~\} \\
faultRefs = \{~x : faultRefComps @ x.id~\} \\
features = \{~x : featureComps @ x.id~\} \\
properties = \{~x : propertyComps @ x.id~\} \\
bindings = \{~x : bindingComps @ x.id~\} \\
bindingFaults = \{~x : bindingFaultComps @ x.id~\} \\
bindingOps = \{~x : bindingOpComps @ x.id~\} \\
bindingMessageRefs = \{~x : bindingMessageRefComps @ x.id~\} \\
services = \{~x : serviceComps @ x.id~\} \\
endpoints = \{~x : endpointComps @ x.id~\}
\end{schema}
\section{OPTIONAL}
An OPTIONAL simple property type is treated
as a set-valued type that contains at most one member.
If the property is absent then its value is the empty set.
If the property is present then its value is the singleton set
that contains the actual value of the property.
Let $OPTIONAL$[$X$] be the OPTIONAL values
of type X where X is a simple property type:
\begin{gendef}[X]
OPTIONAL : \power (\finset X)
\where
OPTIONAL = \{\emptyset \} \cup \{~x : X @ \{x\}~\}
\end{gendef}
An optional value of type $X$ is either the empty set or a singleton set
that contains one member of $X$.
\section{ElementContentModel}
Let $ElementContentModel$ be the set of all models that define the allowable
values for the [children] and [attribute] properties of an element information item:
\begin{zed}
[ElementContentModel]
\end{zed}
\section{ElementDeclaration}
Let $ElementDeclaration$ be the collection of properties of the Element Declaration component:
Let $name$ be the QName defined by the [local name] and [namespace name]
properties of the element information item.
Let $elementContentModel$ be the element content model that constrains the
allowable contents of the [children] and [attribute] properties of the element information item.
\begin{schema}{ElementDeclaration}
Identifier \\
name : QName \\
elementContentModel : ElementContentModel
\end{schema}
\section{TypeDefinition}
Let $TypeDefinition$ be the collection of properties of the Type Definition component:
Let $name$ be the QName of the type definition.
Let $elementContentModel$ be the element content model that constrains the
allowable contents of the [children] and [attribute] properties of the element information item
described by the type definition.
\begin{schema}{TypeDefinition}
Identifier \\
name : QName \\
elementContentModel : ElementContentModel
\end{schema}
\section{Description}
Let $Description$ be the collection of properties of the Description component:
\begin{schema}{Description}
Identifier \\
interfaces : \finset ID \\
bindings : \finset ID \\
services : \finset ID \\
elementDeclarations : \finset ID \\
typeDefinitions : \finset ID
\end{schema}
\section{DescriptionIds}
The component model contains a unique Description component.
Each component refered to by the properties of the Description component
must exist in the component model.
Let $DescriptionIds$ express these referential integrity constraints
on the Description component:
Let $descriptionComp$ be the Description component.
Let $descriptionProps$ be the properties of the Description component.
\begin{schema}{DescriptionIds}
ComponentIds \\
descriptionComp : Description
\where
descriptionComps = \{descriptionComp\}
\also
descriptionComp.interfaces = interfaces \\
descriptionComp.bindings = bindings \\
descriptionComp.services = services \\
descriptionComp.elementDeclarations = elementDecls \\
descriptionComp.typeDefinitions = typeDefs
\end{schema}
The component model contains a unique Description component.
The Description component contains exactly the set of Interface components contained in the component model.
The Description component contains exactly the set of Binding components contained in the component model.
The Description component contains exactly the set of Service components contained in the component model.
The Description component contains exactly the set of Element Declaration components contained in the component model.
The Description component contains exactly the set of Type Definition components contained in the component model.
\section{DescriptionQNames}
Let $DescriptionQNames$ express the
QName uniqueness constraint on the Description component:
\begin{schema}{DescriptionQNames}
Components
\where
\forall x, y : interfaceComps @ \\
\t1 x.name = y.name \implies x = y
\also
\forall x, y : bindingComps @ \\
\t1 x.name = y.name \implies x = y
\also
\forall x, y : serviceComps @ \\
\t1 x.name = y.name \implies x = y
\also
\forall x, y : elementDeclComps @ \\
\t1 x.name = y.name \implies x = y
\also
\forall x, y : typeDefComps @ \\
\t1 x.name = y.name \implies x = y
\end{schema}
No two Interface components have the same QName.
No two Binding components have the same QName.
No two Service components have the same QName.
No two Element Declaration components have the same QName.
No two Type Definition components have the same QName.
\section{Interface}
Let $Interface$ be the Interface component:
\begin{schema}{Interface}
Identifier \\
name : QName \\
extendedInterfaces : \finset ID \\
faults : \finset ID \\
operations : \finset ID \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{InterfaceIds}
Each component referenced by an Interface component must exist in the component model.
Let $InterfaceIds$ express the referential integrity constraints on the Interface component:
\begin{schema}{InterfaceIds}
ComponentIds
\where
\forall x : interfaceComps @ \\
\t1 x.id \notin x.extendedInterfaces \land \\
\t1 x.extendedInterfaces \subset interfaces \land \\
\t1 x.faults \subseteq interfaceFaults \land \\
\t1 x.operations \subseteq interfaceOps \land \\
\t1 x.features \subseteq features \land \\
\t1 x.properties \subseteq properties
\end{schema}
No Interface component extends itself.
The Interface components extended by each Interface component are contained in the component model.
The Fault components of each Interface component are contained in the component model.
The Operation components of each Interface component are contained in the component model.
The Feature components of each Interface component are contained in the component model.
The Property components of each Interface component are contained in the component model.
\section{InterfaceClosure}
The properties of an Interface component contain the properties of each
Interface component that it extends.
Let $InterfaceClosure$ express the Interface closure constraints:
\begin{schema}{InterfaceClosure}
InterfaceIds
\where
\forall x, y : interfaceComps | \\
\t1 y.id \in x.extendedInterfaces @ \\
\t2 y.extendedInterfaces \subset x.extendedInterfaces \land \\
\t2 y.faults \subseteq x.faults \land \\
\t2 y.operations \subseteq x.operations \land \\
\t2 y.features \subseteq x.features \land \\
\t2 y.properties \subseteq x.properties
\end{schema}
\section{InterfaceFault}
Let $InterfaceFault$ be the
Interface Fault component:
\begin{schema}{InterfaceFault}
Identifier \\
name : QName \\
element : OPTIONAL[ID] \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{InterfaceOperation}
Let $InterfaceOperation$ be the
Interface Operation component:
\begin{schema}{InterfaceOperation}
Identifier \\
name : QName \\
messageExchangePattern : AbsoluteURI \\
messageReferences : \finset ID \\
faultReferences : \finset ID \\
style : \finset AbsoluteURI \\
safety : Boolean \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{Direction}
Let $Direction$ be a message direction of either in or out:
\begin{zed}
Direction ::= inToken | outToken
\end{zed}
\section{MessageContentModel}
Let $MessageContentModel$ be a message content model of either any, none, or element:
\begin{zed}
MessageContentModel ::= anyToken | noneToken | elementToken
\end{zed}
\section{MessageReference}
Let $MessageReference$ be the Message Reference component:
\begin{schema}{MessageReference}
Identifier \\
messageLabel : NCName \\
direction : Direction \\
messageContentModel : OPTIONAL[MessageContentModel] \\
element : OPTIONAL[ID] \\
features : \finset ID \\
properties : \finset ID
\where
messageContentModel = \{elementToken\} \iff element \neq \emptyset
\end{schema}
\section{FaultReference}
Let $FaultReference$ be the Fault Reference component:
\begin{schema}{FaultReference}
Identifier \\
faultReference : ID \\
messageLabel : NCName \\
direction : Direction \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{Feature}
Let $Feature$ be the Feature component:
\begin{schema}{Feature}
Identifier \\
name : AbsoluteURI \\
required : Boolean
\end{schema}
\section{ValueConstraint}
Let $ValueConstraint$ be the set of value constraints for Property components:
\begin{zed}
ValueConstraint ::= typeDefinitionId\ldata ID\rdata | valueToken
\end{zed}
A value constraint is either a Type Definition component which defines
the set of allowable values, or the token value which
indicates that the value is given by the contents of the value property
of the Property component.
\section{ElementChildren}
Let $ElementChildren$ be the set of all allowable values of the [children]
property of an XML Infoset element information item:
\begin{zed}
[ElementChildren]
\end{zed}
\section{Property}
Let $Property$ be the Property component:
\begin{schema}{Property}
Identifier \\
name : AbsoluteURI \\
required : Boolean \\
valueConstraint : OPTIONAL[ValueConstraint] \\
value : OPTIONAL[ElementChildren]
\where
valueConstraint = \{valueToken\} \iff value \neq \emptyset
\end{schema}
The value is constrained to be an explicitly given value exactly when
the value property is defined.
\section{Binding}
Let $Binding$ be the Binding component:
\begin{schema}{Binding}
Identifier \\
name : QName \\
interface : OPTIONAL[ID] \\
type : AbsoluteURI \\
faults : \finset ID \\
operations : \finset ID \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{BindingFault}
Let $BindingFault$ be the BindingFault component:
\begin{schema}{BindingFault}
Identifier \\
faultReference : ID \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{BindingOperation}
Let $BindingOperation$ be the BindingOperation component:
\begin{schema}{BindingOperation}
Identifier \\
operationReference : ID \\
messageReferences : \finset ID \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{BindingMessageReference}
Let $BindingMessageReference$ be the BindingMessageReference component:
\begin{schema}{BindingMessageReference}
Identifier \\
messageLabel : OPTIONAL[NCName] \\
direction : Direction \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{Service}
Let $Service$ be the Service component:
\begin{schema}{Service}
Identifier \\
name : QName \\
interface : ID \\
endpoints : \finset_1 ID \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{Endpoint}
Let $Endpoint$ be the Endpoint component:
\begin{schema}{Endpoint}
Identifier \\
name : NCName \\
binding : ID \\
address : AbsoluteURI \\
features : \finset ID \\
properties : \finset ID
\end{schema}
\section{NCName}
Let $NCName$ be wsdls:NCName:
\begin{zed}
[NCName]
\end{zed}
\section{URI}
Let $URI$ be wsdls:anyURI:
\begin{zed}
[URI]
\end{zed}
\section{AbsoluteURI}
Let $AbsoluteURI$ be the subset of absolute URIs:
\begin{axdef}
AbsoluteURI : \power URI
\end{axdef}
\section{QName}
Let $QName$ be wsdls:QName:
\begin{schema}{QName}
namespaceName : AbsoluteURI \\
localName : NCName
\end{schema}
\section{Boolean}
Let $Boolean$ be wsdls:boolean:
\begin{zed}
Boolean ::= True | False
\end{zed}
\end{document}
Received on Friday, 12 November 2004 01:30:51 UTC