summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/zed-csp/zed2e.tex
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/zed-csp/zed2e.tex')
-rw-r--r--macros/latex/contrib/zed-csp/zed2e.tex774
1 files changed, 774 insertions, 0 deletions
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}