W3C home > Mailing lists > Public > public-ws-desc-eds@w3.org > November 2004

2002/ws/desc/wsdl20 zml2latex.xsl,NONE,1.1 wsdl20.tex,NONE,1.1 .cvsignore,1.4,1.5

From: Arthur Ryman <aryman@dev.w3.org>
Date: Fri, 12 Nov 2004 01:30:50 +0000
To: public-ws-desc-eds@w3.org
Message-ID: <E1CSQH4-0006MA-Jd@lionel-hutz.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>&#x0A;</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="'}&amp;'" />
			</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>&amp;</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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.22 : Friday, 12 November 2004 01:30:51 GMT