From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Mon, 2 Sep 2019 13:46:59 +0900 Subject: Initial commit --- macros/latex/contrib/zed-csp/csp2e.pdf | Bin 0 -> 112501 bytes macros/latex/contrib/zed-csp/csp2e.tex | 381 +++++++++++++++ macros/latex/contrib/zed-csp/zed-csp.sty | 789 +++++++++++++++++++++++++++++++ macros/latex/contrib/zed-csp/zed2e.pdf | Bin 0 -> 147037 bytes macros/latex/contrib/zed-csp/zed2e.tex | 774 ++++++++++++++++++++++++++++++ 5 files changed, 1944 insertions(+) create mode 100644 macros/latex/contrib/zed-csp/csp2e.pdf create mode 100644 macros/latex/contrib/zed-csp/csp2e.tex create mode 100644 macros/latex/contrib/zed-csp/zed-csp.sty create mode 100644 macros/latex/contrib/zed-csp/zed2e.pdf create mode 100644 macros/latex/contrib/zed-csp/zed2e.tex (limited to 'macros/latex/contrib/zed-csp') diff --git a/macros/latex/contrib/zed-csp/csp2e.pdf b/macros/latex/contrib/zed-csp/csp2e.pdf new file mode 100644 index 0000000000..557e7d7045 Binary files /dev/null and b/macros/latex/contrib/zed-csp/csp2e.pdf differ diff --git a/macros/latex/contrib/zed-csp/csp2e.tex b/macros/latex/contrib/zed-csp/csp2e.tex new file mode 100644 index 0000000000..880eedf08f --- /dev/null +++ b/macros/latex/contrib/zed-csp/csp2e.tex @@ -0,0 +1,381 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% csp2e.tex -> hack guide to zed-csp.sty + +% (c) Jim Davies September 1994 >> Version 0 << + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\documentclass[12pt]{article} + +% \usepackage[yy]{lucbr} + +% Uncomment the above line if you have the Lucida fonts and want to +% use them to set csp. Note that you may have to change the [yy] +% option if you are not using the Y&Y font naming convention. + +\usepackage{zed-csp} + +\advance\textwidth 30mm +\advance\oddsidemargin -15mm +\advance\evensidemargin -15mm +\advance\textheight 35mm +\advance\topmargin -20mm + +\begin{document} \thispagestyle{empty} + +\def\AMS{% + $\cal{A}$ + \kern-.5em\lower.5ex\hbox{$\cal{M}$}\kern-.125em$\cal{S}$} + +\parindent 0pt +\parskip 10pt + +{\huge\bf Setting real-time CSP} + +\vskip 2mm + +{\Large Jim Davies} + +\vskip 8mm + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section{Introduction} + +The language and models of CSP have undergone a gradual evolution +since the publication of the first CSP textbook---Hoare's {\sl +Communicating Sequential Processes\/} (Prentice-Hall, 1985). The +forthcoming text on real-time CSP will provide for some +degree of standardisation. + +In parallel, we hope to provide a standard set of macros for setting +documents which use CSP notation. This will allow users to exchange +documents in electronic form, and will form part of the user interface +to the language tools. + +The macros are defined by a style file called \verb|zed-csp.sty|. +This should work with \LaTeXe. Inquiries, suggestions, or complaints +should be addressed to + +\begin{center} + {\tt Jim.Davies@comlab.ox.ac.uk}. +\end{center} + +Note that this is a fairly quick fix of the style to enable myself and +others to use the improved facilities offered by the new version of +\LaTeX. It has not been rigorously tested, although it seems to work +for me. + +\section{Symbols} + +We can divide the symbols used into three separate classes: symbols +for the language itself, symbols used in the definition of the +semantics, and symbols used in the specification language. + +\subsection{The language of real-time CSP} + +The operators of real-time CSP are set using macros of the same name. +The macros for atomic operators begin with an uppercase letter; the +same is true for those representing indexed versions of parallel and +choice operators. All other macros are lowercase throughout. Some +operators accept optional arguments, but no argument is compulsory. + +When an operator with an optional argument appears within an optional +argument, \LaTeX may require assistance if it is to parse the +expression correctly. In these circumstances, we use an extra pair of +braces to delimit the process expression: e.g., +\begin{center} + \verb|\Ftf[{P \parallel[A] Q}]|. +\end{center} + +\begin{tabular}{p{2in}p{1.5in}c} \\ \\ +bottom & \verb|\Bottom| & $ \Bottom $ \\[1ex] +stop & \verb|\Stop| & $ \Stop $ \\[1ex] +skip & \verb|\Skip| & $ \Skip $ \\[1ex] +wait & \verb|\Wait| & $ \Wait $ \\[1ex] +prefix & \verb|\then| & $ \then $ \\[1ex] +external choice & \verb|\extchoice| & $ \extchoice $ \\[1ex] +internal choice & \verb|\intchoice| & $ \intchoice $ \\[1ex] +hiding & \verb|\hide| & $ \hide $ \\[1ex] +parallel & \verb|\parallel[A][B]|& $ \parallel[A][B] $\\[1ex] +interleaving & \verb|\interleave| & $ \interleave $ \\[1ex] +sharing & \verb|\parallel[C]| & $ \parallel[C] $ \\[1ex] +recursion & \verb|\mu X \spot P| & $ \mu X \spot P $ \\[1ex] +timeout & \verb|\timeout[t]| & $\timeout[t]$\\[1ex] +transfer & \verb|\transfer[t]| & $\transfer[t]$\\[1ex] +interrupt & \verb|\interrupt| & $\interrupt$ \\[1ex] +timer & \verb|\at| & $\at$ \\[1ex] +indexed external choice & \verb|\Extchoice| & $ \Extchoice $ \\[1ex] +indexed internal choice & \verb|\Intchoice| & $ \Intchoice $ \\[1ex] +indexed alphabet parallel & \verb|\Parallel| & $ \Parallel $ \\[1ex] +indexed interleaving & \verb|\Interleave| & $ \Interleave $ +\end{tabular} + +\subsection{Parallel combinations} + +There are several ways to denote the parallel combination of +two processes in CSP. Firstly, we can describe the set of events upon +which they must cooperate: e.g., in the process +\[ +P \parallel[C] Q +\] +components $P$ and $Q$ must cooperate upon every event from the shared +set $C$. Alternatively, we can declare two alphabets +\begin{eqnarray*} +\alpha P & = & A \\ +\alpha Q & = & B +\end{eqnarray*} +and write +\[ +P \parallel Q +\] +to denote the parallel combination in which $P$ and $Q$ must cooperate +upon every event in the intersection of their alphabets. Finally, we +can add explicit alphabet information to the parallel operator: e.g., +\[ +P \parallel[A][B] Q +\] +is equivalent to the above parallel combination, given the values +chosen for $\alpha P$ and $\alpha Q$. + +\subsection{Delays and timers} + +We write $\Wait t ; P$ to denote the process which will delay for time +$t$ before behaving as $P$. The wait process is a delayed form of +termination $\Skip$: i.e., +\begin{eqnarray*} +\Wait 0 & = & \Skip +\end{eqnarray*} +To model a nondeterministic delay, we can use an internal choice +operator indexed by a range of time values: +\[ +\Intchoice_{t \in [t_1,t_2)} \Wait t +\] +A convenient abbreviation for this involves overloading the $\Wait$ +operator: e.g., +\[ +\Wait [t_1,t_2) +\] +abbreviates the above choice. + +External events in a process description are performed in cooperation +with the environment of that process. It is therefore quite likely +that an external event will not occur as soon as the process is ready. +The time elapsed between the offer of an event and its occurrence can +influence future behaviour; the rest of the process description should +be allowed to refer to this time. + +Accordingly, real-time CSP includes a timer construct, or +`passage-of-time' operator. We write +\[ +a \at t \then P \qquad \qquad \hbox{\verb|a \at t \then P|} +\] +to denote a process which is initially ready to engage in event $a$. +The time variable $t$ is assigned the relative time at which $a$ +occurs. This is the same as the elapsed time between control being +passed to this process---at which point the offer of $a$ is made---and +the event $a$ actually occuring. + +A useful extension to this, which adds nothing to the expressivity of +the language but can make for more intelligible process descriptions, +is the offer timeout. We write +\[ +a \at t \{ d \} \then P \qquad \qquad +\hbox{\verb|a \at t \{ d \} \then P|} +\] +to denote a process which offers to perform $a$, and will store the +time of occurrence in $t$, but will withdraw the offer if it has not +been accepted by time $d$. (This form of timeout was suggested +by Guy Leduc for his version of timed LOTOS.) + +\section{Mathematical language} + +The semantic models of CSP come with a great deal of notational +baggage. We need to define operators to project information out of +traces, refusals, and timed failures. There is also a specification +language based upon the timed semantics, and the names used for the +models themselves. + +\subsection{Logic, sets, and sequences} + +\begin{tabular}{c@{\hspace{0.55in}}c@{\hspace{0.55in}}c} \\ +\begin{tabular}[t]{@{}lc} +\verb|\defs| & $ \defs $ \\[0.6ex] +\verb|\mu| & $ \mu $ \\[0.6ex] +\verb|\lambda| & $ \lambda $ \\[0.6ex] +\verb|\exists| & $ \exists $ \\[0.6ex] +\verb|\forall| & $ \forall $ \\[0.6ex] +\verb|\spot| & $ \spot $ \\[0.6ex] +\verb|\nat| & $ \nat $ \\[0.6ex] +\verb|\num| & $ \num $ \\[0.6ex] +\verb|\rat| & $ \rat $ \\[0.6ex] +\verb|\real| & $ \real $ \\[0.6ex] +\verb|\seq| & $ \seq $ +\end{tabular} & +\begin{tabular}[t]{lc} +\verb|\land| & $ \land $ \\[0.6ex] +\verb|\lor| & $ \lor $ \\[0.6ex] +\verb|\Land| & $ \Land $ \\[0.6ex] +\verb|\Lor| & $ \Lor $ \\[0.6ex] +\verb|\lnot| & $\lnot $ \\[0.6ex] +\verb|\implies| & $ \implies $ \\[0.6ex] +\verb|\iff| & $ \iff $ \\[0.6ex] +\verb|\upto| & $\upto$ \\[0.6ex] +\verb|\le| & $ \le $ \\[0.6ex] +\verb|\ge| & $ \ge $ \\[0.6ex] +\verb|\project| & $ \project $ +\end{tabular} & +\begin{tabular}[t]{lc} +\verb|\power| & $ \power $ \\[0.6ex] +\verb|\finset| & $ \finset $ \\[0.6ex] +\verb|\cross| & $ \cross $ \\[0.6ex] +\verb|\union| & $ \union $ \\[0.6ex] +\verb|\inter| & $ \inter $ \\[0.6ex] +\verb|\Union| & $ \Union $ \\[0.6ex] +\verb|\Inter| & $ \Inter $ \\[0.6ex] +\verb|\dom| & $ \dom$ \\[0.6ex] +\verb|\ran| & $ \ran$ \\[0.6ex] +\verb|\emptyset| & $\emptyset$ \\[0.6ex] +\verb|\set{x}| & $ \set{x} $ +\end{tabular} +\end{tabular} + +\subsection{Operators on traces} + +\begin{tabular}{p{1.95in}p{1.75in}c} \\ +empty trace & \verb|\nil| & $\nil $ \\[0.6ex] +trace & \verb|\trace{e_1,e_2}| & $\trace{e_1,e_2}$\\[0.6ex] +catenation of traces & \verb|\cat| & $\cat $ \\[0.6ex] +count & \verb|\cnt| & $\cnt $ \\[0.6ex] +during & \verb|\during| & $\during $ \\[0.6ex] +tick event & \verb|\tick| & $\tick$ \\[0.6ex] +subsequence & \verb|\subseq| & $\subseq$ \\[0.6ex] +data values & \verb|\data| & $\data$ +\end{tabular} + +\subsection{Projection functions} + +\begin{tabular}{p{1.95in}p{1.75in}l} \\ + begin & \verb|\Begin | & $\Begin$ \\[0.4ex] + end & \verb|\End | & $\End $ \\[0.4ex] + head & \verb|\Head | & $\Head $ \\[0.4ex] + first & \verb|\First | & $\First$ \\[0.4ex] + tail & \verb|\Tail | & $\Tail $ \\[0.4ex] + front & \verb|\Front | & $\Front$ \\[0.4ex] + last & \verb|\Last | & $\Last $ \\[0.4ex] + times & \verb|\Times | & $\Times$ \\[0.4ex] + events & \verb|\Events | & $\Events$ \\[0.4ex] +\end{tabular} + +$\Times$ and $\Events$ are projection functions from timed traces to +sequences of times and sequences of events respectively. $\Head$ and +$\Tail$ may be applied to any sequence. $\Begin$ and $\End$ may be +applied to timed traces and timed refusals. $\First$ is a synonym for +$\Head$. $\Front$ is the dual of $\Tail$. $\Last$ is the dual of +$\Head$. + +To denote the set of events mentioned in a timed or untimed trace or +refusal, we prefix the name of the object with $\alpha$. For example, +the set of events mentioned in the timed trace $s$ would be written +$\alpha s$. Earlier version of real-time CSP did this using the +$\sigma$ operator to avoid confusion with process alphabets. Where +there is scope for confusion, we suggest that this practice is +continued. + +\subsection{Semantic functions, models, and spaces} + +In {\sl Advanced CSP}, we use long names for the semantic functions: + +\begin{tabular}{p{1.95in}p{1.75in}l} \\ +semantics & \verb|\Semantics| & $\Semantics$ \\ +traces & \verb|\Traces| & $\Traces$ \\ +failures & \verb|\Failures| & $\Failures$ \\ +timed failures & \verb|\TimedFailures| & $\TimedFailures$ \\ +divergences & \verb|\Divergences| & $\Divergences$ \\ +infinites & \verb|\Infinites| & $\Infinites$ +\end{tabular} + +Any semantic function macro can be given an optional argument. This +will be set within semantic brackets: e.g., \verb|\Traces[P]| yields +$\Traces[P]$. To obtain the semantic brackets alone, use the +\verb|\semb| macro; this takes a single compulsory argument. +Alternatively, the macros \verb|\leftsemb| and \verb|\rightsemb| +produce left and right semantic brackets respectively. + +In theoretical papers, we often need to refer to several models, +functions, and associated spaces. To make things easier on ourselves, +we adopt short names for these mathematical objects, using subscripts +to identify the model concerned. For example, the objects associated +with the timed failures model are all subscripted with $TF$. + +The models themselves have macros beginning \verb|\M|: + +\begin{tabular}{p{2.4in}p{1.1in}l} \\ +traces & \verb|\Mut| & $ \Mut $ \\ +failures & \verb|\Muf| & $ \Muf $ \\ +failures-divergences & \verb|\Mufd| & $ \Mufd $ \\ +timed failures & \verb|\Mtf| & $ \Mtf $ \\ +timed failures-stability & \verb|\Mtfs| & $ \Mtfs $ \\ +timed infinite & \verb|\Mti| & $ \Mti $ +\end{tabular} + +The matching semantic functions use \verb|\F| instead---e.g., +\verb|\Fut| for untimed traces---and the observation spaces use +\verb|\S|. + +\subsection{Refinement and satisfaction} + +The satisfaction notation employed in Hoare's {\sl Communicating +Sequential Processes} has been retained. We also have a refinement +relation between processes, possibly indexed by the name of the model +concerned. + +The satisfaction relation is set as follows: \verb|P \sat S| produces +$P \sat S$. The refinement relation is produced by \verb|\lessdet| (or +\verb|refinedby|, a synonymbol). + +\subsection{Specifications} + +To capture timing constraints at the level of the semantic models, we +use a number of specification `macros'. These are set using \LaTeX\ +macros which begin with an `m' (for macro) and are then capitalised. +\par +\begin{tabular}{p{1.95in}p{1.75in}l} \\ +internal & \verb|\mInternal | & $ \mInternal $ \\[0.4ex] +refuses & \verb|\mRef | & $ \mRef $ \\[0.4ex] +at & \verb|\mAt | & $ \mAt $ \\[0.4ex] +live & \verb|\mLive | & $ \mLive $ \\[0.4ex] +open & \verb|\mOpen | & $ \mOpen $ \\[0.4ex] +from & \verb|\mFrom | & $ \mFrom $ \\[0.4ex] +until & \verb|\mUntil | & $ \mUntil $ \\[0.4ex] +live from & \verb|\mLiveFrom | & $ \mLiveFrom $ \\[0.4ex] +open from & \verb|\mOpenFrom | & $ \mOpenFrom $ \\[0.4ex] +name of last & \verb|\mNameOfLast| & $ \mNameOfLast $ \\[0.4ex] +before & \verb|\mBefore | & $ \mBefore $ \\[0.4ex] +after & \verb|\mAfter | & $ \mAfter $ \\[0.4ex] +time of last & \verb|\mTimeOfLast| & $ \mTimeOfLast $ \\[0.4ex] +\end{tabular} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\section{Discussion} + +\subsection{Dependencies} + +You must have the AMS fonts available, and the {\tt amsfonts} +installation must have been performed for \LaTeXe. This requires the +{\tt mfnfss} package; it takes about twenty seconds. + +\subsection{CSP and Z} + +You may have problems if you try to use the {\tt zed-csp} package with +{\tt fuzz} or any style package that uses the AMS fonts. The good +news is that you shouldn't need them. All of the AMS symbols are +defined in the {\tt zed-csp} package, using the standard names. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\end{document} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/macros/latex/contrib/zed-csp/zed-csp.sty b/macros/latex/contrib/zed-csp/zed-csp.sty new file mode 100644 index 0000000000..c89ce59eda --- /dev/null +++ b/macros/latex/contrib/zed-csp/zed-csp.sty @@ -0,0 +1,789 @@ +% +% >>> zed-csp.sty <<< +% +% (c) Jim Davies, January 1995 + +% You may copy and distribute this file freely. Any queries and +% complaints should be forwarded to Jim.Davies@comlab.ox.ac.uk. + +% If you make any changes to this file, please do not distribute +% the results under the name `zed-csp.sty'. + +% >>> information <<< + +% This is a LaTeX2e package for typesetting Z and CSP notation. It +% employs the standard (JMS) set of macros, but uses the AMS fonts in +% place of `oxsy'. You will need the tfm and fd files for the `A' and +% `B' symbol fonts installed. This requires (1) the AMSFONTS package +% and (2) the MFNFSS package for LaTeX2e. + +% If you have the Lucida Bright font set from Y&Y, then you can use +% that instead. In this case, you have only to load `lucbr' (from the +% PSNFSS package) before `zed-csp'. + +% >>> changes <<< + +% version 0 (Sep 94): first attempt +% version 0a (Oct 94): fixed error in definition of \cat +% version 0b (Nov 94): added composite for \uminus +% version 0c (Jan 95): removed definition of \emptyset + +% >>> date and version <<< + +\def\fileversion{0c} +\def\filedate{95/01/11} +\def\docdate {95/01/11} + +\NeedsTeXFormat{LaTeX2e} + +\ProvidesPackage{zed-csp}[{% + \filedate\space\fileversion\space zed-csp package}] + +% >>> fonts and symbols <<< + +% We declare a new math version. For convenience, I have chosen the +% same name as that used in oz.sty. The following code is based upon +% the work of Paul King, Sebastian Rahtz, and Mike Spivey. Alan +% Jeffrey's influence is everywhere. + +\@ifpackageloaded{lucbr}{}{% + \DeclareMathVersion{zed} + \SetMathAlphabet{\mathrm}{zed}{\encodingdefault}{\rmdefault}{m}{n}% + \SetMathAlphabet{\mathbf}{zed}{\encodingdefault}{\rmdefault}{bx}{n}% + \SetMathAlphabet{\mathsf}{zed}{\encodingdefault}{\sfdefault}{m}{n}% + \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% + \DeclareSymbolFontAlphabet{\mathrm}{operators} + \DeclareSymbolFontAlphabet{\mathit}{letters} + \DeclareSymbolFontAlphabet{\mathcal}{symbols} + \DeclareSymbolFontAlphabet{\zedit}{italics} + \DeclareSymbolFont{lasy}{U}{lasy}{m}{n} + \DeclareSymbolFont{AMSa}{U}{msa}{m}{n} + \DeclareSymbolFont{AMSb}{U}{msb}{m}{n} + \let\mho\undefined + \let\Join\undefined + \let\Box\undefined + \let\Diamond\undefined + \let\leadsto\undefined + \let\sqsubset\undefined + \let\sqsupset\undefined + \let\lhd\undefined + \let\unlhd\undefined + \let\rhd\undefined + \let\unrhd\undefined + \DeclareMathSymbol{\mho}{\mathord}{lasy}{"30} + \DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31} + \DeclareMathSymbol{\Box}{\mathord}{lasy}{"32} + \DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33} + \DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B} + \DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C} + \DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D} + \DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01} + \DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02} + \DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03} + \DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04} + \DeclareSymbolFontAlphabet{\bbold}{AMSb} + \mathversion{zed} + } + +\@ifpackageloaded{lucbr}{% + \DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4} + \DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE} + \DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF} + \DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0} + }{% + \let\rightleftharpoons\undefined + \let\angle\undefined + \DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00} + \DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01} + \DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02} + \DeclareMathSymbol\square{\mathord}{AMSa}{"03} + \DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04} + \DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05} + \DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06} + \DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07} + \DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08} + \DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09} + \DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A} + \DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B} + \DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C} + \DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D} + \DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E} + \DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F} + \DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10} + \DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11} + \DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12} + \DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13} + \DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14} + \DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15} + \DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16} + \DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17} + \DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18} + \DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19} + \DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A} + \DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B} + \DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C} + \DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D} + \DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E} + \DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F} + \DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20} + \DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21} + \DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22} + \DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23} + \DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24} + \DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25} + \DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26} + \DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27} + \DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28} + \DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29} + \DeclareMathSymbol\because{\mathrel}{AMSa}{"2A} + \DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B} + \DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C} + \DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D} + \DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E} + \DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F} + \DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30} + \DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31} + \DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32} + \DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33} + \DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34} + \DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35} + \DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36} + \DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37} + \DeclareMathSymbol\backprime{\mathord}{AMSa}{"38} + \DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A} + \DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B} + \DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C} + \DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D} + \DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E} + \DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F} + \DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40} + \DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41} + \DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42} + \DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43} + \DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44} + \DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45} + \DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46} + \DeclareMathSymbol\between{\mathrel}{AMSa}{"47} + \DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48} + \DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49} + \DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A} + \DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D} + \DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E} + \DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F} + \DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50} + \DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51} + \DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52} + \DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53} + \DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54} + \DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56} + \DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57} + \DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59} + \DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A} + \DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B} + \DeclareMathSymbol\angle{\mathord}{AMSa}{"5C} + \DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D} + \DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E} + \DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F} + \DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60} + \DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61} + \DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62} + \DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63} + \DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64} + \DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65} + \DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66} + \DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67} + \DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68} + \DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69} + \DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A} + \DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B} + \DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C} + \DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D} + \DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E} + \DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F} + \DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70} + \DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71} + \DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78} + \DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79} + \xdef\yen {\noexpand\mathhexbox\hexnumber@\symAMSa 55 } + \xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa 58 } + \xdef\circledR {\noexpand\mathhexbox\hexnumber@\symAMSa 72 } + \xdef\maltese {\noexpand\mathhexbox\hexnumber@\symAMSa 7A } + \DeclareMathSymbol\circledS{\mathord}{AMSa}{"73} + \DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74} + \DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75} + \DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76} + \DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77} + \DeclareMathSymbol\complement{\mathord}{AMSa}{"7B} + \DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C} + \DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D} + \DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E} + \DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F} + \DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00} + \DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01} + \DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02} + \DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03} + \DeclareMathSymbol\nless{\mathrel}{AMSb}{"04} + \DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05} + \DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06} + \DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07} + \DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08} + \DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09} + \DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A} + \DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B} + \DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C} + \DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D} + \DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E} + \DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F} + \DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10} + \DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11} + \DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12} + \DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13} + \DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14} + \DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15} + \DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16} + \DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17} + \DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18} + \DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19} + \DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A} + \DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B} + \DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C} + \DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D} + \DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20} + \DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21} + \DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22} + \DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23} + \DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24} + \DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25} + \DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26} + \DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27} + \DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28} + \DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29} + \DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A} + \DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B} + \DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C} + \DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D} + \DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E} + \DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F} + \DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30} + \DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31} + \DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32} + \DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33} + \DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34} + \DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35} + \DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36} + \DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37} + \DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38} + \DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39} + \DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A} + \DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B} + \DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C} + \DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D} + \DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E} + \DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F} + \DeclareMathSymbol\mho{\mathord}{AMSb}{"66} + \DeclareMathSymbol\eth{\mathord}{AMSb}{"67} + \DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68} + \DeclareMathSymbol\beth{\mathord}{AMSb}{"69} + \DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A} + \DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B} + \DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C} + \DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D} + \DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E} + \DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F} + \DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70} + \DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71} + \DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72} + \DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73} + \DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74} + \DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75} + \DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76} + \DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77} + \DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78} + \DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79} + \DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A} + \DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B} + \DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D} + \DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E} + \DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F} + } + +% A macro name has been chosen for each of the symbols in the AMS +% fonts. There is no need to load any other AMS package in order to +% access these symbols. + +% >>> fuzz <<< + +% This is the standard fuzz setup, apart from the oz style change to +% the setmcodes macro. + +\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 + \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 + \advance\count0 by1 \advance\count1 by1 \repeat}} +\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}% +\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}% + +\def~{\ifmmode\,\else\penalty\@M\ \fi} + +\let\@mc=\mathchardef \mathcode`\;="8000 {\catcode`\;=\active + \gdef;{\semicolon\;}} \@mc\semicolon="603B + +\def\strut@op#1{\mathop{\mathstrut{#1}}\nolimits} + +\def\_{\leavevmode \ifmmode\else\kern0.06em\fi \vbox{\hrule + width0.5em}} + +\mathcode`\"="8000 \def\@kwote#1"{\hbox{\it #1}} {\catcode`\"=\active + \global\let"=\@kwote} + +\mathchardef\spot="320F +\mathcode`\@=\spot +\mathcode`\|=\mid + +\def\bsup#1 \esup{^{#1}} + +\def\inrel#1{\mathrel{\underline{#1}}} + +\newdimen\zedindent \zedindent=\leftmargini% +\newdimen\zedleftsep \zedleftsep=1em% +\newdimen\zedtab \zedtab=2em% +\newdimen\zedbar \zedbar=6em% +\newskip\zedskip \zedskip=0.5\baselineskip plus0.333333\baselineskip% + minus0.333333\baselineskip% +\def\zedsize{}% + +\newcount\interzedlinepenalty \interzedlinepenalty=10000% +\newcount\preboxpenalty \preboxpenalty=0% +\newif\ifzt@p \zt@pfalse% + +\def\@jot{0.5\zedskip} + +\def\@narrow{\advance\linewidth by-\zedindent} + +\def\@zrulefill{\leaders\hrule height\arrayrulewidth\hfill} + +\def\@topline#1{\hbox to\linewidth{% + \vrule height\arrayrulewidth width\arrayrulewidth + \vrule height0pt depth\@jot width0pt + \hbox to\zedleftsep{\@zrulefill\thinspace}% + #1\thinspace\@zrulefill}} + +\def\@zedline{\omit \vrule height\arrayrulewidth width\linewidth \cr} + +\def\where{\@zskip\@jot + \omit \vrule height\arrayrulewidth width\zedbar \cr + \@zskip\@jot} + +\def\also{\crcr \noalign{\penalty\interdisplaylinepenalty + \vskip\zedskip}} +\def\@zskip#1{\crcr \omit \vrule height#1 width\arrayrulewidth \cr} +\def\@zlign{\tabskip\z@skip\everycr{}} + +\let\tie=\t +\def\t#1{\afterassignment\@t\count@=#1} +\def\@t{\hskip\count@\zedtab} + +\def\@setzsize{\let\next=\@nomath\def\@nomath##1{}% + \skip0=\abovedisplayskip\skip1=\belowdisplayskip + \zedsize \let\@nomath=\next + \abovedisplayskip=\skip0\belowdisplayskip=\skip1} + +\def\@zed{\ifvmode\@zleavevmode\fi + $$\global\zt@ptrue + \@setzsize + \advance\linewidth by-\zedindent + \advance\displayindent by\zedindent + \def\\{\crcr}% Must have \def and not \let for nested alignments. + \let\par=\relax + \tabskip=0pt} + +\def\@znoskip{\offinterlineskip + \everycr={\noalign{\ifzt@p \global\zt@pfalse + \ifdim\prevdepth>-1000pt \skip0=\normalbaselineskip + \advance\skip0by-\prevdepth \advance\skip0by-\ht\strutbox + \ifdim\skip0<\normallineskiplimit \vskip\normallineskip + \else \vskip\skip0 \fi\fi + \else \penalty\interzedlinepenalty \fi}}} + +\def\zed{\@zed\@znoskip\halign to\linewidth\bgroup + \strut$\@zlign##$\hfil \tabskip=0pt plus1fil\cr} +\def\endzed{\crcr\egroup$$\global\@ignoretrue} + +\def\[{\begingroup\zed} +\def\]{\crcr\egroup$$\endgroup\ignorespaces} + +\def\axdef{\def\also{\@zskip\zedskip}% + \predisplaypenalty=\preboxpenalty + \@zed\@znoskip \halign to\linewidth\bgroup + \strut \vrule width\arrayrulewidth \hskip\zedleftsep + $\@zlign##$\hfil \tabskip=0pt plus1fil\cr} +\let\endaxdef=\endzed + +\def\schema#1{\@ifnextchar[{\@schema{#1}}{\@nschema{#1}}} +\def\@schema#1[#2]{\@nschema{#1[#2]}} +\def\@nschema#1{\@narrow\axdef \omit\@topline{$\strut#1$}\cr} +\def\endschema{\@zskip\@jot \@zedline \endzed} + +\@namedef{schema*}{\@narrow\axdef \@zedline \@zskip\@jot} +\expandafter\let\csname endschema*\endcsname=\endschema + +\def\gendef{\@ifnextchar[{\@gendef}{\@ngendef}} +\def\@gendef[#1]{\@narrow\axdef \omit \setbox0=\hbox{$\strut[#1]$}% + \rlap{\raise\doublerulesep\@topline{\hskip\wd0}}\@topline{\box0}\cr} +\def\@ngendef{\@narrow\axdef \@zedline \omit \hbox to\linewidth{\vrule + height\doublerulesep width\arrayrulewidth \@zrulefill}\cr + \@zskip\@jot + } +\let\endgendef=\endschema + +\def\argue{\@zed \interzedlinepenalty=\interdisplaylinepenalty + \openup\@jot \halign to\linewidth\bgroup + \strut$\@zlign##$\hfil \tabskip=0pt plus1fil + &\hbox to0pt{\hss[\@zlign##\unskip]}\tabskip=0pt\cr + \noalign{\vskip-\@jot}} +\let\endargue=\endzed + +\def\because#1{\noalign{\vskip-\jot}\cr} + +\def\syntax{\@zed\@znoskip \halign\bgroup + \strut$\@zlign##$\hfil &\hfil$\@zlign{}##{}$\hfil + &$\@zlign##$\hfil\cr} +\let\endsyntax=\endzed + +\def\infrule{\@zed\@znoskip \halign\bgroup + \strut\quad$\@zlign##$\quad\hfil&\quad\@zlign##\hfil\cr} +\let\endinfrule=\endzed + +\def\derive{\crcr \noalign{\vskip\@jot} \omit\@zrulefill + \@ifnextchar[{\@xderive}{\@yderive}} +\def\@xderive[#1]{&$\smash{\lower 0.5ex\hbox{$[\;#1\;]$}}$\cr + \noalign{\vskip\@jot}} +\def\@yderive{\cr \noalign{\vskip\@jot}} + +\def\@zleavevmode{\if@inlabel \indent + \else\if@noskipsec \indent + \else\if@nobreak \global\@nobreakfalse + \everypar={}\abovedisplayskip=0pt\fi + {\parskip=0pt\noindent}\fi\fi} + +% From now on, we must depart from the text of fuzz, as we do not have +% the oxsy symbol font at our disposal. We must choose symbols from +% the AMS or Lucida fonts to compensate for our loss. Sadly, this +% means a number of conditional definitions. I have tried to maintain +% the order of definitions used in fuzz2.sty, rather than factor the +% font-dependent ones out. + +\let\xlambda=\lambda \let\xmu=\mu +\let\xforall=\forall \let\xexists=\exists + +\def \bind {\mathrel{\leadsto}} +\def \bindsto {\mathrel{\leadsto}} + +\@ifpackageloaded{lucbr}{% + \def \lblot {{\langle}\mkern -5mu{|}} + \def \rblot {{|}\mkern -5mu{\rangle}} + }{% + \def \lblot {{\langle}\mkern -3.5mu{|}} + \def \rblot {{|}\mkern -3.5mu{\rangle}} + } + +\let\lbind=\lblot +\let\rbind=\rblot + +\def \defs {\mathrel{\widehat=}} +\def \power {\strut@op{\bbold P}} +\let \cross \times +\def \lambda {\strut@op{\xlambda}} +\def \mu {\strut@op{\xmu}} +\@ifpackageloaded{lucbr}{}{ + \def\ldbrack{{[}\mkern-2mu{[}} + \def\rdbrack{{]}\mkern-2mu{]}}} +\let \lbag \ldbrack +\let \rbag \rdbrack +\def \lnot {\neg\;} +\def \land {\mathrel{\wedge}} +\def \lor {\mathrel{\vee}} +\let \implies \Rightarrow +\let \iff \Leftrightarrow +\def \forall {\strut@op{\xforall}} +\def \exists {\strut@op{\xexists}} +\def \hide {\mathrel{\backslash}} +\@ifpackageloaded{lucbr}{% + \DeclareMathSymbol{\project}{3}{arrows}{"75}}{% + \DeclareMathSymbol{\project}{\mathrel}{AMSa}{"16}} +\def \pre {{\mathrm{pre}}\;} +\def \semi {\mathrel{\comp}} +\def \ldata {\langle\!\langle} +\def \rdata {\rangle\!\rangle} +\let \shows \vdash +\def \pipe {\mathord>\!\!\mathord>} +\def \LET {{\mathbf{let}}\;} +\def \IF {{\mathbf{if}}\;} +\def \THEN {\mathrel{\mathbf{then}}} +\def \ELSE {\mathrel{\mathbf{else}}} + +\let \rel \leftrightarrow +\def \dom {\mathop{\mathrm{dom}}} +\def \ran {\mathop{\mathrm{ran}}} +\def \id {\mathop{\mathrm{id}}} +\@ifpackageloaded{lucbr}{% + \def\comp{\mathrel{\raise 0.66ex\hbox{\oalign{\hfil% + $\scriptscriptstyle\mathsf{o}$\hfil% + \cr\hfil$\scriptscriptstyle\mathsf{9}$\hfil}}}} + \DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F} + \DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E}}{% + \def\comp{\mathbin{\raise 0.6ex\hbox{\small\oalign{\hfil% + $\scriptscriptstyle\mathrm{o}$\hfil% + \cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}} + \DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43} + \DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42} + } +\def \ndres {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}} +\def \nrres {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}} +\def \inv {^\sim} +\def \limg {(\!|} +\def \rimg {|\!)} + +\def\@p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern + 5mu$\hfil\cr$#1$}}} +\def \pfun {\@p\fun} +\let \fun \rightarrow +\let \inj \rightarrowtail +\@ifpackageloaded{lucbr}{% + \DeclareMathSymbol{\pinj}{3}{arrows}{"92} + \def \surj {\mathrel{\ooalign{$\fun$\hfil\cr$\mkern3mu\fun$}}} + \def \bij {\mathrel{\ooalign{$\inj$\hfil\cr$\mkern4mu\fun$}}}}{% + \def \pinj {\@p\inj} + \def \surj {\mathrel{\ooalign{$\fun$\hfil\cr$\mkern4mu\fun$}}} + \def \bij {\mathrel{\ooalign{$\inj$\hfil\cr$\mkern5mu\fun$}}}} +\def \psurj {\@p\surj} +\def \nat {{\bbold N}} +\def \num {{\bbold Z}} +\def \div {\mathbin{\mathsf{div}}} +\def \mod {\mathbin{\mathsf{mod}}} +\def \upto {\mathbin{\ldotp\ldotp}} +\def \plus {^+} +\def \star {^*} +\def \finset {\strut@op{{\bbold F}}} +\def\@f#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 3mu + \mapstochar\mkern 5mu$\hfil\cr$#1$}}} +\def \ffun {\@f\fun} +\def \finj {\@f\inj} +\def \seq {\mathop{\mathrm{seq}}} +\def \iseq {\mathop{\mathrm{iseq}}} +\def \cat {\mathbin{\raise 0.8ex\hbox{$\smallfrown$}}} +\def \filter {\mathbin{\project}} +\def \dcat {\mathop{\cat/}} +\def \bag {\mathop{\mathrm{bag}}} +\def \bcount {\mathbin{\sharp}} +\def \inbag {\mathrel{\mathrm{in}}} +\let \subbageq \sqsubseteq +\def \disjoint {{\mathsf{disjoint}}\;} +\def \partition {\mathrel{\mathsf{partition}}} +\def \prefix {\mathrel{\mathsf{prefix}}} +\def \suffix {\mathrel{\mathsf{suffix}}} +\def \inseq {\mathrel{\mathsf{in}}} +\def \extract {\mathrel{\upharpoonleft}} + +\def \uminus@sym{\setbox0=\hbox{$\cup$}\rlap{\hbox + to\wd0{\hss\raise0.3ex\hbox{$\scriptscriptstyle{-}$}\hss}}\box0} +\def \uminus {\mathrel{\uminus@sym}} + +% If you are not using csp notation, then feel free to uncomment the +% following: + +% \endinput + + +% >>> csp <<< + +% We require the following mathematical symbols and aliases when +% specifying and reasoning about the behaviour of CSP processes. + +\let \Inter \bigcap +\let \Land \bigwedge +\let \Lor \bigvee +\let \Union \bigcup +\let \inter \cap +\def \nin {\not\in} +\let \union \cup +\def \rat {{\bbold Q}} +\def \real {{\bbold R}} +\def \cnt {\mathrel{\downarrow}} +\def \data {\mathrel{\Downarrow}} +\def \during {\mathrel{\uparrow}} +\def \nil {\trace{}} +\def \clause {\Bigm{|}} +\def \contig {\mathrel{\mathbf{in}}} +\def \trace#1{\langle #1\rangle} +\def \set#1{\{#1\}} +\let \ge \geqslant +\let \le \leqslant +\@ifpackageloaded{lucbr}{% + \DeclareMathSymbol{\tick}{0}{arrows}{"AC} + }{ + \DeclareMathSymbol{\tick}{0}{AMSa}{"58} + } + +\let \subseq \preccurlyeq + +% We define a number of useful macros for projecting information from +% a timed or untimed observation. + +\def \Begin {\strut@op{\mathrm{begin}}} +\def \End {\strut@op{\mathrm{end}}} +\def \Head {\strut@op{\mathrm{head}}} +\def \First {\strut@op{\mathrm{first}}} +\def \Tail {\strut@op{\mathrm{tail}}} +\def \Front {\strut@op{\mathrm{front}}} +\def \Last {\strut@op{\mathrm{last}}} +\def \Times {\strut@op{\mathrm{times}}} +\def \Events {\strut@op{\mathrm{events}}} +\def \Reverse {\strut@op{\mathrm{reverse}}} + +% We define a number of useful macros for specification purposes. + +\def\@PreMacro#1{\mathop{\mbox{\sffamily #1}}} +\def\@InMacro#1{\mathrel{\mbox{\sffamily #1}}} +\def\@@InMacro#1^#2{\;\mbox{\sffamily #1}^{#2}\;} +\def\@SupInMacro#1{\@ifnextchar^{\@@InMacro{#1}}{\@InMacro{#1}}} + +\def \mInternal {\@PreMacro{internal}} +\def \mRef {\@InMacro{ref}} +\def \mAt {\@SupInMacro{at}} +\def \mLive {\@SupInMacro{live}} +\def \mOpen {\@SupInMacro{open}} +\def \mFrom {\@InMacro{from}} +\def \mUntil {\@InMacro{until}} +\def \mLiveFrom {\@InMacro{live from}} +\def \mOpenFrom {\@InMacro{open from}} +\def \mNameOfLast {\@InMacro{name of last}} +\def \mBefore {\@InMacro{before}} +\def \mAfter {\@InMacro{after}} +\def \mTimeOfLast {\@InMacro{time of last}} + +% We define a conditional syntax for processes. This is an expression +% conditional, and should not be confused with the command conditional +% of programming languages. That is, if the boolean condition is +% true, then the expression under consideration is equal to the +% expression in the first branch. + +\def \If {\mathrel{\hbox{if}}} +\def \Then {\mathrel{\hbox{then}}} +\def \Otherwise {\mathrel{\hbox{otherwise}}} +\def \Else {\mathrel{\hbox{else}}} +\def \Fi {\mathrel{\hbox{fi}}} + +% In defining macros to set the syntax of real-time CSP, some symbols +% are used more than once. For ease of understanding, we define these +% symbols as internal macros. + +\def \csp@at {\hbox{\it @}} +\def \csp@bar {\mathord{\mid}} +\def \csp@chain {\mathord{\gg}} +\def \csp@ext {\mathord{\Box}} +\def \csp@int {\mathord{\sqcap}} +\def \csp@par {\mathord{\xparallel}} + +\def \csp@interrupt {\mathord{\triangle}} +\def \csp@timeout {\mathord{\triangleright}} + +\@ifpackageloaded{lucbr}{% + \def \csp@leftpar {\csp@bar\mkern -3mu{[}} + \def \csp@rightpar {{]}\mkern -3mu\csp@bar} + \def \csp@interleave {\csp@bar\mkern-2mu\csp@bar\mkern-2mu\csp@bar} + \DeclareMathSymbol{\csp@transfer}{0}{arrows}{"93} + }{ + \def \csp@leftpar {\csp@bar{[}} + \def \csp@rightpar {{]}\csp@bar} + \def \csp@interleave {\csp@bar\csp@bar\csp@bar} + \def \csp@transfer {\mathord{\swarrow}} + } + +% We define a quick hack to magnify the indexed forms of the choice +% and parallel composition operators. It seems to work okay. + +\def\indexed@op#1{% + \mathop{\vcenter{\hbox{\Large$\mathstrut#1$}}}\nolimits} + +% We are now ready to define the macros used for setting the syntax of +% real-time CSP. Notice that the LaTeX version of \parallel *must* be +% saved as \xparallel at this point. + +\let\xparallel \parallel + +\def \Bottom {\mathord{\perp}} +\def \Chaos {{Chaos}} +\def \Stop {{Stop}} +\def \Skip {{Skip}} +\def \Wait {\strut@op{{Wait}}} +\def \at {\mathord{\csp@at}} +\def \then {\@ifnextchar[{\@then}{\mathrel{\rightarrow}}} +\def \@then[#1]{\buildrel #1\over\rightarrow} +\def \barchoice {\mathrel{\csp@bar}} +\def \intchoice {\mathrel{\csp@int}} +\def \extchoice {\mathrel{\csp@ext}} +\def \interrupt {\mathrel{\csp@interrupt}} +\def \timeout {\@ifnextchar[{\@timeout}{\mathrel{\csp@timeout}}} +\def \@timeout[#1]{\mathrel{\csp@timeout\{#1\}}} +\def \transfer {\@ifnextchar[{\@transfer}{\mathrel{\csp@transfer}}} +\def \@transfer[#1]{\mathrel{\csp@transfer\{#1\}}} +\def \parallel {\@ifnextchar[{\@parallel}{\mathrel{\csp@par}}} +\def \@parallel[#1]{\@ifnextchar[{\@@parallel[#1]}{% + {\mathrel{\,\csp@leftpar\,{#1}\,\csp@rightpar\,}}}} +\def \@@parallel[#1][#2]{\mathrel{\,\csp@leftpar\,{#1}\, + \csp@bar\,{#2}\,\csp@rightpar\,}} +\def \interleave{\mathrel{\csp@interleave}} +\def \chain {\mathrel{\csp@chain}} +\def \Intchoice {\indexed@op{\csp@int}} +\def \Extchoice {\indexed@op{\csp@ext}} +\def \Parallel {\indexed@op{\csp@par}} +\def \Interleave{\indexed@op{\csp@interleave}} + +\def \@semapp[#1]{\,\ldbrack #1 \rdbrack} +\def \sem@fun#1{{#1}\@ifnextchar[{\@semapp}{}} +\def \Semantics {\sem@fun{semantics}} +\def \Traces {\sem@fun{traces}} +\def \Failures {\sem@fun{failures}} +\def \TimedTraces {\sem@fun{timed\,traces}} +\def \TimedFailures {\sem@fun{timed\,failures}} +\def \Divergences {\sem@fun{divergences}} +\def \Infinites {\sem@fun{infinites}} + +\def \lessdet{\@ifnextchar[{\@lessdet}{\mathrel\sqsubseteq}} +\def \@lessdet[#1]{\@ifnextchar[{\lessdet@two[#1]}{\lessdet@one[#1]}} +\def \lessdet@one[#1]{\mathrel{\sqsubseteq_{#1}}} +\def \lessdet@two[#1][#2]{% + \mathrel{{\vphantom{\sqsubseteq}}_{#1}{\sqsubseteq}_{#2}}} + +\let \refinedby \lessdet + +\def \sat {\mathrel{\mbox{\bf sat}}} +\def \semb#1{{\ldbrack #1 \rdbrack}} + +% The following symbols have been used by researchers at Oxford to +% denote the various semantic models, spaces, and functions. + +\def\UT{UT} \def\TE{TE} \def\TT{TT} +\def\RT{RT} \def\TR{TR} \def\TI{TI} +\def\TTi{\TT^i} \def\TTw{\TT^\omega} \def\TRu{\TR^u} + +\def\@obsmodel#1{{\cal{O}}_{#1}} +\def\@obsspace#1{{\cal{S}}_{#1}} +\def\@semmodel#1{{\cal{M}}_{#1}} +\def\@semfunct#1{{\cal{F}}_{#1}\@ifnextchar[{\@semapp}{}} + +\def\Out {\@obsmodel{UT}} \def\Sut {\@obsspace{UT}} +\def\Ouf {\@obsmodel{UF}} \def\Suf {\@obsspace{UF}} +\def\Oufd {\@obsmodel{UFD}} \def\Sufd {\@obsspace{UFD}} +\def\Otf {\@obsmodel{TF}} \def\Stf {\@obsspace{TF}} +\def\Otfs {\@obsmodel{TFS}} \def\Stfs {\@obsspace{TFS}} +\def\Oti {\@obsmodel{TI}} \def\Sti {\@obsspace{TI}} + +\def\Mut {\@semmodel{UT}} \def\Fut {\@semfunct{UT}} +\def\Muf {\@semmodel{UF}} \def\Fuf {\@semfunct{UF}} +\def\Mufd {\@semmodel{UFD}} \def\Fufd {\@semfunct{UFD}} +\def\Mtf {\@semmodel{TF}} \def\Ftf {\@semfunct{TF}} +\def\Mtfs {\@semmodel{TFS}} \def\Ftfs {\@semfunct{TFS}} +\def\Mti {\@semmodel{TI}} \def\Fti {\@semfunct{TI}} + +\endinput diff --git a/macros/latex/contrib/zed-csp/zed2e.pdf b/macros/latex/contrib/zed-csp/zed2e.pdf new file mode 100644 index 0000000000..0f6daf8654 Binary files /dev/null and b/macros/latex/contrib/zed-csp/zed2e.pdf differ diff --git a/macros/latex/contrib/zed-csp/zed2e.tex b/macros/latex/contrib/zed-csp/zed2e.tex new file mode 100644 index 0000000000..ae6a4d41e6 --- /dev/null +++ b/macros/latex/contrib/zed-csp/zed2e.tex @@ -0,0 +1,774 @@ +% STOLEN VERSION of ``zguide.tex'' 11th December 1990 +% Copyright (C) J. M. Spivey 1990 + +% The zed style option and its documentation may be freely copied, +% distributed and used for any purpose except direct commercial gain, +% provided that they are copied and distributed as a whole and without +% modification. The author accepts no liablility for their accuracy or +% fitness for any purpose. + +\documentclass{article} + +\usepackage{zed-csp} + +\def\fuzz{{\large\it f\kern0.1em}{\normalsize\sc uzz}} +\let\Fuzz=\fuzz +\def\ZRM{{\rm ZRM}} + +\makeatletter % Oh-ho: here comes some more lark's vomit ... + +\def\demo{\par\vbox\bgroup\begingroup\quote} +\def\gives{\endquote\endgroup\egroup} +\def\enddemo{\global\@ignoretrue} + +% Try doing this in pure LaTeX without `visual formatting'! +\def\symtab{\setbox0=\vbox\bgroup \def\\{\cr} + \halign\bgroup\strut$##$\hfil&\quad##\hfil\cr} +\def\endsymtab{\crcr\egroup\egroup + \dimen0=\ht0 \divide\dimen0 by2 \advance\dimen0 by\ht\strutbox + \splittopskip=\ht\strutbox \vbadness=10000 + \predisplaypenalty=0 + $$\halign{##\cr\hbox to\linewidth{% + \valign{##\vfil\cr + \setbox1=\vsplit0 to\dimen0 \unvbox1\cr + \noalign{\hfil}\unvbox0\cr + \noalign{\hfil}}}\cr + \noalign{\prevdepth=\dp\strutbox}}$$ + \global\@ignoretrue} + +\makeatother % Sanity is restored + +\begin{document} + +\title{A guide to the {\tt zed} style option} +\author{Mike Spivey} +\date{December 1990} +\maketitle + +\section{Introduction} + +This document is a guide to the version of the {\tt zed} style option +for \LaTeX\ dated 11th December 1990. This new version of the style +option is fully compatible with the {\tt fuzz} style option +distributed with the my \fuzz\ type-checker for Z, but uses two fonts +from the AMS in place of the special Z font distributed with +\fuzz. Some of the symbols have been cobbled together by combining +two or more characters, but the results are good enough for rough +drafts. The style option requires the `old' AMS fonts, and will not at +present work with Sli\TeX\ or the Sch\"opf-Mittelbach font selection +scheme. + +The rest of this guide is mostly extracted from the manual for \fuzz, +and it assumes a basic knowledge of \LaTeX. I have not removed some +information about how the \fuzz\ type-checker treats various +constructs, in case you later want to type-check a document you have +formatted with the {\tt zed} style option. For information about the +\fuzz\ package and how to order it, see the end of this guide. + +This guide and the {\tt zed} style option itself may be freely copied, +distributed and used for any purpose except direct commercial gain, +provided that they are copied and distributed as a whole and without +modification. The author accepts no liablility for their accuracy or +fitness for any purpose. + +\section{Loading the {\tt zed} style option} + +Every \LaTeX\ document should begin with a \verb/\documentstyle/ +command. If the document contains a Z specification, this command +should include the style option \verb/zed/. For example: +\begin{quote} + \verb/\documentstyle[12pt,zed]{article}/ +\end{quote} +Including \verb/zed/ as a style option loads macros from the file +\verb/zed.sty/ and also loads four fonts of extra mathematical symbols +called \verb/msxm9/, \verb/msym9/, \verb/msxm10/, and \verb/msym10/. +Your \LaTeX\ installation must have these fonts for the \verb/zed/ +style option to work; if it doesn't, or they are in the wrong place to +be found by \TeX, then you will get an error message like this: +\begin{quote} + \verb/! Font \ninsxm=msxm9 not loadable .../ +\end{quote} +The \verb/zed/ style option can be used with any of the standard +\LaTeX\ styles, and it can appear either before or after the type-size +option if one is used. It can be combined with most of the standard +style options, but it should not be combined with \verb/fleqn/, +because {\tt zed} already makes provision for setting mathematics +flush left. At present, \verb/zed/ does not work with Sli\TeX. + +\section{Making boxes} + +To print a schema, use the \verb/schema/ environment. Here is an +example, showing first the input, then the output from \LaTeX: +\begin{demo} +\begin{verbatim} +\begin{schema}{PhoneDB} + known: \power NAME \\ phone: NAME \pfun PHONE +\where + known = \dom phone +\end{schema} +\end{verbatim} +\gives +\begin{schema}{PhoneDB} + known: \power NAME \\ phone: NAME \pfun PHONE +\where + known = \dom phone +\end{schema} +\end{demo} +The name of the schema appears as an argument to the environment, and +the horizontal dividing line between declarations and predicates is +indicated by \verb/\where/. Successive lines in the declaration and +predicate parts are separated by the command \verb/\\/. In this +example, the Z symbols `$\power$', `$\pfun$' and `$\dom$' have been +entered as the commands \verb/\power/, \verb/\pfun/ and \verb/\dom/: +for a complete list of these commands, see Section~\ref{s:symtabs} +below. + +Like the \verb/displaymath/ environment of \LaTeX, the \verb/schema/ +environment (and the others we shall come to in a moment) can appear +in the middle of a paragraph, and ordinarily should have no blank +lines either before or after it. Blank lines before the environment +are ignored, but blank lines afterwards cause the following text to +begin a new paragraph. + +For a schema without a predicate part, the command \verb/\where/ is +simply omitted, as in the following example: +\begin{demo} +\begin{verbatim} +\begin{schema}{Document[CHAR]} + left, right: \seq CHAR +\end{schema} +\end{verbatim} +\gives +\begin{schema}{Document[CHAR]} + left, right: \seq CHAR +\end{schema} +\end{demo} +This example also shows how to set schemas with generic parameters. + +For axiomatic descriptions, the \verb/axdef/ environment is used. +Here is an example: +\begin{demo} +\begin{verbatim} +\begin{axdef} + limit: \nat +\where + limit \leq 65535 +\end{axdef} +\end{verbatim} +\gives +\begin{axdef} + limit: \nat +\where + limit \leq 65535 +\end{axdef} +\end{demo} +In both kinds of box, predicates and declarations can be split between +lines before or after infixed symbols, as shown in the following +example: +\begin{demo} +\begin{verbatim} +\begin{axdef} + policy: \power_1 RESOURCE \fun RESOURCE +\where + \forall S: \power_1 RESOURCE @ \\ +\t1 policy(S) \in S +\end{axdef} +\end{verbatim} +\gives +\begin{axdef} + policy: \power_1 RESOURCE \fun RESOURCE +\where + \forall S: \power_1 RESOURCE @ \\ +\t1 policy(S) \in S +\end{axdef} +\end{demo} +The strange hint \verb/\t1/ in this example makes the corresponding +line in the output have one helping of indentation. As things get +more nested, you can say \verb/\t2/, \verb/\t3/, and so on. But if +you should ever get beyond \verb/t9/, you'll need to use braces around +the argument: \verb/\t{10}/, and you'd better look for some way to +simplify your specification! + +This system of tab stops is a little crude, but it is easier to use +than the alternatives, and usually gives acceptable results. The +\verb/\t/$n$ commands are completely ignored by the type-checker, +so you are free to use them as you like to improve the look of your +specification. The size of `helping' you get with +\verb/\t/$n$ is a style parameter \verb/\zedindent/, and the default +is 2em. + +For generic definitions, there's the \verb/gendef/ environment: for +example, +\begin{demo} +\begin{verbatim} +\begin{gendef}[X,Y] + first: X \cross Y \fun X +\where + \forall x: X; y: Y @ \\ +\t1 first(x,y) = x +\end{gendef} +\end{verbatim} +\gives +\begin{gendef}[X,Y] + first: X \cross Y \fun X +\where + \forall x: X; y: Y @ \\ +\t1 first(x,y) = x +\end{gendef} +\end{demo} +In this environment, the formal generic parmeters are an optional +argument. Omitting this argument results in a box with a solid double +bar at the top, which can be used for uniquely defining non-generic +constants. + +If a schema or other box contains more than one predicate below the +line, it often looks better to add a small vertical space between +them. This can be done with the command \verb/\also/: +\begin{demo} +\begin{verbatim} +\begin{schema}{AddPhone} + \Delta PhoneDB \\ name?: NAME \\ number?: PHONE +\where + name? \notin known +\also + phone' = phone \oplus \{name? \mapsto number?\} +\end{schema} +\end{verbatim} +\gives +\begin{schema}{AddPhone} + \Delta PhoneDB \\ name?: NAME \\ number?: PHONE +\where + name? \notin known +\also + phone' = phone \oplus \{name? \mapsto number?\} +\end{schema} +\end{demo} + +Some Z paragraphs do not appear in boxes, and for these the \verb/zed/ +environment is used: +\begin{demo} +\begin{verbatim} +\begin{zed} + [NAME, DATE] +\also + REPORT ::= ok | unknown \ldata NAME \rdata +\also + \exists n: NAME @ \\ +\t1 birthday(n) \in December. +\end{zed} +\end{verbatim} +\gives +\begin{zed} + [NAME, DATE] +\also + REPORT ::= ok | unknown \ldata NAME \rdata +\also + \exists n: NAME @ \\ +\t1 birthday(n) \in December. +\end{zed} +\end{demo} +This environment should be used for basic type definitions, +constraints, abbreviation definitions, free type definitions, and the +horizontal form of schema definitions. As the example illustrates, a +full stop or comma is allowed just before the closing \verb/\end/ +command of any of the Z environments, if that suits your taste (or is +forced on you by a publisher's house rules). This punctuation is +ignored by the type-checker. + +For large free type definitions, the \verb/syntax/ environment +provides a useful alternative to the \verb/zed/ environment, as the +following example suggests: +\begin{demo} +\begin{verbatim} +\begin{syntax} + OP & ::= & plus | minus | times | divide +\also + EXP & ::= & const \ldata \nat \rdata \\ + & | & binop \ldata OP \cross EXP \cross EXP \rdata +\end{syntax} +\end{verbatim} +\gives +\begin{syntax} + OP & ::= & plus | minus | times | divide +\also + EXP & ::= & const \ldata \nat \rdata \\ & | & binop \ldata OP +\cross EXP \cross EXP \rdata +\end{syntax} +\end{demo} +Just as in the \verb/eqnarray/ environment of \LaTeX, the fields are +separated by \verb/&/ characters, and these are ignored by the +type-checker. + +\section{Inside the boxes}\label{s:symtabs} + +The first thing to notice about the text inside the boxes is that +multi-character identifiers look better than they do with ordinary +\LaTeX: instead of $\mit specifications$, you get $specifications$. +The letters are not spread apart, and ligatures like $fi$ are used. +This is achieved by an adjustment to the way \TeX\ treats letters in +mathematical formulas, and no special commands are needed in the input +file. Embedded underline characters can be set with the \verb/\_/ +command, which is also used for dummy arguments of operators: +\verb/not\_known/ gives $not\_known$, and \verb/\_ + \_/ gives +$\_ + \_$~. + +The various special symbols of the Z language and library have +mnemonic names. Some of these names are the same as in ordinary +\LaTeX, and some symbols have new names more suggestive of their +meaning in Z. The spaces inserted around the symbols have been +adjusted to make them look better in Z specifications. + +A few symbols have two names, reflecting two different uses for the +symbol in Z. The symbol $\semi$ is called \verb/\semi/ when it is used +as an operation on schemas, and \verb/\comp/ when it is used for +composition of relations. The symbol $\hide$ is called \verb/\hide/ as +the hiding operator of the schema calculus, and \verb/\setminus/ for +the set difference operator. The symbol $\project$ is called +\verb/project/ as the schema projection operator, and \verb/\filter/ +for filtering of sequences. The spaces around the schema operations +are a little larger, and the type-checker recognizes each name only in +the appropriate context. + +For most symbols, two attributes are of interest: the syntactic class +({\sf In-Fun}, \dots) assigned to it by the type-checker, and the kind +of symbol \LaTeX\ generates from it. The first of these affects the +parsing of an expression containing the symbol, and the second affects +the way spaces will be inserted when the expression is printed. In the +description below, `thin', `medium' and `thick' spaces are the same as +those produced by the \LaTeX\ commands \verb/\,/ and \verb/\:/ and +\verb/\;/ respectively. + +Here are the mnemonics for the basic elements of the Z language: +\begin{symtab} + \power & \verb/\power/ \\ + \cross & \verb/\cross/ \\ + \in & \verb/\in/ \\ + | & \verb/|/ or \verb/\mid/ \\ + @ & \verb/@/ or \verb/\spot/ \\ + \theta & \verb/\theta/ \\ + \lambda & \verb/\lambda/ \\ + \mu & \verb/\mu/ \\ + \Delta & \verb/\Delta/ \\ + \Xi & \verb/\Xi/ \\ + \defs & \verb/\defs/ +\end{symtab} +The operators of propositional logic and the schema calculus are as +follows. Many of these names are already defined by \LaTeX, but the +spacing is often adjusted to make them look better in Z +specifications. +\begin{symtab} + \lnot & \verb/\lnot/ \\ + \land & \verb/\land/ \\ + \lor & \verb/\lor/ \\ + \implies & \verb/\implies/ \\ + \iff & \verb/\iff/ \\ + \forall & \verb/\forall/ \\ + \exists & \verb/\exists/ \\ + \exists_1 & \verb/\exists_1/ \\ + \hide & \verb/\hide/ \\ + \project & \verb/\project/ \\ + \pre & \verb/\pre/ \\ + \semi & \verb/\semi/ +\end{symtab} +Here are the various sorts of fancy brackets: +\begin{symtab} + \{\ldots\} & \verb/\{ ... \}/ \\ + \langle\ldots\rangle & \verb/\langle ... \rangle/ \\ + \lbag\ldots\rbag & \verb/\lbag ... \rbag/ \\ + \ldata\ldots\rdata & \verb/\ldata ... \rdata/ \\ + \ldots\limg\ldots\rimg & \verb/... \limg ... \rimg/ +\end{symtab} +Those are all the symbols `built-in' to the Z language; now for the +symbols defined as part of the mathematical tool-kit. First come the +symbols which are not defined as infix operators, etc.: +\begin{symtab} + \empty & \verb/\empty/ \\ + \bigcup & \verb/\bigcup/ \\ + \bigcap & \verb/\bigcap/ \\ + \dom & \verb/\dom/ \\ + \ran & \verb/\ran/ \\ + \nat & \verb/\nat/ \\ + \num & \verb/\num/ \\ + \nat_1 & \verb/\nat_1/ \\ + \# & \verb/\#/ \\ + \dcat & \verb/\dcat/ +\end{symtab} +Here are the infix function symbols; they are defined in \LaTeX\ as +binary operators, so medium spaces are inserted automatically. The +type-checker recognizes them as of class {\sf In-Fun}. Each symbol is +shown with its priority: +\begin{symtab} + \mapsto & \verb/\mapsto/\quad\hfill 1 \\ + \upto & \verb/\upto/\quad\hfill 2 \\ + + & \verb/+/\quad\hfill 3 \\ + - & \verb/-/\quad\hfill 3 \\ + \cup & \verb/\cup/\quad\hfill 3 \\ + \setminus & \verb/\setminus/\quad\hfill 3 \\ + \cat & \verb/\cat/\quad\hfill 3 \\ + \uplus & \verb/\uplus/\quad\hfill 3 \\ + * & \verb/*/\quad\hfill 4 \\ + \div & \verb/\div/\quad\hfill 4 \\ + \mod & \verb/\mod/\quad\hfill 4 \\ + \cap & \verb/\cap/\quad\hfill 4 \\ + \comp & \verb/\comp/\quad\hfill 4 \\ + \circ & \verb/\circ/\quad\hfill 4 \\ + \filter & \verb/\filter/\quad\hfill 4 \\ + \oplus & \verb/\oplus/\quad\hfill 5 \\ + \dres & \verb/\dres/\quad\hfill 6 \\ + \rres & \verb/\rres/\quad\hfill 6 \\ + \ndres & \verb/\ndres/\quad\hfill 6 \\ + \nrres & \verb/\nrres/\quad\hfill 6 +\end{symtab} +The postfix function symbols (class {\sf Post-Fun}) all produce +superscripts: +\begin{symtab} + \inv & \verb/\inv/ \\ + \plus & \verb/\plus/ \\ + \star & \verb/\star/ \\ + \bsup n \esup & \verb/\bsup n \esup/ +\end{symtab} +As an example, \verb/R \star/ is printed as $R \star$. For iteration, +the commands \verb/\bsup ... \esup/ should be used: for example, +\verb/R \bsup n \esup/ is printed as $R \bsup n \esup$. The +type-checker regards this formula as equivalent to $iter~n~R$, as +explained on page 112 of the \ZRM. + +The infix relation symbols (class {\sf In-Rel}) are defined in +\LaTeX\ as relations, so thick spaces are inserted around them +automatically: +\begin{symtab} + \neq & \verb/\neq/ \\ + \notin & \verb/\notin/ \\ + \subseteq & \verb/\subseteq/ \\ + \subset & \verb/\subset/ \\ + < & \verb/ & \verb/>/ \\ + \leq & \verb/\leq/ \\ + \geq & \verb/\geq/ \\ + \partition & \verb/\partition/ \\ + \inbag & \verb/\inbag/ \\ +\end{symtab} +There is only one prefix relation symbol (class {\sf Pre-Rel}). It +separates itself from an argument with a thick space: +\begin{symtab} + \disjoint & \verb/\disjoint/ +\end{symtab} +The infix generic symbols are seen by \LaTeX\ as relation symbols, so +they are surrounded by thick spaces. Of course, the type-checker +itself assigns them class {\sf In-Gen}: +\begin{symtab} + \rel & \verb/\rel/ \\ + \pfun & \verb/\pfun/ \\ + \fun & \verb/\fun/ \\ + \pinj & \verb/\pinj/ \\ + \inj & \verb/\inj/ \\ + \psurj & \verb/\psurj/ \\ + \surj & \verb/\surj/ \\ + \bij & \verb/\bij/ \\ + \ffun & \verb/\ffun/ \\ + \finj & \verb/\finj/ +\end{symtab} +Prefix generic symbols are assigned class {\sf Pre-Gen} by the +type-checker; in \LaTeX, they are defined as operator symbols, so that +a thin space is inserted between the symbol and a following generic +parameter: +\begin{symtab} + \power_1 & \verb/\power_1/ \\ + \id & \verb/\id/ \\ + \finset & \verb/\finset/ \\ + \finset_1 & \verb/\finset_1/ \\ + \seq & \verb/\seq/ \\ + \seq_1 & \verb/\seq_1/ \\ + \iseq & \verb/\iseq/ \\ + \bag & +\verb/\bag/ +\end{symtab} + +\section{Fine points} + +In math mode, which is used for type-setting the contents of Z boxes, +\TeX\ ignores all space characters in the input file. The spaces which +appear between elements of a mathematical formula are determined by +\TeX\ itself, working from information about the symbols in the +formula. Although this information has been adjusted in the {\tt zed} +style option to make Z texts look as balanced as possible, there are +one or two situations in which \TeX\ needs a little help. + +Special care is needed when function application is indicated by +juxtaposing two identifiers, as in the expression $rev~words$. This +expression should be typed as % +\verb/rev~words/. Typing just % +\verb/rev words/ results in the output $rev words$, since \TeX\ ignores the +space separating the two identifiers. In a formula, the character +% +\verb/~/ inserts the same amount of space as the \LaTeX\ % +\verb/\,/ +command, but it looks better in the input file. The type-checker +completely ignores both the % +\verb/~/ character and the \LaTeX\ spacing +commands, except that it issues a warning if it finds that a needed +one is missing, for example, between two identifiers. It is not +necessary to separate symbols like % +\verb/\dom/ and % +\verb/\ran/ from +their arguments with a % +\verb/~/, because \TeX\ inserts the right +amount of space automatically. For example, the input % +\verb/\dom f/ +produces $\dom f$. + +It is good style also to insert small spaces inside the braces of a +set comprehension, as in this example: +\begin{demo} +% +\verb/\{~x: \nat | x \leq 10 @ x * x~\}/ +\gives +\[\{~x: \nat | x \leq 10 @ x * x~\}\] +\end{demo} +This helps to distinguish it visually from a set display, which should +not have the space: +\begin{demo} +% +\verb/\{1, 2, 3\}/ +\gives +\[\{1, 2, 3\}\] +\end{demo} +The space symbol % +\verb/~/ is ignored by the type-checker, so this is +purely a matter of appearance. It also looks better if you add small +spaces inside the square brackets of `horizontal' schema texts. + +\TeX\ also needs help when a binary operator appears at the end of a +line, as in the following example: +\begin{demo} +\begin{verbatim} +\begin{zed} + directory' = directory \cup {} \\ +\t3 \{new\_name? \mapsto new\_number?\} +\end{zed} +\end{verbatim} +\gives +\begin{zed} + directory' = directory \cup {} \\ +\t3 \{new\_name? \mapsto new\_number?\} +\end{zed} +\end{demo} +\TeX\ will not recognize % +\verb/\cup/ as a binary operator and insert +the correct space unless it is surrounded by two operands, so the +dummy operand % +\verb/{}/ has been inserted: this is ignored by the +type-checker. This problem affects only binary operators; relation +signs do not need to be surrounded by arguments to be recognized by +\TeX. + +\section{Bits and pieces} + +Specification documents often contain mathematical text which does not +form part of the specification proper. This section describes some +environments for setting various kinds of mathematics; they are +provided for convenience, and they are all ignored by the +type-checker. Besides these environments for making displays, run-in +mathematics can be set with the usual % +\verb/math/ environment, or with +the commands % +\verb/$ ... $/ or \hbox{% +\verb/\( ... \)/}. All the Z +symbols listed in Section~\ref{s:symtabs} can be used with these +commands. + +The simplest display environment is provided by the commands +% +\verb/\[ ... \]/. This form acts just like % +\verb/\begin{zed} ... \end{zed}/, except that the contents are ignored by the +type-checker. Here is an example: +\begin{demo} +\begin{verbatim} +\[ + \exists PhoneDB @ \\ +\t1 known = \empty +\] +\end{verbatim} +\gives +\[ + \exists PhoneDB @ \\ +\t1 known = \empty +\] +\end{demo} +These commands generalize the standard \LaTeX\ commands with the same +name, because the displayed material can be several lines. Note, +however, that the contents are set as text style rather than display +style mathematics. + +A schema box with no name is generated by the % +\verb/schema*/ +environment: +\begin{demo} +\begin{verbatim} +\begin{schema*} + x, y: \nat +\where + x > y +\end{schema*} +\end{verbatim} +\gives +\begin{schema*} + x, y: \nat +\where + x > y +\end{schema*} +\end{demo} +This form is often useful for showing the result of expanding a +complex schema-expression. + +Another kind of mathematical display is provided by the % +\verb/argue/ +environment. This is like the % +\verb/zed/ environment, but the +separation between lines is increased a little, and page breaks may +occur between lines. The intended use is for arguments like this: +\begin{demo} +\begin{verbatim} +\begin{argue} + S \dres (T \dres R) \\ +\t1 = \id S \comp \id T \comp R \\ +\t1 = \id (S \cap T) \comp R & law about $\id$ \\ +\t1 = (S \cap T) \dres R. +\end{argue} +\end{verbatim} +\gives +\begin{argue} + S \dres (T \dres R) \\ +\t1 = \id S \comp \id T \comp R \\ +\t1 = \id (S \cap T) \comp R & law about $\id$ \\ +\t1 = (S \cap T) \dres R. +\end{argue} +\end{demo} +When the left-hand side is long, I find this style better than the +\LaTeX\ % +\verb/eqnarray/ style, which wastes a lot of space. The second +field on each line is optional. Again, the % +\verb/argue/ environment is +ignored by the type-checker. + +Finally, there is the % +\verb/infrule/ environment, used for inference +rules: +\begin{demo} +\begin{verbatim} +\begin{infrule} + \Gamma \shows P +\derive[x \notin freevars(\Gamma)] + \Gamma \shows \forall x @ P +\end{infrule} +\end{verbatim} +\gives +\begin{infrule} + \Gamma \shows P +\derive[x \notin freevars(\Gamma)] + \Gamma \shows \forall x \spot P +\end{infrule} +\end{demo} +The horizontal line is generated by % +\verb/\derive/; the optional +argument is a side-condition of the rule. + +\section{Style parameters} + +A few style parameters affect the way Z text is set out; they can be +changed at any time if your taste doesn't match mine. + +\begin{description} +\item[\tt\string\zedindent] The indentation for mathematical text. + By default, this is the same as % +\verb|\leftmargini|, the indentation + used for list environments. +\item[\tt\string\zedleftsep] The space between the vertical line on the left + of schemas, etc., and the maths inside. The default is 1em. +\item[\tt\string\zedtab] The unit of indentation used by % +\verb|\t|. The default + is 2em. +\item[\tt\string\zedbar] The length of the horizontal bar in the middle of a + schema. The default is 6em. +\item[\tt\string\zedskip] The vertical space inserted by + % +\verb/\also/. By default, this is the same as that inserted by + % +\verb/\medskip/. +\end{description} + +\newpage +\section{The fuzz package} + +The \fuzz\ package consists of two parts -- a style option compatible +with the {\tt zed} style option described here, and an analysis and +checking program. Using \fuzz\ together with \LaTeX, you can: +\begin{itemize} +\item Input Z specifications as ordinary ASCII files. +\item Process them for laser printing or photo-typesetting. +\item Check them for conformance with the Z language rules. +\item Produce a listing showing the schemas in the specification with + components and their types. +\end{itemize} +The \fuzz\ analysis program works on the same ASCII file as \LaTeX; it +extracts the formal text and checks it for conformance with the rules +of the Z language, producing clear error messages. Analysis of a +1300-line specification takes about 7 seconds on a SUN 3/75. + +The \fuzz\ distribution contains the \LaTeX\ style option, a special +font of Z symbols, object code for the analysis program, a library +containing the standard mathematical tool-kit, and some example +specifications. To use \fuzz, you will need to have \LaTeX\ installed +on your machine, but everything else you need is included. \fuzz\ is +currently available under `no-nonsense' licence conditions for the IBM +PC and other DOS machines, and for the SUN 3 and SUN 4 under SUN UNIX. +The PC version can also be used on the PS/2. We are willing to +produce versions for other machines according to demand. + +\newpage +\thispagestyle{empty} +\section*{Ordering information} + +You can order the \fuzz\ package either by cutting out the coupon +below and sending it with your payment, or by sending an official +order -- we will send an invoice. Please send all orders to the +address below. Technical enquiries can be sent to Mike Spivey at the +same address, or by E-mail to {\tt mike@uk.ac.oxford.prg} . + +\vfill +{\center\large\bf \Fuzz\ package: order form\par} +\bigskip +\noindent To: Mrs.\ A. Spivey, 34, Westlands Grove, Stockton Lane, +\hfil\break\hphantom{To: }York, YO3 0EF, England. +\par\bigskip +\newdimen\x \setbox0=\hbox{Telephone:} \x=\wd0 +\begingroup +\baselineskip=24pt +\def\addrline#1{\hbox to\linewidth{\hbox to\x{#1\hfil}\qquad\hrulefill}} +\addrline{Name:} +\addrline{Address:} +\addrline{} +\addrline{} +\addrline{Telephone:} +\endgroup +\bigskip +\noindent Please send [\qquad] copies of the \fuzz\ package for the +following machines: +\par\bigskip +\halign{\hskip\x\qquad#\hfil\qquad&#\qquad\hfil&#\hfil\cr + [\quad]& SUN 3 version: Cartridge tape& \pounds 300\cr + \noalign{\medskip} + [\quad]& SUN 4 version: 3.5in disk& \pounds 275\cr + \noalign{\medskip} + [\quad]& SUN 4 version: Cartridge tape& \pounds 300\cr + \noalign{\medskip} + [\quad]& IBM PC version: 5.25in disk& \pounds 200\cr + \noalign{\medskip} + [\quad]& IBM PC version: 3.5in disk& \pounds 200\cr} +\bigskip +\noindent I enclose a cheque for \pounds [\qquad], payable to +Dr.\ J. M.~Spivey. +\par\bigskip\noindent +Signed: +\par\bigskip +\end{document} -- cgit v1.2.3