diff options
Diffstat (limited to 'Master/texmf-dist/doc/latex/zed-csp/zed2e.tex')
| -rw-r--r-- | Master/texmf-dist/doc/latex/zed-csp/zed2e.tex | 774 |
1 files changed, 774 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/zed-csp/zed2e.tex b/Master/texmf-dist/doc/latex/zed-csp/zed2e.tex new file mode 100644 index 00000000000..ae6a4d41e63 --- /dev/null +++ b/Master/texmf-dist/doc/latex/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} |