summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2006-07-10 21:24:34 +0000
committerKarl Berry <karl@freefriends.org>2006-07-10 21:24:34 +0000
commitac151dac1f876a711cd50b4127c3c5aa8e837556 (patch)
tree622db4347270a735b6aefdf88f1b6954526665a1 /Master/texmf-dist/doc
parenta9018e6c8e9ffc9fdf4f881ab4726e90c01508d9 (diff)
remove vdm package, since license is unstated, author apparently uncontactable, ancient stuff anyway
git-svn-id: svn://tug.org/texlive/trunk@1808 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc')
-rw-r--r--Master/texmf-dist/doc/latex/vdm/vdm.dvibin68980 -> 0 bytes
-rw-r--r--Master/texmf-dist/doc/latex/vdm/vdm.tex1562
2 files changed, 0 insertions, 1562 deletions
diff --git a/Master/texmf-dist/doc/latex/vdm/vdm.dvi b/Master/texmf-dist/doc/latex/vdm/vdm.dvi
deleted file mode 100644
index 268896fa44e..00000000000
--- a/Master/texmf-dist/doc/latex/vdm/vdm.dvi
+++ /dev/null
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/vdm/vdm.tex b/Master/texmf-dist/doc/latex/vdm/vdm.tex
deleted file mode 100644
index ddce8336f38..00000000000
--- a/Master/texmf-dist/doc/latex/vdm/vdm.tex
+++ /dev/null
@@ -1,1562 +0,0 @@
-%%% ====================================================================
-%%% @LaTeX-file{
-%%% author = "Mario Wolczko",
-%%% version = "3.02",
-%%% date = "14 October 1994",
-%%% filename = "vdm.tex",
-%%% address = "FORMERLY AT
-%%% Dept of Computer Science
-%%% The University of Manchester
-%%% Oxford Road
-%%% Manchester M13 9PL
-%%% UK",
-%%% codetable = "ISO/ASCII",
-%%% keywords = "LaTeX, VDM specification language",
-%%% supported = "yes",
-%%% docstring = "Documentation for vdm.sty
-%%% NOTE
-%%% Mario no longer works at Manchester
-%%% This is a minimal update to LaTeX2e
-%%% By David Carlisle",
-%%% }
-%%% ====================================================================
-\documentclass{article}
-
-\usepackage{latexsym,vdm,verbatim}
-
-
-
-\title{Typesetting BSI VDM with \LaTeX}
-\author{Mario Wolczko\\
-Dept. of Computer Science\\
-The University\\
-Manchester M13 9PL\\
-U.K.\\
-\texttt{mario@cs.man.ac.uk}, {\tt ...!uknet!man.cs!mario}}
-\date{09 June 1992 \\
-Version 3.01}
-
-\newcommand{\Vdm}{{\tt vdm\/}}
-
-\newenvironment{dangerous}{\par\vspace{5pt}\bgroup\small\noindent}%
- {\par\egroup\vspace{5pt}}
-
-\newlength{\righthalf} \setlength{\righthalf}{0.5\textwidth}
-\newlength{\lefthalf} \setlength{\lefthalf}{0.4\textwidth}
-
-\newenvironment{leftside}{\noindent\hspace{0.1\textwidth}%
- \minipage[t]{\lefthalf}\vspace{10pt}%
- \noindent\begin{vdm}\leftskip=0pt\VDMindent=0pt}%
- {\end{vdm}\endminipage}
-\newenvironment{rightside}{\minipage[t]{\righthalf}\verbatim}%
- {\endverbatim\endminipage}
-
-
-\renewcommand{\^}[1]{$\langle${\rm #1\/}$\rangle$}
-
-\newcommand{\mmexp}{\^{math-mode-expression}}
-\newcommand{\cs}[1]{\leavevmode\hbox{\tt \string#1}}
-
-\setlength{\VDMindent}{3\parindent}
-
-\setlength{\preOperationSkip}{0pt}
-\setlength{\preFunctionSkip}{0pt}
-\setlength{\preTypeSkip}{0pt}
-\setlength{\preCompositeSkip}{0pt}
-\setlength{\preRecordSkip}{0pt}
-\setlength{\preFormulaSkip}{0pt}
-
-\begin{document}
-
-\maketitle
-
-\tableofcontents
-
-\section{Overview}
-
-This document describes a style option, \Vdm, for use with
-\LaTeX. The purpose of \Vdm\ is to make the typesetting of VDM
-specifications easy. Other goals are:
-\begin{itemize}
-\item To enable users of \Vdm\ to communicate their specifications
- to others, possibly in a variety of concrete syntaxes, without
- having to change their source files
-\item To enable a user of \Vdm\ to concentrate on his%
- \footnote{Read `his/her' for every occurence of `his'.}
- specifications, and ignore the detailed layout as much as
- possible. A side effect of this is that the effort required
- to improve layout is concentrated in one place, within the
- \Vdm\ macros.
-\end{itemize}
-(This version of the \Vdm\ style option uses the {\sc bsi} concrete
-syntax. Any document prepared using earlier versions is still
-accepted, but the way it is typeset will match more closely the {\sc
-bsi} standard concrete syntax. There are also a few additional
-commands (summarised at the end). Note that this is {\em not\/} a
-complete style file for all of {\sc bsi vdm}.)
-
-But enough evangelising. Let's get to the the real meat. This
-document is broken up into the following sections:
-\begin{itemize}
-\item General points about using \Vdm
-\item Typesetting formulas
-\item How to typeset data types
-\item How to typeset functions
-\item How to typeset operations
-\item How to typeset proofs
-\item How to tailor/extend the system for your own
- application.
-\end{itemize}
-You should definitely read the first two sections---then you'll know
-roughly what you're in for, and whether you want to continue. The
-remaining sections can be read as and when you need them.
-
-\begin{dangerous}
-In keeping with the best traditions of \TeX\ documentation, paragraphs
-that contain material that is not essential for novices, but vital if
-you want to parameterise or extend the system, are in smaller type,
-like this one.
-\end{dangerous}
-
-Just to give a preliminary example, here is some output from \Vdm, and
-the corresponding input:
-
-\begin{vdm}
-\begin{fn}{dec}{ptrs,om} \\
-\signature{
- \setof{Oop} \x \mapof{Oop}{Object} \to \mapof{Oop}{Object}
-}
-\If ptrs = \emptyset
-\Then om
-\Else \Let gone = \set{p \in ptrs | RC(om(p)) = 1} \In
- \Let om' = gone \dsub om \In
- \Let om'' = om' \owr
- \map{p \mapsto \chg{om'(p)}{RC}{RC\minus 1}\R
- | p \in ptrs \diff gone} \In
- dec(\Union\set{\elems{BODY(om(p))} | p \in gone}, om'')
-\Fi
-\end{fn}
-
-\begin{op}[DESTROYPTR]\label{op-ex}
-\args{ Obj, Ptr : Oop }
-\ext{ \Wr OM : \mapof{Oop}{Basic_Object} }
-\pre{ ptr \in \elems{BODY(om(obj))} }
-\post{ om = ~{om} \owr \map{ obj \mapsto
- \chg{om(obj)}{BODY}{BODY \diff \set{ptr}}}}
-\end{op}
-\end{vdm}
-
-% this is verbatim input
-\begin{verbatim}
-\begin{vdm}
-\begin{fn}{dec}{ptrs,om} \\
-\signature{
- \setof{Oop} \x \mapof{Oop}{Object} \to \mapof{Oop}{Object}
-}
-\If ptrs = \emptyset
-\Then om
-\Else \Let gone = \set{p \in ptrs | RC(om(p)) = 1} \In
- \Let om' = gone \dsub om \In
- \Let om'' = om' \owr
- \map{p \mapsto \chg{om'(p)}{RC}{RC\minus 1}
- | p \in ptrs \diff gone} \In
- dec(\Union\set{\elems{BODY(om(p))} | p \in gone}, om'')
-\Fi
-\end{fn}
-
-\begin{op}[DESTROYPTR]
-\args{ Obj, Ptr : Oop }
-\ext{ \Wr OM : \mapof{Oop}{Basic_Object} }
-\pre{ ptr \in \elems{BODY(om(obj))} }
-\post{ om = ~{om} \owr \map{ obj \mapsto
- \chg{om(obj)}{BODY}{BODY \diff \set{ptr}}}}
-\end{op}
-\end{vdm}
-
-\end{verbatim}
-
-
-
-\section{Using \Vdm---General Points}
-
-To get at \Vdm, include {\tt vdm\/} as a document style option, e.g.:
-\begin{verbatim}
- \documentstyle[12pt,vdm]{report}
-\end{verbatim}
-\begin{dangerous}
-To the best of my knowledge, the use of \Vdm\ does not conflict with
-any of the other document styles, except when something has been
-redefined. An attempt will be made to document all such redefinitions.
-\end{dangerous}
-Once \Vdm\ has been included, you can then use the {\tt vdm\/}
-environment. For example,
-\begin{verbatim}
- \begin{vdm}
- ....
- \end{vdm}
-\end{verbatim}
-All specification material should be placed within the {\tt vdm\/}
-environment. The use of \Vdm\ only affects text within the {\tt vdm\/}
-environment, except for the following global changes (which are only
-relevant when in math or display math mode):
-
-
-\begin{enumerate}
-\item The mathcodes of a\dots z and A\dots Z have been changed. In
- plain English, this means that when you type letters in math
- mode the inter-letter spacing may be different than it would be
- had you not included \Vdm\ as an option.\footnote{This is not
- the case if you are using PS\LaTeX, as that does not
- distinguish text italic from math italic.} This is because
- \LaTeX\ math mode is usually tuned for single letter
- identifiers, as used by mathematicians for millenia. However,
- you and I both know that most meaningful identifiers have more
- than one letter in them, so \Vdm\ provides better spacing for
- them. As an example, if you type \verb;$identifier$;, \LaTeX\
- would normally print {\defaultMathcodes$identifier$}, whereas
- the use of \Vdm\ will yield $identifier$.
- \begin{dangerous}If you really want to use the
- `normal' inter-letter spacing, say \cs\defaultMathcodes.
- \end{dangerous}
-\item Underscore gives you an underscore, and not a subscript. If
- you want a subscript use \verb;@;, e.g.,~$x@0$ is typed
- \verb;x@0;, or use \TeX's \cs\sb\ macro. An \verb;@; is still an
- @ when not in math mode. Occasionally you may find that an @
- in math mode {\em doesn't\/} give you a subscript
- (particularly when used with moving arguments). Should
- this happen, you are advised to use \TeX's \cs\sb\ macro,
- e.g.,~\verb;$x\sb{0}$;.
- \begin{dangerous}
- If you don't use
- underscores much, and you want to use \verb;_; for subscripts,
- you can say \cs\underscoreon\ (and \cs\underscoreoff\ to
- make it revert to its usual meaning in \Vdm).
- \end{dangerous}
-\item \verb;-; typesets a hyphen, and not a minus sign. VDM specifications
- usually contain a lot more
- \begin{vdm}$long-identifiers$\end{vdm}\
- than subtractions, so
- on the whole this alteration should save effort.
- If you really want
- to do a single subtraction sign, use \cs\minus.
- If you find the default is inappropriate, you can revert to
- the original behaviour using \cs\mathminus; \cs\textminus\ is
- the inverse. Example: \verb;a-b \ne\mathminus a-b; gives
- \begin{vdm}$a-b \ne\mathminus a-b$\end{vdm}.
-\item \verb;|; gives you a \begin{vdm}$|$\end{vdm}, and not a $\vert$.
- Do you see the difference? No? The former goes between things,
- e.g., \begin{vdm}$\set{x|p(x)}$\end{vdm}, while the latter is
- a delimiter, e.g.,~$\vert x\vert$.
- In VDM, most people use the former more than the latter, so again this
- seems reasonable.
- If you really want a $\vert$ (the second kind),
- say \cs\vert.
-\item In \TeX\ and \LaTeX\ \verb;~; has always been a tie (a space
- between words at which the line is never broken). Well
- in \Vdm\ it isn't. \verb;~x; will give you a
- \begin{vdm}$~x$\end{vdm}. For long identifiers, such as
- \begin{vdm}$~{long}$\end{vdm}, say
- \verb;~{long};.
- {\em Note that this only applies in math
- mode; elsewhere a \verb;~; is still a tie.}
-\item In math mode, the double quote character \verb;''; is actually
- a macro. Placing text between pairs of double quotes causes
- that text to be set in the normal text font. For example,
- \verb;$x="a variable"$; gives you $x="a variable"$.
- \begin{dangerous}
- \indent If you want to change the font used for text placed between
- quotes, redefine the command \cs\mathTextFont. By default
- it is defined to be \cs\rm\ (\cs\mathrm\ for the New Font
- Selection Scheme).
- \end{dangerous}
-\item The following macros have been altered in a non-trivial way:
- \cs\forall, \cs\exists\ (see later).
-\end{enumerate}
-
-\begin{dangerous}
-When you typeset some VDM within the {\tt vdm\/} environment, by
-default it is set in from the left margin by an amount equal to
-\cs\parindent, the indentation at the beginning of each paragraph.
-If you want to change this, change the value of \cs\VDMindent, e.g.:
-\begin{verbatim}
- \setlength{\VDMindent}{0cm}
-\end{verbatim}
-will make your specs come out flush left. This document has been
-typeset with \cs\VDMindent\ equal to $3\times \cs\parindent$.
-
-Similarly, the right hand margin is controlled by a parameter called
-\cs\VDMrindent. By default it is also set to \cs\parindent.
-\end{dangerous}
-
-\begin{dangerous}
-You can have a particular line spacing in force within the
-{\tt vdm} environment.
-The spacing within a {\tt vdm} environment is dictated by the
-\cs\VDMbaselineskip\ command. Note that this is {\em not\/} a
-length, but a command. By default it expands to \cs\baselineskip\
-so that the line spacing is that of the surrounding text, whatever
-size that may be. To make it smaller, you may want to say
-\begin{verbatim}
- \renewcommand{\VDMbaselineskip}{0.8\baselineskip}
-\end{verbatim}
-for example.
-\end{dangerous}
-
-
-\section{Typesetting formulas}
-
-Most of the text you enter within {\tt vdm\/} environments will be in
-\TeX's math mode, but VDM does its best to conceal this fact from you,
-so that you should rarely, if ever, have to type a dollar sign.
-However, several new features have been provided for the typesetting
-of logical formulas. Firstly, operators with sensible names have been
-provided: use \cs\Iff, \cs\Implies, \cs\Or, \cs\And\
-and \cs\Not\ for the operators~\begin{vdm}%
-$\Leftrightarrow,\Rightarrow,\Or,\And$ and $\Not$\end{vdm}.
-(To retain compatibility with a previous version, \cs\iff,
-\cs\implies, \cs\and\ and \cs\neg\ are still provided, but
-\cs\or\ is not.)
-
-A major change has come in the area of quantified expressions. In
-VDM, they
-have very well-defined forms, so the \LaTeX\ sequences \cs\forall\
-and \cs\exists\ have been re-defined to take arguments. For
-example, to get
-\begin{vdm}
-\begin{formula}
-\exists{x \in S}{p(x)}
-\end{formula}
-\end{vdm}
-\noindent type
-\begin{verbatim}
- \exists{x \in S}{p(x)}
-\end{verbatim}
-Note the separating dot that was put in auto\-matically. If you want
-one of these dots by itself, you can have one by saying
-\cs\suchthat.
-
-In addition, two new quantifiers, \cs\unique\ and \cs\nexists, have
-been added:
-
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\unique{x \in S}{p(x)}
-\end{formula}
-\begin{formula}
-\nexists{x \in S}{p(x)}
-\end{formula}
-\end{leftside}\begin{rightside}
-\unique{x \in S}{p(x)}
-\nexists{x \in S}{p(x)}
-\end{rightside}
-\end{minipage}
-
-Additionally, to complement \cs\unique, there is \cs\uniqueval. This
-is the so-called ``iota-function'' that returns the unique value, if
-there is one:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\uniqueval{x \in S}{p(x)}
-\end{formula}
-\end{leftside}\begin{rightside}
-\uniqueval{x \in S}{p(x)}
-\end{rightside}
-\end{minipage}
-
-
-\begin{dangerous}
-If you want to use the old versions of \cs\forall\ and
-\cs\exists\ they are available under the pseudonyms of
-\cs\Forall\ and \cs\Exists.
-\end{dangerous}
-
-If you find that the body of the quantified expression is too long to
-fit comfortably on a line, there are *-forms of the above commands
-that place the body of the quantified expression on a new line,
-slightly indented. For example,
-
-\begin{vdm}
-\begin{formula}
-\exists*{x \in S}{
- p(x) \And q(x) \Or \Not p(x) \Implies r(x) \And S(x)}
-\end{formula}
-\end{vdm}
-
-\noindent can be obtained with
-\begin{verbatim}
- \exists*{x \in S}{p(x) \And q(x) \Or \Not p(x)
- \Implies r(x) \And S(x)}
-\end{verbatim}
-
-If you need ``Strachey'' brackets, e.g., $M\term{e}$, place the
-material to appear within the brackets within \verb;\term{ ... };,
-thus: \verb;$M\term{e}$;.
-
-A special control sequence, \cs\const, is available for constants.
-To get, for example, $\const{Yes}|\const{No}$, type
-\verb;\const{Yes}|\const{No};.
-\begin{dangerous}
-If you don't like the font that constants are set in, you can change
-them by redefining the command \cs\constantFont. By
-default it expands to \cs\sc.
-\end{dangerous}
-
-\subsection{The {\tt formula} Environment}
-
-Occasionally you may want a formula on its own, between paragraphs of
-text, say. Normally, the provided environments and commands suffice,
-but sometimes they don't. If you need an odd equation to stand on its
-own, use the {\tt formula} environment:
-\begin{verbatim}
- \begin{formula}
- x = 10
- \Or \forall{i \in \Nat}{i \ne 10 \Implies i \ne x}
- \end{formula}
-\end{verbatim}
-\sloppy
-The {\tt formula} environment is similar to displayed math mode,
-except: formulas are indented by \cs\VDMindent, not
-\cs\mathindent, and line breaks can be made using \cs\\.
-Also, within the {\tt formula} environment everything appears flush
-left, as opposed to being centred.
-
-\subsection{Constructions}
-
-A particularly nice feature of \Vdm\ is that you can typeset multi-line
-constructions such as those in the earlier example without having to
-worry about, say, lining up ``thens'' and ``elses'' with ``ifs''.
-In the following definitions, whenever you see the term \mmexp, you
-should type an expression as if in math mode, but you needn't put
-dollar signs in. All of the constructions described below can be used
-where a \mmexp\ is required. Each construction is shown by example;
-the output on the left results from the input on the right.
-Also note that each macro name begins with an upper-case letter.
-\TeX\ and \LaTeX\ frequently use the lower-case variants for
-completely unrelated things. Naturally, chaos will ensue if you mix
-the names up.
-
-Typesetting an \kw{if} is done using \cs\If\ \mmexp \cs\Then\ \mmexp
-\cs\Else\ \mmexp \cs\Fi.
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \If x\in S
- \Then S \diff x
- \Else \emptyset
- \Fi
- \end{formula}
-\end{leftside}%
-\begin{rightside}
-\If x\in S
-\Then S \diff x
-\Else \emptyset
-\Fi
-\end{verbatim}
-\end{rightside}
-\end{minipage}
-
-If you nest \cs\If{}s then you must enclose inner \cs\If{}s within
-braces:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \If \ldots
- \Then{
- \If \ldots
- \Then \ldots
- \Else \ldots
- \Fi
- }\Else
- \Fi
- \end{formula}
-\end{leftside}\begin{rightside}
-\If ...
-\Then{
- \If ...
- \Then ...
- \Else ...
- \Fi
-}\Else
-\Fi
-\end{rightside}
-\end{minipage}
-
-You are advised to place the extra braces exactly as above; don't let
-extraneous spaces intervene between the keywords and the braces.
-
-The \cs\If\ macro always starts a new line for the \kw{then} and
-\kw{else} parts. If you want \TeX\ to try to choose line breaks, use
-\cs\SIf\ instead:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \SIf a=b
- \Then c=d+e
- \Else p=q+r+s+t+u
- \Fi
- \end{formula}
-\end{leftside}%
-\begin{rightside}
-\SIf a=b
-\Then c=d+e
-\Else p=q+r+s+t+u
-\Fi
-\end{rightside}
-\end{minipage}
-
-\mbox{\kw{let}\dots\kw{in}} constructions are done in a similar way:
-\cs\Let{} \mmexp{} \cs\In{} \mmexp, and \cs\SLet{} \mmexp{}
-\cs\In{} \mmexp.
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \Let x=f(y,z) \In
- g(x)+h(x)
- \end{formula}
-\end{leftside}%
-\begin{rightside}
-\Let x=f(y,z) \In
-g(x)+h(x)
-\end{rightside}
-\end{minipage}
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \SLet x=f(y,z) \In{x^2}
- \end{formula}
-\end{leftside}%
-\begin{rightside}
-\SLet x=f(y,z) \In{x^2}
-\end{rightside}
-\end{minipage}
-
-Notice that \cs\SLet\ takes a second argument, which is part of the
-same `paragraph', where \cs\Let\ does not.
-
-The typesetting of a \kw{cases} clause is more complicated. It takes
-the form:
-\begin{verse}
-\verb;\Cases{; \mmexp \verb;}; \\
-from-\mmexp \verb;&; to-\mmexp \cs\\ \\
-from-\mmexp \verb;&; to-\mmexp \cs\\ \\
-\dots \\
-\verb;\Otherwise{; \mmexp \verb;}; \\
-\verb;\Endcases;
-\end{verse}
-
-The \cs\Otherwise\ field is optional. This construction follows a
-general pattern that is common in \Vdm\ input: lists of things are
-separated by \cs\\s, and subfields are separated by \verb;&;s or
-\verb;:;s.
-\begin{dangerous}
-In reality, there is another, optional argument, after the
-\cs\Endcases. If you were to try typesetting something like
-\begin{verbatim}
- (... var = \Cases ...
- \Endcases)
-\end{verbatim}
-you'd find the closing right parenthesis in an unexpected place (on
-the same line as the $=$, in fact). To get text to the right of the
-\cs\Endcases\ you can place an optional argument within brackets
-after it:
-\begin{verbatim}
- (... var = \Cases ...
- \Endcases[)]
-\end{verbatim}
-Admittedly, this looks a little strange, but it does work.
-\end{dangerous}
-
-Here is an example of \cs\Cases\ in action:
-
-\begin{formula}
- \Cases{ select(x) }
- \nil & \emptyset \\
- mk-Lst(hd,tl) & \set{hd} \union \elems{tl}
- \Otherwise{ x }
- \Endcases
-\end{formula}
-
-\begin{verbatim}
- \Cases{ select(x) }
- \nil & \emptyset \\
- mk-Lst(hd,tl) & \set{hd} \union \elems{tl}
- \Otherwise{ x }
- \Endcases
-\end{verbatim}
-
-Note the \cs\\ is a {\em separator\/} and not a {\em
-terminator\/}---you don't need one after the last item. Also, the
-\cs\Otherwise\ can appear anywhere between the \verb;\Cases{}; and the
-\cs\Endcases, but it will always be typeset last.
-\begin{dangerous}
-Some people prefer the selectors to appear lined up on the left, some
-on the right. If you want them to appear on the left, say
-\cs\leftCases; if you want them on the right, say
-\cs\rightCases. The scope of the \cs\leftCases\ and
-\cs\rightCases\ commands is the current group. By default, you
-get \cs\rightCases.
-\end{dangerous}
-
-\subsubsection{The {\tt formbox} Environment}
-
-Occasionally you might find that you want to put a line break in a
-place that can't handle \cs\\. For example, if you have a \cs\Cases\
-command and the rhs of a particular case is too big, you can't use
-\cs\\ to break the line directly, as it will be interpreted as the
-separator between cases. Then you must the {\tt formbox} environment.
-It is similar to the {\tt formula} environment in that you can put all
-sorts of things in it, but it can be used within other constructions,
-unlike the {\tt formula} environment, which can only be used at the
-outermost level.
-
-This example should convey the general idea:
-\begin{verbatim}
- \Cases{ f(x) }
- mk-Very_long_constructor(foo,bar) &
- {\begin{formbox}
- long_predicate_with(foo) \\
- \And long_predicate_with(bar)
- \end{formbox}}
- ...
-\end{verbatim}
-\begin{vdm}
-\begin{formula}
- \Cases{ f(x) }
- mk-Very_long_constructor(foo,bar) &
- {\begin{formbox}
- long_predicate_with(foo) \\
- \And long_predicate_with(bar)
- \end{formbox}}\\
- \ldots
- \Endcases
-\end{formula}
-\end{vdm}
-Note the extras braces around the {\tt formbox}; these are required to
-``hide'' the \cs\\ from the \cs\Cases.
-
-\subsection{Other General Points about Formulas}
-
-\cs\\ will%
-\footnote{For `will' read `should'.}
-{\em always\/}
-start a new line. Sometimes this is done in addition to some other
-function (as in the \cs\Cases\ macro, where it delimits a
-particular case), but you should be able to use \cs\\ almost
-anywhere to force a line break. Indeed, sooner or later you'll want
-to typeset a long formula and \TeX\ will not be able to break the line
-sensibly, or will choose an unpleasant break. In this case you'll
-have to use \cs\\.
-
-Frequently you need to indent things within multi-line formulas. To
-help you do this, a command is provided which breaks a line, and
-indents the next line by an amount which you can supply (in units of
-{\tt ems}). The \cs\T\ command takes a single argument that controls
-how much the next line will be indented:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-a \And b \T2
-\Implies b \And a \T1
-\Or d \And e
-\end{formula}
-\end{leftside}\begin{rightside}
-a \And b \T2
-\Implies b \And a \T1
-\Or d \And e
-\end{rightside}
-\end{minipage}
-
-Along similar lines is the \cs\R\ command. This does a line break,
-like \cs\\, but then pushes the formula on the next line as far to the
-right as it can:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-(a \And b \Implies b \And a) \R
-\Or d \And e
-\end{formula}
-\end{leftside}\begin{rightside}
-(a \And b \Implies b \And a) \R
-\Or d \And e
-\end{rightside}
-\end{minipage}
-
-Beware: it may end up pushing it further to the right than you
-expected! This is {\sc A Bug}, and {\sc Will Not Be Fixed}, so you'll
-have to work around it.
-
-The \cs\If, \cs\Let, etc., constructions are all unusual in
-that it's impossible to typeset something sensibly to the right of
-them. For example, if you try
-\begin{verbatim}
- \exists{x \in S}{
- \If x=0 \Then S=Q \Else S=P \Fi}
- \Or S=\emptyset
-\end{verbatim}
-then you'll get
-
-\begin{vdm}
- \begin{formula}
- \exists{x \in S}{\If x=0 \Then S=Q \Else S=P \Fi} \Or S=\emptyset
- \end{formula}
-\end{vdm}
-
-\noindent which is unlikely to be what you wanted.
-
-You should also remember that where \Vdm\ wants a \mmexp, \TeX\ will
-be placed in math mode. This is usually the right thing to do, but
-occasionally you might want a natural language comment to appear
-there.
-In this case you'll have to insert an \cs\mbox\ or a \cs\parbox\
-depending on whether your comment might span one or more lines:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \If \mbox{the condition is true}
- \Then \mbox{do the true part}
- \Else "do the false part"
- \Fi
- \end{formula}
-\end{leftside}\begin{rightside}
-\If \mbox{the condition is true}
-\Then \mbox{do the true part}
-\Else "do the false part"
-\Fi
-\end{rightside}
-\end{minipage}
-The else-part illustrates how quotes can be used an an abbreviation
-for \verb;\mbox{...}; within math mode.
-
-Finally, all the constructions above will not break at a page
-boundary. This means that you're in big trouble if you want to
-typeset a three-page \cs\Cases. The only statement I can make to
-mitigate this is: you shouldn't have expressions that complicated in
-the first place---who do you expect to read them? Remember: ``truth
-is beauty'', so if your formulas are not beautiful, then chances are
-they're not true either.
-
-
-
-
-
-\section{Typesetting data types}
-
-The following table lists the primitive types and values available:
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-$\set{0,1,\dots}$ & $\Nat$ & \cs\Nat \\
-$\set{1,2,\dots}$ & $\Natone$ & \cs\Natone,\cs\Nati \\
-$\set{\dots,\minus1,0,1,\dots}$& $\Int$ & \cs\Int \\
-Rationals & $\Rat$ & \cs\Rat \\
-Real numbers & $\Real$ & \cs\Real \\
-$\set{\true,\false}$ & $\Bool$ & \cs\Bool \\
-Truth & $\true$ & \cs\true,\cs\True \\
-Falsehood & $\false$ & \cs\false,\cs\False\\
-Nil & $\nil$ & \cs\nil \\
-\hline
-\end{tabular}
-\end{center}
-
-If you need a new keyword, you can create one easily. For example, if
-your favourite brand of logic has ``maybe'' as a value, you can say
-\begin{verbatim}
- \makeNewKeyword{\maybe}{maybe}
-\end{verbatim}
-and henceforth \cs\maybe\ is a valid control sequence that produces
-the text \kw{maybe}. The text of the second argument to
-\cs\makeNewKeyword\ can be anything; it doesn't have to match your
-control sequence name.
-\begin{dangerous}
-If you don't like the font that keywords are set in, you can change
-it by redefining the command \cs\keywordFontBeginSequence. By
-default it expands to \cs\sf.
-\end{dangerous}
-
-The following type-related commands are provided:
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-Output & Input & \\
-\hline
-$\setof{x}$ & \verb;\setof{x}; & set type constructor \\
-$\set{a,b,c}$ & \verb;\set{a,b,c}; & set enumeration \\
-$\emptyset$ & \cs\emptyset & the empty set \\
-$\seqof{x}$ & \verb;\seqof{x}; & seq. type constructor\\
-$\seq{a,b,a,c}$ & \verb;\seq{a,b,a,c}; & seq. enumeration\\
-$\emptyseq$ & \cs\emptyseq & the empty sequence \\
-$\mapof{x}{y}$ & \verb;\mapof{x}{y}; & map type constructor \\
-$\mapinto{x}{y}$& \verb;\mapinto{x}{y}; & one-one map type \\
-$\map{p\mapsto x}$
- & \verb;\map{p\mapsto x}; & map enumeration\\
-$\emptymap$ & \cs\emptymap & the empty map \\
-\hline
-\end{tabular}
-\end{center}
-
-\noindent Here are the relevant operators:
-
-\begin{center}\small
-\begin{tabular}{llllll}
-$\in$ & \cs\in &
- $\owr$ & \cs\owr &
- $\sconc$ & \cs\sconc \\
-$\notin$ & \cs\notin &
- $\dres$ & \cs\dres &
- $\len{l}$ & \verb;\len{l};\\
-$\subset$ & \cs\subset&
- $\rres$ & \cs\rres &
- $\hd{l}$ & \verb;\hd{l}; \\
-$\subseteq$ & \cs\subseteq&
- $\dsub$ & \cs\dsub &
- $\tl{l}$ & \verb;\tl{l}; \\
-$\inter$ & \cs\inter,\cs\intersection;&
- $\rsub$ & \cs\rsub &
- $\elems{l}$ & \verb;\elems{l};\\
-$\Inter$ & \cs\Inter,\cs\Intersection;&
- $\dom{m}$&\verb;\dom{m};&
- $\inds{l}$ & \verb;\inds{l};\\
-$\union$ & \cs\union &
- $\rng{m}$&\verb;\rng{m};&
- $\Conc{l}$ & \verb;\Conc{l};\\
-$\Union$ & \cs\Union &
- $\Min{s}$& \verb;\Min{s};&
- $\cons{h,t}$ & \verb;\cons{h,t};\\
-$\diff$ & \cs\diff,\cs\difference;&
- $\Max{s}$& \verb;\Max{s};&
- & \\
-$\card{s}$ & \verb;\card{s};&
- & &
- &
-\end{tabular}
-\end{center}
-
-\begin{dangerous}
-If you invent a new monadic keyword operator (like \dom{}, etc.),
-then you can have \Vdm\ define for you a control sequence which
-switches font, and puts the right spacing in. For example,
-\begin{verbatim}
- \newMonadicOperator{\inv}{inv}
-\end{verbatim}
-will define the \cs\inv\ control sequence to print
-{\keywordFontBeginSequence inv\/}. Henceforth you can say, e.g.,
-\verb;\inv{Foo};. All such sequences take one argument (they are
-monadic, after all).
-\end{dangerous}
-
-You can define a new type using
-\verb;\type{;type-name\verb;}{;type\verb;};:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \type{Complex}{\Real\x \Real}
-\end{leftside}%
-\begin{rightside}
-\type{Complex}{\Real\x \Real}
-\end{rightside}
-\end{minipage}
-
-Composites types can be typeset using the {\tt composite} environment:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{composite}{Datec}
- day:\set{1,\ldots,366}, \\
- year:\set{1583,\ldots,2599}
- \end{composite}
-\end{leftside}%
-\begin{rightside}
-\begin{composite}{Datec}
- day :\set{1,\ldots,366}, \\
- year:\set{1583,\ldots,2599}
-\end{composite}
-\end{rightside}
-\end{minipage}
-
-There is also a {\tt composite*} environment (and an equivalent
-\cs\scompose\ control sequence) that places the entire composite
-type on a single line:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{composite*}{Celsius}
- \Real
- \end{composite*}
-\end{leftside}%
-\begin{rightside}
-\begin{composite*}{Celsius}
- \Real
-\end{composite*}
-\end{rightside}
-\end{minipage}
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \scompose{Celsius}{\Real}
-\end{leftside}%
-\begin{rightside}
-\scompose{Celsius}{\Real}
-\end{rightside}
-\end{minipage}
-
-`Records' can be defined using the {\tt record\/} environment:
-
-\begin{verse}
-\verb;\begin{record}{;record-type-name\verb;}; \\
-field-name \verb;:; field-type \cs\\ \\
-\dots \\
-\verb;\end{record};
-\end{verse}
-The colons are used as sub-field separators.
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{record}{PERSON}
- NM : \seqof{Char} \\
- FEM : \Bool
- \end{record}
-\end{leftside}%
-\begin{rightside}
- \begin{record}{PERSON}
- NM : \seqof{Char} \\
- FEM : \Bool
- \end{record}
-\end{rightside}
-\end{minipage}
-
-If the definition is short, you may prefer to use a short form:
-\begin{verbatim}
- \defrecord{PERSON}{
- NM : \seqof{Char} \\
- FEM : \Bool
- }
-\end{verbatim}
-
-\begin{dangerous}
-Some people prefer the field names to appear lined up on the left, some
-on the right. If you want them to appear on the left, say
-\cs\leftRecord; if you want them on the right, say
-\cs\rightRecord. The scope of the \cs\leftRecord\ and
-\cs\rightRecord\ commands are the current group. By default, you
-get \cs\rightRecord.
-\end{dangerous}
-
-Updating fields of composites using the $\mu$-function can be
-specified using \cs\chg:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \chg{p}{FEM}{\Not man(q)}
- \end{formula}
-\end{leftside}%
-\begin{rightside}
-\chg{p}{FEM}{\Not man(q)}
-\end{rightside}
-\end{minipage}
-
-Notice that the $\mu$, parentheses, comma and $\mapsto$ were inserted
-automatically.
-
-
-
-\section{How to Typeset Functions}
-
-Typesetting $\lambda$-expressions is easy:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \LambdaFn{x,y}{x^2+y^2}
- \end{formula}
-\end{leftside}%
-\begin{rightside}
-\LambdaFn{x,y}{x^2+y^2}
-\end{rightside}
-\end{minipage}
-
-As with \cs\forall, \cs\exists\ and \cs\unique,
-\cs\LamdbaFn\ has a *-form that places the body of the function
-below and to the right:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
- \begin{formula}
- \LambdaFn*{x,y,z}{
- (x^2+y^2+z^2)^{\frac12}}
- \end{formula}
-\end{leftside}%
-\begin{rightside}
-\LambdaFn*{x,y,z}{
- (x^2+y^2+z^2)^{\frac12}}
-\end{rightside}
-\end{minipage}
-
-There is also a {\tt fn\/} (function) environment for defining named
-functions. It has the following structure:
-\begin{verse}
-\verb;\begin{fn}{;name-of-function\verb;}{; argument-list \verb;}; \\
-\verb;\signature{;signature-of-function\verb;}; \\
-\^{optional precondition}\\
-\^{optional postcondition}\\
- body of function (a \mmexp) \\
-\verb;\end{fn};
-\end{verse}
-
-See the third page for an example. The \cs\signature\ is optional
-and can be placed anywhere within the body---it will always be typeset
-before the body. Useful macros within the \cs\signature\ are:
-\cs\x\ and \cs\to, which yield $\x$ and~$\to$. Note that you can also
-enter functions defined implicitly with pre- and post-conditions; see the
-next section on how to enter them.
-
-All of the material in the section on formulas is relevant within the
-body of the function.
-
-\sloppy\sloppy
-If you frequently intersperse your function definitions with text (and you
-should), you can save some typing by using the {\tt vdmfn\/} environment.
-\cs\begin\verb;{vdmfn}; \dots \cs\end\verb;{vdmfn}; is equivalent to
-\cs\begin\verb;{vdm};\cs\begin\verb;{fn}; \dots
-\cs\end\verb;{fn};\cs\end\verb;{vdm};.
-
-The {\tt fn} environment also has a *-form that does not insert
-parentheses around the argument list. For example:
-
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{fn*}{MP}{\term{p}\rho\sigma}
-\ldots
-\end{fn*}
-\end{leftside}\begin{rightside}
-\begin{fn*}{MP}{
- \term{p}\rho\sigma}
-...
-\end{fn*}
-\end{rightside}
-\end{minipage}
-
-If you require the $\DEF$ symbol by itself, then you can get it by
-saying \cs\DEF.
-
-\subsection{Invariants}
-
-To typeset an invariant on a composite object, use the following
-structure:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{record}{D}
- day : Day \\
- year : Year
-\end{record}
-\where
-\begin{fn}{inv-D}{mk-D(d,y)}
- is-leapyr(y) \Or d \le 365
-\end{fn}
-\end{leftside}\begin{rightside}
-\begin{record}{D}
- day : Day \\
- year : Year
-\end{record}
-\where
-\begin{fn}{inv-D}{mk-D(d,y)}
- is-leapyr(y) \Or d \le 365
-\end{fn}
-\end{rightside}
-\end{minipage}
-
-
-\section{How to Typeset Operations}
-
-Operations are typeset within the {\tt op\/} environment.
-The general structure is:
-
-\begin{verse}
-\verb;\begin{op}[;\^{name-of-operation}\verb;]; \\
-\verb;\args{;\^{list-of-arguments}\verb;}; \\
-\verb;\res{;\^{result(s)}\verb;}; \\
-\verb;\ext{;\^{list-of-externals}\verb;}; \\
-\^{pre-condition} \\
-\^{post-condition} \\
-\verb;\end{op};
-\end{verse}
-
-The order of the various parts within the {\tt op} environment is not
-important; they will always be printed in a canonical style (see
-page~\pageref{op-ex} for an example).
-
-Any of \cs\args, \cs\res, \cs\ext, \^{pre-condition} or
-\^{post-condition} may be omitted. \verb;\begin{vdmop}; is an
-abbreviation for \verb;\begin{vdm}\begin{op};; \verb;\end{vdmop}; is an
-abbreviation for \verb;\end{op}\end{vdm};.
-
-The \^{name-of-operation} can be any one-line expression; it is
-typeset in math mode. An alternative way of specifying the name of
-the operation is to omit the optional argument (within \verb;[];), and
-use \verb;\opname{;\^{name-of-operation}\verb;};, anywhere within the
-body of the {\tt op} environment.
-
-The \^{list-of-arguments} is a \mmexp\ that can span multiple lines;
-force a newline with \cs\\. If present it is placed within
-parentheses.
-
-The \^{result(s)} is also any \mmexp. It is typeset to the right of
-any arguments.
-
-The \^{list-of-externals} takes the following form:
-\begin{verse}
-\verb;\ext{; \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
- \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
- \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\dots \\
-\verb;};
-\end{verse}
-Alternatively, if the list of externals is long (say, more than five
-lines) the {\tt externals\/} environmment can be used:
-\begin{verse}
-\verb;\begin{externals}; \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
- \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\quad $\langle$optional \cs\Rd\ or \cs\Wr$\rangle$
- \^{external-name(s)} {\tt :\/} \^{external-types} \cs\\ \\
-\dots \\
-\verb;\end{externals};
-\end{verse}
-\begin{dangerous}
-Some people prefer the externals identifiers to appear lined up on the
-left, some on the right. If you want them to appear on the left, say
-\cs\leftExternals; if you want them on the right, say
-\cs\rightExternals. The scope of the \cs\leftExternals\ and
-\cs\rightExternals\ commands are the current group. By default,
-you get \cs\leftExternals.
-\end{dangerous}
-
-
-The \^{pre-condition} and \^{post-condition} take similar forms:
-\begin{verse}
-\verb;\pre{;\mmexp\verb;}; \\
-\end{verse}
-or
-\begin{verse}
-\verb;\begin{precond}; \\
-\mmexp \\
-\verb;\end{precond};
-\end{verse}
-and
-\begin{verse}
-\verb;\post{;\mmexp\verb;}; \\
-\end{verse}
-or
-\begin{verse}
-\verb;\begin{postcond}; \\
-\mmexp \\
-\verb;\end{postcond};
-\end{verse}
-Use the \cs\begin\dots\cs\end\ style if the \mmexp\ is longer
-than a few lines.
-All of the constructs mentioned in the section on formulas can be used
-within pre- and post-conditions.
-
-\section{Proofs}
-
-Here's an example of typesetting proofs in the ``natural deduction''
-style.
-
-\begin{proof}
- \From E@1 \Or E@2 \\
-1 \From E@1 \\
- \Infer E@2 \Or E@1 \` $\vee$-I(h1) \\
-2 \From E@2 \\
- \Infer E@2 \Or E@1 \` $\vee$-I(h2) \\
- \Infer E@2 \Or E@1 \` $\vee$-E(h,1,2)\\
-\end{proof}
-\begin{verbatim}
- \begin{proof}
- \From E@1 \Or E@2 \\
- 1 \From E@1 \\
- \Infer E@2 \Or E@1 \by $\vee$-I(h1) \\
- 2 \From E@2 \\
- \Infer E@2 \Or E@1 \by $\vee$-I(h2) \\
- \Infer E@2 \Or E@1 \by $\vee$-E(h,1,2) \\
- \end{proof}
-\end{verbatim}
-
-Proofs are embedded within the {\tt proof} environment. (A proof does
-not have to be within a {\tt vdm} environment.) Each line of the
-proof ends with \cs\\. Lines that begin a subproof
-have \cs\From\ after the equation number. Lines that end a
-subproof have \cs\Infer\ after the equation number. Other lines
-have \cs\& after the equation number (see next example). If you
-don't need an equation number, just omit it, but you must have one of
-either \cs\From, \cs\Infer\ or \cs\& on each proof line.
-If you want to include a justification of a particular proof line at
-the right hand end of the line, type it after a \cs\by. \cs\by\
-is optional; you needn't include it if you don't need a justification.
-
-Points worth bearing in mind:
-\begin{itemize}
-\item You are automatically placed in math mode after the
- \cs\From, \cs\Infer\ or \cs\&; the math mode ends
- at the next \cs\by\ or \cs\\.
-\item You {\em cannot} break a line in the middle simply by using
- \cs\\ before \cs\by; you must use separate proof lines
- to split a formula.
-\item You are within a {\tt tabbing} environment within a proof, so
- you can use all the usual {\tt tabbing} commands (\cs\=,
- \cs\>, etc.) to line things up across proof lines. Note
- that you will explicitly have to enter math mode again after
- any of these commands though.
-\end{itemize}
-
-Here's another example:
-
-\begin{proof}
- \From \forall{x\in X}{E(x); s\in X} \\
-1 \& \Not\exists{x\in X}{\Not E(x)} \` $\Forall$-defn(h)\\
-2 \& \Not\Not E(s/x) \` $\Not\Exists$-E(1,h)\\
- \Infer E(s/x) \\
-\end{proof}
-\begin{verbatim}
-\begin{proof}
- \From \forall{x\in X}{E(x); s\in X} \\
-1 \& \Not\exists{x\in X}{\Not E(x)} \by $\Forall$-defn(h)\\
-2 \& \Not\Not E(s/x) \by $\Not\Exists$-E(1,h)\\
- \Infer E(s/x) \\
-\end{proof}
-\end{verbatim}
-
-\begin{dangerous}
-The amount of space used by the proof number can be changed by
-changing the length \cs\ProofNumberWidth. The distance from the
-left margin to the proof number is dictated by \cs\ProofIndent.
-\end{dangerous}
-
-
-\section{Customising the Style}
-
-{\em Some people are never satisfied.} We all know that it's true.
-In order to cater for those who aren't satisfied with the output from
-\Vdm, some attempt has been made to allow a limited degree of
-customisation by the user. In particular, you can alter some of the
-internal spacing chosen by \Vdm, and even have your own macros called
-at chosen places within \Vdm's macros. Naturally, you are not advised
-to try this unless you feel you have some idea of what you want, and
-what you are doing. In this section we list the things that you can
-change, in order of increasing difficulty.
-
-\subsection{Changing the Spacing}
-
-In several places, essentially arbitrary spacings have been chosen by
-the author. The dimensions of these spaces are given by {\em rubber
-lengths.}\footnote{See the \LaTeX\ book for an explanation of rubber
-lengths} If you want to change any of them, use \LaTeX's
-\cs\setlength\ or \cs\addtolength\ commands.
-For example,
-\begin{verbatim}
- \setlength{\postHeaderSkip}{13.33pt plus 2pt minus 1pt}
-\end{verbatim}
-
-\begin{dangerous}
-The {\tt plus} and {\tt minus} parts of a length let you say how much
-that length can grow or shrink by. For example, {\tt 12pt plus 2pt
-minus 1pt} means that the length will be in the range 11--14pt, with
-12pt as its ``natural'' length.
-\end{dangerous}
-
-The spaces in question all appear around \Vdm\ items such as
-operations, and in between major parts of such items. The names of
-the lengths should convey where they apply. The following table lists
-all the lengths, and their default settings. Note that an {\tt ex} is
-about the height of an ``x'' in the current font, and an {\tt em} is
-about the width of an ``M'' in the current font.
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-\em Length &\em Default size &\em Used within \\
-\hline
-\cs\preOperationSkip &2ex $+$ 0.5ex $\minus$ 0.2ex & {\tt op} env \\
-\cs\postOperationSkip &2ex $+$ 0.5ex $\minus$ 0.2ex &\\
-\cs\postHeaderSkip &.5ex $+$ .2ex $\minus$ .2ex &\\
-\cs\postExternalsSkip &.5ex $+$ .2ex $\minus$ .2ex &\\
-\cs\postPreConditionSkip &.5ex $+$ .2ex $\minus$ .2ex &\\
-\hline
-\cs\preFunctionSkip &2ex $+$ .5ex $\minus$ .2ex & {\tt fn} env \\
-\cs\postFunctionSkip &2ex $+$ .5ex $\minus$ .2ex &\\
-\cs\betweenSignatureAndBodySkip&1.2ex $+$ .3ex $\minus$ .2ex &\\
-\cs\betweenFunctionAndPreSkip&1.2ex $+$ .3ex $\minus$ .2ex &\\
-\hline
-\cs\preTypeSkip &1.2ex $+$ .5ex $\minus$ .3ex & {\tt type} command \\
-\cs\postTypeSkip &1.2ex $+$ .5ex $\minus$ .3ex &\\
-\hline
-\cs\preCompositeSkip &1.2ex $+$ .5ex $\minus$ .3ex & {\tt
-composite} env \\
-\cs\postCompositeSkip &1.2ex $+$ .5ex $\minus$ .3ex &\\
-\hline
-\cs\preRecordSkip &.75ex $+$ .3ex $\minus$ .2ex & {\tt
-record} env \\
-\cs\postRecordSkip &.75ex $+$ .3ex $\minus$ .2ex &\\
-\hline
-\cs\preFormulaSkip &1.2ex $+$ .5ex $\minus$ .3ex & {\tt
-formula} env \\
-\cs\postFormulaSkip &1.2ex $+$ .5ex $\minus$ .3ex &\\
-\hline
-\cs\preProofSkip &.75ex $+$ .3ex $\minus$ .2ex & {\tt
-proof} env \\
-\cs\postProofSkip &.75ex $+$ .3ex $\minus$ .2ex &\\
-\hline
-\end{tabular}
-\end{center}
-
-\subsection{Controlling Line and Paragraph Breaks}
-
-\TeX\ uses the notion of {\em penalties\/} to decide where line and
-page breaks go. Various values of penalty are used at places within
-\Vdm\ to control breaks. To fully understand how to choose breaks,
-read {\em The \TeX{}book}. However, put simply, penalties are whole
-numbers in the range $\minus10000$~to $10000$. A value of $10000$
-means ``never break here,'' and a value of $\minus10000$ means
-``always break here.'' Values in between penalise or encourage
-breaking proportionally, so that, e.g.,~a value of $\minus500$
-encourages a break, but by no means forces it. A value of zero is
-neutral.
-
-To assign to a penalty~\cs\p, write {\tt \cs\p=1000}, for example.
-The table below list the penalties used by \Vdm, and their default
-values.
-
-\begin{center}
-\begin{tabular}{|l|l|l|}
-\hline
-\em Penalty Name & Default Value & Where Used \\
-\hline
-\cs\preOperationPenalty & 0 & {\tt op} env \\
-\cs\preExternalPenalty & 2000 & \\
-\cs\prePreConditionPenalty & 800 & \\
-\cs\prePostConditionPenalty & 500 & \\
-\cs\postOperationPenalty & -500 & \\
-\hline
-\cs\preFunctionPenalty & 0 & {\tt fn} env \\
-\cs\betweenSignatureAndBodyPenalty&500&\\
-\cs\betweenFunctionAndPrePenalty&1000&\\
-\cs\postFunctionPenalty & -500 & \\
-\hline
-\cs\preRecordPenalty & 0 & {\tt record} env\\
-\cs\postRecordPenalty & -100 & \\
-\hline
-\cs\preProofPenalty & -100 & {\tt proof} env\\
-\cs\postProofPenalty & 0 & \\
-\hline
-\cs\preFormulaPenalty & -100 & {\tt formula} env\\
-\cs\postFormulaPenalty & 0 & \\
-\hline
-\end{tabular}
-\end{center}
-
-
-\subsection{Unforeseen Changes}
-
-It is a truism that no matter how good the designer of a piece of
-software is, he can never foresee all of its uses. In this case, the
-author is quite certain that people will use \Vdm\ for all sorts of
-things apart from typesetting VDM specifications. To cater for those
-who find that \Vdm\ does almost, but not quite, what they want, a
-number of {\em hooks\/} have been left in place. These hooks are
-macros, which at the moment do little or nothing, but which can be
-redefined by users to change the basic operation of \Vdm (see the {\tt
-vdmindex} style for one such use). Needless to
-say, anyone wishing to redefine a hook should already be competent in
-the ways of \LaTeX\ at least, and probably \TeX\ as well. Rather than
-trying to explain what the hooks do, and where they do it, the user
-should look through the commented version of \Vdm\ (usually stored as
-{\tt vdm.doc}) and figure it out for himself. Below are listed all
-the provided hooks, their default definitions, and where they are used.
-
-\begin{center}\footnotesize
-\begin{tabular}{|l|l|}
-\hline
-\em Name of hook & \em Default definition \\
-\hline
-\multicolumn{2}{|c|}{{\tt op} environment} \\
-\hline
-\cs\preOperationHook
- &\verb*;\penalty\preOperationPenalty ;\\
-\cs\betweenHeaderAndExternalsHook
- &\verb*;\penalty\preExternalPenalty ;\\
-\cs\betweenExternalsAndPreConditionHook
- &\verb*;\penalty\prePreConditionPenalty ;\\
-\cs\betweenPreAndPostConditionHook
- &\verb*;\penalty\prePostConditionPenalty ;\\
-\cs\postOperationHook
- &\verb*;\penalty\postOperationPenalty ;\\
-\hline
-\multicolumn{2}{|c|}{{\tt fn} environment} \\
-\hline
-\cs\preFunctionHook
- &\verb*;\penalty\preFunctionPenalty ;\\
-\cs\betweenSignatureAndBodyHook
- &\verb*;\penalty\betweenSignatureAndBodyPenalty ; \\
-\cs\betweenFunctionAndPreHook&\verb*;\vskip-\lastskip ;\\
- &\verb;\vskip\betweenFunctionAndPreSkip ;\\
- &\verb*;\penalty\betweenSignatureAndBodyPenalty ; \\
-\cs\postFunctionHook
- &\verb*;\penalty\postFunctionPenalty ; \\
-\hline
-\multicolumn{2}{|c|}{{\tt record} environment} \\
-\hline
-\cs\preRecordHook
- &\verb*;\penalty\preRecordPenalty ;\\
-\cs\postRecordHook
- &\verb*;\penalty\postRecordPenalty ; \\
-\hline
-\multicolumn{2}{|c|}{{\tt proof} environment} \\
-\hline
-\cs\preProofHook
- &\verb*;\penalty\preProofPenalty ;\\
-\cs\postProofHook
- &\verb*;\penalty\postProofPenalty ; \\
-\hline
-\multicolumn{2}{|c|}{{\tt formula} environment} \\
-\hline
-\cs\preFormulaHook
- &\verb*;\penalty\preFormulaPenalty ;\\
-\cs\postFormulaHook
- &\verb*;\penalty\postFormulaPenalty ; \\
-\hline
-\end{tabular}
-\end{center}
-
-
-\section{Installing the \Vdm\ files}
-
-Place the file {\tt vdm.sty} in your standard directory for \LaTeX\
-style files (your system administrator will know where this is). If
-you have the AMS fonts, change the appropriate line in {\tt vdm.sty}
-(see instructions at the head of the file).
-%If you're on a
-%UNIX\footnote{UNIX is a trademark of AT\&T} system, you can make the
-%{\tt .sty} file from the {\tt .doc} file with the command:
-%\begin{verbatim}
-% sed -e '/^[ ]*%/d' -e 's/%.*/%/' -e '/^$/d' vdm.doc > vdm.sty
-%\end{verbatim}
-%There are two characters between the square brackets: a tab and a
-%space. If you're on some other system, figure out an equivalent
-%command, or make the two files the same.
-
-
-\section{New \Vdm\ commands (introduced for the {\sc bsi} version)}
-
-\begin{itemize}
- \item There is a new keyword, \cs\rem.
- \item Operations can also have an {\em error condition\/} part, typeset
- after the postcondition. The error condition is placed in an {\tt
- errcond} environment. An alternative short form, \cs\err, is also
- available, which works in the same way as \cs\pre\ and \cs\post.
-
- {\emergencystretch=4pt In support of this new part, there is a hook,
- \cs\betweenPostAndErrConditionHook, defined to be
- \cs\penalty\ \cs\preErrConditionPenalty\ (the default penalty is
- 500). The preceding white space is defined by
- \cs\preErrConditionSkip\ (default .5ex $+$ .2ex $\minus$ .2ex).}
-
- \item \cs\Others\ is an alias for \cs\Otherwise.
- \item Sequents are supported using the {\tt sequent} command,
- thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\sequent{A}{B}\\
-\sequent*{Truth,Beauty,eq-intr}{Truth=Beauty}
-\end{formula}
-\end{leftside}\begin{rightside}
-\sequent{A}{B}
-\sequent*{Truth,Beauty,eq-intr}
- {Truth=Beauty}
-\end{rightside}
-\end{minipage}
-
- \item Optional items can be typeset using \cs\Opt, thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-$\Opt{fred}$
-\end{leftside}\begin{rightside}
-\Opt{fred}
-\end{rightside}
-\end{minipage}
-
- \item There are two new monadic operators, \cs\abs\ and \cs\merge.
-
- \item A non-empty sequence type can be defined using \cs\neseqof,
- thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{formula}
-\neseqof{\Nat}
-\end{formula}
-\end{leftside}\begin{rightside}
-\neseqof{\Nat}
-\end{rightside}
-\end{minipage}
-
- \item Restricted types (those with invariants) can be typeset, with
- or without initialisation, using \cs\ritype\ and \cs\rtype, thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\rtype{Partition}{\setof{(\setof{\Nat})}}{inv-Partition(p)}
-\ritype{Dict}{\Bool \x (\mapof{Letter}{Dict})}{\true}{(\true,\emptymap)}
-\end{leftside}\begin{rightside}
-\rtype{Partition}
- {\setof{(\setof{\Nat})}}
- {inv-Partition(p)}
-\ritype{Dict}
- {\Bool \x (\mapof{Letter}{Dict})}
- {\true}
- {(\true,\emptymap)}
-\end{rightside}
-\end{minipage}
-
- Accompanying these commands are \cs\betweenTypeAndInvSkip\ (default
- .5ex $+$ .3ex $\minus$ .2ex) and \cs\betweenInvAndInitSkip\
- (same default).
-
- \item Record types may also have invariants and initial states
- attached, using the \cs\inv\ and \cs\init\ commands within the {\tt
- record} environment, thus:
-
-\noindent\begin{minipage}{\textwidth}\begin{leftside}
-\begin{record}{D}
- day : Day \\
- year : Year
-\inv{(mk-D(d,y)) \DEF\\
-\quad is-leapyr(y) \Or d \le 365}
-\init{day=40 \And year=1962}
-\end{record}
-\end{leftside}\begin{rightside}
-\begin{record}{D}
- day : Day \\
- year : Year
-\inv{(mk-D(d,y)) \DEF
- is-leapyr(y) \Or d \le 365}
-\init{day=40 \And year=1962}
-\end{record}
-\end{rightside}
-\end{minipage}
-
- {\emergencystretch=4pt To go with these are \cs\betweenRecordAndInvHook,
- \cs\betweenInvAndInitHook, \cs\betweenRecordAndInvSkip\ (default
- .5ex $+$ .2ex $\minus$ .1ex), and \cs\betweenInvAndInitSkip\
- (same default).}
-
-\end{itemize}
-
-\section{Acknowledgements}
-
-Many people have passed on useful suggestions and comments about \Vdm\
-and this documentation; many thanks to all of them. In particular I
-would like to acknowledge the extensive testing done by Lynn Marshall
-while preparing her thesis, and her helpful comments and ideas, and
-the numerous worthwhile discussions with Cliff Jones. Cliff, in
-particular, deserves the highest commendation for bravery, in actually
-using these macros in his book. Thanks to David Carlisle for helping
-with the conversion to \TeX~3.
-
-\end{document}
-