summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/vdm
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/vdm
Initial commit
Diffstat (limited to 'macros/latex/contrib/vdm')
-rw-r--r--macros/latex/contrib/vdm/vdm.pdfbin0 -> 197434 bytes
-rw-r--r--macros/latex/contrib/vdm/vdm.sty1185
-rw-r--r--macros/latex/contrib/vdm/vdm.tex1562
3 files changed, 2747 insertions, 0 deletions
diff --git a/macros/latex/contrib/vdm/vdm.pdf b/macros/latex/contrib/vdm/vdm.pdf
new file mode 100644
index 0000000000..4c66bbf1c2
--- /dev/null
+++ b/macros/latex/contrib/vdm/vdm.pdf
Binary files differ
diff --git a/macros/latex/contrib/vdm/vdm.sty b/macros/latex/contrib/vdm/vdm.sty
new file mode 100644
index 0000000000..8ff0260c04
--- /dev/null
+++ b/macros/latex/contrib/vdm/vdm.sty
@@ -0,0 +1,1185 @@
+%%% ====================================================================
+%%% @LaTeX-style-file{
+%%% author = "Mario Wolczko",
+%%% version = "4.00",
+%%% date = "14 October 1994",
+%%% filename = "vdm.sty",
+%%% 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 = "LaTeX macros for typesetting VDM
+%%% specifications.
+%%% NOTE
+%%% Mario no longer works at Manchester
+%%% This is a minimal update to LaTeX2e
+%%% By David Carlisle",
+%%% }
+%%% ====================================================================
+%
+% BSI VDM documentstyle option for LaTeX
+%
+% M. Wolczko
+%
+%
+% Dept. of Computer Science Internet: mario@cs.man.ac.uk
+% The University uucp: mcsun!uknet!man.cs!mario
+% Manchester M13 9PL JANET: mario@uk.ac.man.cs
+% U.K. Tel: +44-61-275 6146 (FAX: 6236)
+%
+% Version for LaTeX2e by David Carlisle.
+% Just constructed by removing all the old font wierdness.
+% Not tested at all!
+%
+%
+%----------------------------------------------------------------
+%
+% Installation-dependent features
+%
+
+
+\newif\ifams@
+
+\ams@true
+
+\ifams@
+ \RequirePackage{amsfonts}
+\fi
+
+%----------------------------------------------------------------
+%
+% The vdm environment
+%
+% record whether we were in horizontal mode when entering...
+\newif\ifhm@
+
+\def\vdm{\ifhmode\hm@true\else\hm@false\fi
+ \@changeMathmodeCatcodes\@postUnderPenalty10000\relax}
+
+% after an \end{vdm} the next paragraph is not indented unless a \par
+% comes first (if we entered in horizontal mode). This is a bit of a
+% kludge!
+\def\endvdm{\ifhm@\else
+ \global\let\par=\@undonoindent
+ \global\everypar={{\setbox0=\lastbox}\global\everypar={}%
+ \global\let\par=\@@par}%
+ \fi}
+
+\def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}
+
+%-----------------------------------------------------------------
+%
+% Controlling line and page breaks
+%
+% Text within the vdm environment is essentially mathematical in
+% nature, so requires special care. Whenever outer vertical mode is
+% entered, the \@beginVerticalVDM command should be used. This sets
+% up \leftskip, \rightskip, \baselineskip, \lineskip and
+% \lineskiplimit to conform with the overall style.
+%
+% When entering unrestricted horizontal mode, the \@beginHorizontalVDM
+% command should be used. This sets up:
+% \leftskip and \rightskip to 0,
+% \\ to do line breaking
+% ragged right line breaking, with special penalties, and
+% enters math mode.
+% \@endHorizontalVDM should be called when leaving unrestricted
+% horizontal mode.
+
+\def\@beginVerticalVDM{\@changeMargins\@changeBaselineskip}
+
+\def\@beginHorizontalVDM{\@restoreLineSeparator
+ \@restoreMargins\@raggedRight\noindent$\strut\relax}
+\def\@endHorizontalVDM{\relax\strut$}
+
+% \VDMindent is used for \leftskip within VDM, \VDMrindent for
+% \rightskip, \VDMbaselineskip for \baselineskip
+\newdimen\VDMindent \VDMindent=\parindent
+\newdimen\VDMrindent \VDMrindent=\parindent
+\def\VDMbaselineskip{\baselineskip}
+
+\def\@changeMargins{\leftskip=\VDMindent \rightskip=\VDMrindent}
+\def\@restoreMargins{\advance\hsize by-\leftskip
+ \advance\hsize by-\rightskip
+ \leftskip=0pt \rightskip=0pt}
+\def\@changeBaselineskip{\baselineskip=\VDMbaselineskip
+ \lineskip=0pt \lineskiplimit=0pt
+ % need to alter the size of struts, too
+ \setbox\strutbox\hbox{\vrule height.7\baselineskip
+ depth.3\baselineskip width\z@}}
+
+% these are used in externals, records and cases
+\def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
+\def\@restoreLineSeparator{\let\\=\newline}
+
+\def\@raggedRight{\rightskip=0pt plus 1fil
+ \hyphenpenalty=-100 \linepenalty=200
+ \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
+
+% ------------------------------------------------------------------------
+
+% Font and Character Changes
+
+% make a-zA-Z use the \it family within math mode, and ~ mean \hook.
+% Digits 0-9 remain as normal.
+\everymath=\expandafter{\the\everymath\vdm@it
+ \@changeMathmodeCatcodes}%
+\everydisplay=\expandafter{\the\everydisplay\vdm@it
+ \@changeMathmodeCatcodes}%
+
+\def\vdm@it{\@fontswitch\it\mathit}
+
+\mathcode`\0="0030
+\mathcode`\1="0031
+\mathcode`\2="0032
+\mathcode`\3="0033
+\mathcode`\4="0034
+\mathcode`\5="0035
+\mathcode`\6="0036
+\mathcode`\7="0037
+\mathcode`\8="0038
+\mathcode`\9="0039
+
+\mathchardef\Gamma="0000
+\mathchardef\Delta="0001
+\mathchardef\Theta="0002
+\mathchardef\Lambda="0003
+\mathchardef\Xi="0004
+\mathchardef\Pi="0005
+\mathchardef\Sigma="0006
+\mathchardef\Upsilon="0007
+\mathchardef\Phi="0008
+\mathchardef\Psi="0009
+\mathchardef\Omega="000A
+
+% If the user really wants the normal codes, she can call \defaultMathcodes
+%\def\defaultMathcodes{\let\vdm@it\relax}
+\def\defaultMathcodes{\let\vdm@it\relax}
+
+
+% remember the original mathcode of minus sign
+\edef\@minuscode{\the\mathcode`\-}
+
+\def\mathminus{\mathcode`\-=\@minuscode }
+\def\textminus{\mathcode`\-="002D }
+% by default, use text minus
+%\textminus
+
+% make a : into punctuation, a - into a letter, and | mean \mid
+ % NFSS-change
+ % \mathcode`\-="042D changed to \mathcode`\-="002D as we can not rely on
+ % \itfam being fam 4.
+ \def\@changeOtherMathcodes{\mathcode`\:="603A \textminus
+ \mathcode`\|="326A \mathchardef\Or="325F }% this is a rel to get 5mu spacing
+ \def\relbar{\mathrel{\smash\minus}}% redefine because mathcode of -
+ % has changed
+
+
+% alternative underscore
+\def\@VDMunderscore{\leavevmode
+ \kern.06em\vbox{\hrule\@height .2ex\@width .3em}\penalty\@postUnderPenalty
+ \hskip 0.1em}
+
+% Allow line breaks after an underscore, but not in vdm mode (see
+% \vdm). This is so long identifiers can be broken when run
+% into paragraphs.
+\newcount\@postUnderPenalty \@postUnderPenalty=200
+
+% now require some catcode trickery to enable us to change _ when we want to
+{\catcode`\_=\active
+ \gdef\@changeGlobalCatcodes{% make _ a normal char
+ \catcode`\_=\active \let_=\@VDMunderscore}
+ \gdef\@changeMathmodeCatcodes{%
+ % make ~ mean \hook, " do text, @ mean subscript
+ \let~=\hook
+ \catcode`\@=8
+ \mathcode`\"="8000 }
+ \uccode`\~=`\"%
+ \gdef\underscoreoff{% make _ a normal char
+ \catcode`\_=\active \let_=\@VDMunderscore}
+ \gdef\underscoreon{% restore underscore to usual meaning
+ \catcode`\_=8}
+\uppercase{\gdef~}#1"{\nfss@text{\rm #1}}}
+
+%----------------------------------------------------------------
+%
+% Keywords
+%
+\ifx\fmtname\@fmtname
+ \def\keywordFontBeginSequence{\sf}% user-definable
+\else\ifx\fmtname\@psfmtname
+ \def\keywordFontBeginSequence{\sf}% Helvetica is OK
+\else
+ \def\keywordFontBeginSequence{\bf}% good for SliTeX
+\fi\fi
+
+\def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
+
+\def\makeNewKeyword#1#2{% use \newcommand for extra checks
+ \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}
+
+\makeNewKeyword{\nil}{nil}
+\makeNewKeyword{\True}{true}
+\makeNewKeyword{\true}{true}
+\makeNewKeyword{\False}{false}
+\makeNewKeyword{\false}{false}
+\makeNewKeyword{\rem}{ rem }
+
+\def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}
+
+%----------------------------------------------------------------
+%
+% monadic operator creation
+%
+\def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}
+
+%----------------------------------------------------------------
+%
+% primitive numeric types
+%
+% use the AMS fonts for these if possible
+
+\ifams@
+ \DeclareMathSymbol{\Bool} {\mathord}{AMSb}{"42} % Booleans
+ \DeclareMathSymbol{\Nat} {\mathord}{AMSb}{"4E} % Natural numbers
+ \def\Nati{\Nat_1} % Positive natural numbers
+ \DeclareMathSymbol{\Int} {\mathord}{AMSb}{"5A} % Integers
+ \DeclareMathSymbol{\Real} {\mathord}{AMSb}{"52} % Reals
+ \DeclareMathSymbol{\Rat} {\mathord}{AMSb}{"51} % Rationals
+\else
+ \def\Bool{\nfss@text{\bfseries B\/}}
+ \def\Nat{\nfss@text{\bfseries N\/}}
+ \def\Nati{\hbox{$\nfss@text{\bfseries N}_1$}}
+ \def\Int{\nfss@text{\bfseries Z\/}}
+ \def\Real{\nfss@text{\bfseries R\/}}
+ \def\Rat{\nfss@text{\bfseries Q\/}}
+\fi
+\let\Natone=\Nati % just for an alternative
+
+%----------------------------------------------------------------
+%
+% Operations
+%
+% The op environment. Within op you can specify args,
+% result, etc. which are gathered into registers, and output when the
+% op env. ends.
+%
+% The optional argument is the operation name
+
+% shorthand for an operation on its own: the vdmop env.
+\def\vdmop{\vdm\op} \def\endvdmop{\endop\endvdm}
+
+% registers constructed within an op environment
+\newtoks\@operationName
+\newbox\@operationNameBox
+\newif\ifArgumentListEncountered@
+\newtoks\@argumentListTokens
+\newtoks\@resultNameAndTypeTokens
+\newbox\@externalsBox
+\newbox\@preConditionBox
+\newbox\@postConditionBox
+\newbox\@errConditionBox
+
+\def\op{% clear temporaries, deal with optional arg
+ \setbox\@operationNameBox=\hbox{}%
+ \@argumentListTokens={}\ArgumentListEncountered@false
+ \@resultNameAndTypeTokens={}%
+ \setbox\@externalsBox=\box\voidb@x
+ \setbox\@preConditionBox=\box\voidb@x
+ \setbox\@postConditionBox=\box\voidb@x
+ \par\preOperationHook
+ \vskip\preOperationSkip
+ \@beginVerticalVDM
+ \@ifnextchar [{\@opname}{}}
+
+% breaking parameters
+\newcount\preOperationPenalty \preOperationPenalty=0
+\newcount\preExternalPenalty \preExternalPenalty=2000
+\newcount\prePreConditionPenalty \prePreConditionPenalty=800
+\newcount\prePostConditionPenalty \prePostConditionPenalty=500
+\newcount\preErrConditionPenalty \preErrConditionPenalty=500
+\newcount\postOperationPenalty \postOperationPenalty=-500
+
+% gaps between bits of operations
+\newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
+\newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
+\newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
+\newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
+\newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
+\newskip\preErrConditionSkip \preErrConditionSkip=.5ex plus .2ex minus .2ex
+
+\def\endop{% make up operation
+ % IMPORTANT---don't remove the vskips in this macro
+ % if you don't want one, set it to 0pt
+ \vskip 0pt
+ \@setOperationHeader
+ \betweenHeaderAndExternalsHook
+ \vskip\postHeaderSkip
+ \ifvoid\@externalsBox
+ \betweenExternalsAndPreConditionHook
+ \else \moveright\VDMindent\box\@externalsBox
+ \betweenExternalsAndPreConditionHook
+ \vskip\postExternalsSkip
+ \fi
+ \ifvoid\@preConditionBox
+ \betweenPreAndPostConditionHook
+ \else \moveright\VDMindent\box\@preConditionBox
+ \betweenPreAndPostConditionHook
+ \vskip\postPreConditionSkip
+ \fi
+ \ifvoid\@postConditionBox
+ \betweenPostAndErrHook
+ \else \moveright\VDMindent\box\@postConditionBox
+ \betweenPostAndErrConditionHook
+ \fi
+ \ifvoid\@errConditionBox
+ \else \vskip\preErrConditionSkip
+ \moveright\VDMindent\box\@errConditionBox
+ \fi
+ \postOperationHook
+ \vskip\postOperationSkip}
+
+% hooks for user-defined expansion
+% TeX is in outer vertical mode when these are called.
+% ALWAYS leave TeX in vertical mode after these macros have been called
+\def\preOperationHook{\penalty\preOperationPenalty }
+\def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
+\def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
+\def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
+\def\betweenPostAndErrConditionHook{\penalty\preErrConditionPenalty }
+\def\postOperationHook{\penalty\postOperationPenalty }
+
+% combine the operation name, argument list and result
+\def\@setOperationHeader{%
+ \moveright\VDMindent\vtop{%
+ \ifArgumentListEncountered@
+ \setbox\@operationNameBox=%
+ \hbox{\unhbox\@operationNameBox$($}\fi
+ \hangindent=\wd\@operationNameBox \hangafter=1
+ \noindent\kern-.05em\box\@operationNameBox
+ \@beginHorizontalVDM
+ \ifArgumentListEncountered@\the\@argumentListTokens)\fi
+ \ \the\@resultNameAndTypeTokens
+ \@endHorizontalVDM}}
+
+% set the operation name
+% \opname{name-of-operation}
+\def\opname#1{\@opname[#1]}
+\def\@opname[#1]{\@operationName={#1}%
+ \global\setbox\@operationNameBox=\hbox{$\relax#1$\ }}
+
+% set up the argument list
+% \args{ argument \\ argument \\ argument... } where \\ forces a line break
+% This is also used in the fn environment
+\def\args{\global\ArgumentListEncountered@true \global\@argumentListTokens=}
+
+% result name and type
+\def\res{\global\@resultNameAndTypeTokens=}
+
+% externals list
+%
+% An external list could be either very long or very short, so we provide
+% two forms. One is the short \ext{..} command, the other is the externals
+% environment.
+% Externals are always separated by \\
+%
+
+% we have to mess a little to get the catcode of : right
+\def\ext{\bgroup\@makeColonActive\@ext}
+\def\@ext#1{\externals#1\endexternals\egroup}
+
+\def\externals{\global\setbox\@externalsBox=%
+ \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
+\def\endexternals{\@endIndentedPara{\@endAlignment}}
+
+\def\@setUpExternals{\@makeColonActive\@changeLineSeparator\@beginAlignment}
+
+% more catcode trickery for :
+{\catcode`\:=\active
+ \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}
+
+% the \expandafters are necessary because TeX doesn't expand
+% \halign specs when scanning for # and &
+\def\@beginAlignment{\expandafter\halign\expandafter\bgroup
+ \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
+\def\@endAlignment{\crcr\egroup}
+
+% the user can decide on the exact alignment of the field names
+\newtoks\@extAlign
+\def\leftExternals{\@extAlign={$##$\hfil}}
+\def\rightExternals{\@extAlign={\hfil$##$}}
+\leftExternals
+
+\makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }
+
+% pre-condition, post-condition and err-condition
+%
+% once again we provide short forms \pre, \post, \err and environments
+% precond, postcond and errcond
+\def\pre#1{\precond#1\endprecond}
+\def\precond{\global\setbox\@preConditionBox=%
+ \@beginMathIndentedPara{\hsize}{pre }}
+\def\endprecond{\@endMathIndentedPara}
+
+\def\post#1{\postcond#1\endpostcond}
+\def\postcond{\global\setbox\@postConditionBox=%
+ \@beginMathIndentedPara{\hsize}{post }}
+\def\endpostcond{\@endMathIndentedPara}
+
+\def\err#1{\errcond#1\enderrcond}
+\def\errcond{\global\setbox\@errConditionBox=%
+ \@beginMathIndentedPara{\hsize}{errs }}
+\def\enderrcond{\@endMathIndentedPara}
+
+
+%----------------------------------------------------------------
+%
+% Box man\oe uvres
+%
+% Here's where all the tricky box manipulation commands go
+%
+% \@beginIndentedPara begins construction of a \hbox of width #1
+% which contains keyword #2 to the left of a para in a vtop.
+% #3 is evaluated within the inner vtop.
+% endIndentedPara closes the box off; its arg. is evaluated just
+% before closing the box.
+%
+\def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
+ \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
+\def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
+
+% \@beginMathIndentedPara places the para in vdm mode
+\def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
+ {\@beginHorizontalVDM}}
+\def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontalVDM}}
+
+% \@belowAndIndent#1#2 places #2 in a vbox below and to the right of #1
+\def\@belowAndIndent#1#2{#1\hfil\break
+ \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
+
+% \@mathIndentedPara does the whole thing
+\def\@mathIndentedPara#1#2#3{\@beginMathIndentedPara{#1}{#2}#3%
+ \@endMathIndentedPara}
+%----------------------------------------------------------------
+%
+% Constructions
+%
+% Here are all the standard constructions.
+% The only tricky one is \cases.
+% Those that construct a box must be made to make that box of 0 width,
+% and force a line break immediately afterwards.
+
+% \If mm-exp \Then mm-exp \Else mm-exp \Fi
+% multi-line indented if-then-else
+%
+\def\If#1\Then#2\Else#3\Fi{\vtop{%
+ \@mathIndentedPara{0pt}{if }{#1}%
+ \@mathIndentedPara{0pt}{then }{#2}%
+ \@mathIndentedPara{0pt}{else }{#3}}}
+
+% \SIf mm-exp \Then mm-exp \Else mm-exp \Fi
+% single line if-then-else
+\def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@beginHorizontalVDM
+ \kw{if }\nobreak#1\penalty0\hskip 0.5em
+ \kw{then }\nobreak#2\penalty-100\hskip 0.5em % break here OK
+ \kw{else }\nobreak#3\@endHorizontalVDM}\hss}}
+
+% \Let mm-exp \In mm-exp2
+% multi-line let..in ; mm-exp2 is `curried'
+\def\Let#1\In{\vtop{%
+ \@mathIndentedPara{0pt}{let }{#1\hskip 0.5em\kw{in}}}\hfil\break}
+
+% \SLet mm-exp \In mm-exp
+% single-line let..in
+\def\SLet#1\In#2{\hbox to 0pt{\vtop{\@beginHorizontalVDM
+ \kw{let }\nobreak#1\hskip 0.5em
+ \kw{in }\penalty-100 #2\@endHorizontalVDM}\hss}}
+
+% multi-line cases
+%
+% \Cases{ selecting-mm-exp }
+% from-case1 & to-case1 \\
+% from-case2 & to-case2 \\
+% ...
+% from-casen & to-casen
+% \Otherwise{ mm-exp }
+% \Endcases[optional text for the rest of the line]
+
+\newif\ifOtherwiseEncountered@
+\newtoks\@OtherwiseTokens
+
+\def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
+ \@mathIndentedPara{\hsize}{cases }{\strut
+ #1\hskip 0.5em\strut\kw{of}}%
+ \bgroup % we might be in a nested case, so we have to
+ % save the \Otherwise bits we might lose
+ \OtherwiseEncountered@false \@changeLineSeparator
+ \@beginCasesAlignment}
+
+% the user can decide on the exact alignment
+\newtoks\@casesDef
+\def\leftCases{\@casesDef={$##$\hfil}}
+\def\rightCases{\@casesDef={\hfil$##$}}
+\rightCases
+
+% the \expandafters are necessary because TeX doesn't expand
+% \halign specs when scanning for # and &
+\def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
+ \the\@casesDef&$\,\rightarrow##$\hfil\cr}
+
+\def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
+\let\Others=\Otherwise
+
+\def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
+\def\@endCasesAlignment{\crcr\egroup}
+\def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
+ \@mathIndentedPara{\hsize}{others }{%
+ \strut\the\@OtherwiseTokens\strut}
+ \fi}
+
+% must test for the optional arg to follow the end
+\def\@setEndcases{\noindent
+ \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
+\def\@unbracket[#1]{$#1$\@finalCaseEnd}
+\def\@finalCaseEnd{\egroup\hss\egroup}%\hfil\break
+
+%----------------------------------------------------------------
+%
+% special symbols
+
+% defined as
+\def\DEF{\raise.5ex
+ \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle
+
+
+% cross product
+\let\x=\times
+
+% logical connectives
+%
+\def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
+ \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
+\let\iff=\Iff
+\def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
+ \mskip 6mu plus 2mu minus 1mu}
+\let\implies=\Implies
+% see changeOtherMathcodes for \Or
+\let\And=\land
+\let\@and=\and
+\def\and{\ifmmode\And\else\@and\fi}
+% use \neg for logical not, or
+\def\Not{\neg\,}
+
+% quantification
+%
+
+\DeclareMathSymbol{\Exists} {\mathord}{symbols}{"39}
+\DeclareMathSymbol{\Forall} {\mathord}{symbols}{"38}
+\DeclareMathSymbol{\suchthat} {\mathbin}{symbols}{"01}
+
+\def\exists{\@ifstar{\@splitExists}{\@normalExists}}
+\ifams@
+ \DeclareMathSymbol{\@nexists} {\mathop}{AMSb}{"40}
+ % crossed out existential quantifier
+\else
+ \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
+\fi
+\def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
+\def\forall{\@ifstar{\@splitForall}{\@normalForall}}
+\def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
+\def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}
+
+\def\@normalExists#1#2{{\Exists#1}\suchthat #2}
+\def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
+\def\@normalForall#1#2{{\Forall#1}\suchthat #2}
+\def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
+\def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}
+
+\def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
+\def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
+\def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
+\def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
+\def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
+%
+% sequents
+%
+\let\Tstlp=\vdash
+%
+\def\sequent{\@ifstar{\@splitSequent}{\@normalSequent}}
+\def\@normalSequent#1#2{{#1}\:\Tstlp\: #2}
+\def\@splitSequent#1{\@belowAndIndent{#1\;\Tstlp}}
+
+%
+% strachey brackets
+%
+% (see TeXbook, p.437)
+\def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
+
+% function composition
+%
+\let\compf=\circ
+
+%----------------------------------------------------------------
+%
+% function environment
+%
+% This environment is similar to the op environment, but is used for
+% function definition.
+%
+% The mandatory first parameter is the name of the function, the
+% second is the argument list.
+%
+% The *-form simply doesn't force the parentheses round the argument list
+
+\def\fn{\parens@true\@beginVDMfunction}
+\@namedef{fn*}{\parens@false\@beginVDMfunction}
+\@namedef{endfn*}{\endfn}
+
+% short form
+\def\vdmfn{\vdm\parens@true \@beginVDMfunction}
+\def\endvdmfn{\endfn\endvdm}
+\@namedef{vdmfn*}{\vdm\parens@false \@beginVDMfunction}
+\@namedef{endvdmfn*}{\endfn\endvdm}
+
+% registers used within the fn environment
+\newtoks\@fnName
+\newbox\@fnNameBox
+\newif\ifsignatureEncountered@
+\newtoks\@signatureTokens
+\newbox\@fnDefnBox
+\newif\ifparens@
+
+\def\@beginVDMfunction#1#2{%
+ \@fnName={#1}%
+ \setbox\@fnNameBox=\hbox{$#1$}%
+ \setbox\@preConditionBox=\box\voidb@x % for people who want to do
+ \setbox\@postConditionBox=\box\voidb@x% implicit defns
+ \@signatureTokens={}\signatureEncountered@false
+ \ifparens@
+ \@argumentListTokens={(#2)}%
+ \else
+ \@argumentListTokens={#2}%
+ \fi
+ \par\preFunctionHook
+ \vskip\preFunctionSkip
+ \@beginVerticalVDM
+ \@beginFnDefn}
+
+% read in a signature
+\def\signature{\global\signatureEncountered@true \global\@signatureTokens=}
+
+\def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
+ \hangindent=2em \hangafter=1 \@beginHorizontalVDM
+ \advance\hsize by-2em % this fools vboxes within the
+ % function body about the hanging indent...yuk.
+ % If you change the size of the indent, change the
+ % corresponding line in \endfn.
+ \copy\@fnNameBox \the\@argumentListTokens
+ \quad\DEF\penalty-100\quad }
+
+\newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
+\newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
+\newskip\betweenSignatureAndBodySkip
+\betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
+\newskip\betweenFunctionAndPreSkip
+\betweenFunctionAndPreSkip=1.2ex plus .3ex minus .2ex
+
+\def\endfn{%
+ \advance\hsize by 2em% matches the dirty \advance in \@beginFnDefn
+ \@endHorizontalVDM
+ \egroup % this ends the vtop we started in \@beginFnDefn
+ \ifsignatureEncountered@
+ \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
+ \dimen255=\wd0 \noindent \box0
+ \vtop{\advance\hsize by-\dimen255 \@beginHorizontalVDM
+ \the\@signatureTokens \@endHorizontalVDM}\par
+ \betweenSignatureAndBodyHook
+ \vskip\betweenSignatureAndBodySkip
+ \fi
+ \moveright\VDMindent\box\@fnDefnBox\,
+ \ifvoid\@preConditionBox
+ \betweenPreAndPostConditionHook
+ \vskip\postFunctionSkip
+ \else \betweenFunctionAndPreHook
+ \vskip\betweenFunctionAndPreSkip
+ \moveright\VDMindent\box\@preConditionBox
+ \betweenPreAndPostConditionHook
+ \vskip\postPreConditionSkip
+ \fi
+ \ifvoid\@postConditionBox
+ \postFunctionHook
+ \else \moveright\VDMindent\box\@postConditionBox
+ \postFunctionHook
+ \vskip\postOperationSkip
+ \fi}
+
+\newcount\preFunctionPenalty \preFunctionPenalty=0
+\newcount\betweenSignatureAndBodyPenalty
+ \betweenSignatureAndBodyPenalty=10000
+\newcount\betweenFunctionAndPrePenalty \betweenFunctionAndPrePenalty=1000
+\newcount\postFunctionPenalty \postFunctionPenalty=-500
+
+% These are called in outer vertical mode---they must also exit in this mode
+\def\preFunctionHook{\penalty\preFunctionPenalty }
+\def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
+\def\betweenFunctionAndPreHook{\penalty\betweenFunctionAndPrePenalty }
+\def\postFunctionHook{\penalty\postFunctionPenalty }
+
+% other function-related things
+%
+
+% function arrow
+\def\to{\penalty-100\rightarrow}
+
+% explicit lamdba function
+\def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
+\def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
+\def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
+ {\lambda#1}\suchthat\hfil\break
+ \@mathIndentedPara{\hsize}{\qquad}{#2}}
+
+%----------------------------------------------------------------
+%
+% Optional fields
+%
+\def\Opt#1{\big[#1\big]}
+
+
+%----------------------------------------------------------------
+%
+% Sets
+
+% new set type
+\def\setof#1{#1-\kw{set}}
+
+% set enumeration
+\def\set#1{\{#1\}}
+
+% empty set
+\def\emptyset{\{\,\}}
+
+% usual LaTeX operators apply: \in \notin \subset \subseteq
+\let\inter=\cap \let\intersection=\inter
+\let\Inter=\bigcap \let\Intersection=\Inter
+\let\union=\cup
+\let\Union=\bigcup
+
+\mathchardef\minus="2200
+
+\def\diff{\minus} \let\difference=\diff
+
+\newMonadicOperator{\card}{card}
+\newMonadicOperator{\Min}{min}
+\newMonadicOperator{\Max}{max}
+\newMonadicOperator{\abs}{abs}
+
+%----------------------------------------------------------------
+%
+% Map type
+
+% new map type
+\def\mapof#1#2{#1\buildrel m\over\longrightarrow#2}
+
+% one-one map
+\def\mapinto#1#2{#1\buildrel m\over\longleftrightarrow#2}
+
+% map enumeration
+\def\map#1{\{#1\}}
+
+% empty map
+\def\emptymap{\{\,\}}
+
+% map operators
+%
+% use \mapsto for |->
+% overwrite
+\def\owr{\dagger}
+
+\let\dres=\lhd
+\let\rres=\rhd
+
+
+% domain subtraction
+\def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
+ \lower.1ex\hbox{$\dres$}$}}}
+
+% range subtraction
+\def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
+ \lower.1ex\hbox{$\rres$}$}}}
+
+\newMonadicOperator{\dom}{dom}
+\newMonadicOperator{\rng}{rng}
+\newMonadicOperator{\merge}{merge}
+
+%----------------------------------------------------------------
+%
+% Sequences
+%
+
+% new type
+\def\seqof#1{#1^*}
+
+% non-empty sequence
+\def\neseqof#1{#1^+}
+
+% enumeration
+\def\seq#1{[#1]}
+
+% empty sequence
+\def\emptyseq{[\,]}
+
+\newMonadicOperator{\len}{len}
+\newMonadicOperator{\hd}{hd}
+\newMonadicOperator{\tl}{tl}
+\newMonadicOperator{\elems}{elems}
+\newMonadicOperator{\inds}{inds}
+\def\cons#1{\kw{cons}\nobreak(#1)}
+
+% sequence concatenation
+
+\DeclareMathSymbol{\@sc@nc} {\mathbin}{AMSb}{"79}
+
+\ifams@
+ \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\@sc@nc$}}}}
+\else
+ % this is truly yukky
+ \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
+ \raise0.2ex\hbox{\it\char"12}}}}
+\fi
+
+% distributed concatenation
+\newMonadicOperator{\Conc}{dconc}
+
+%----------------------------------------------------------------
+%
+% type equation
+%
+\newtoks\@typeName
+\def\type#1#2{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
+ \@beginVerticalVDM
+ \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
+ \@endHorizontalVDM}
+ \postTypeHook \vskip\postTypeSkip}}
+
+% restricted type (has invariant)
+\def\rtype#1#2#3{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
+ \@beginVerticalVDM
+ \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
+ \@endHorizontalVDM}
+ \vskip\betweenTypeAndInvSkip
+ \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
+ \postTypeHook \vskip\postTypeSkip}}
+
+% initialised type
+\def\ritype#1#2#3#4{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
+ \@beginVerticalVDM
+ \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
+ \@endHorizontalVDM}
+ \vskip\betweenTypeAndInvSkip
+ \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
+ \vskip\betweenInvAndInitSkip
+ \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{#4}%
+ \postTypeHook \vskip\postTypeSkip}}
+
+\def\preTypeHook{} \def\postTypeHook{}
+\newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
+\newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
+\newskip\betweenTypeAndInvSkip
+ \betweenTypeAndInvSkip=.5ex plus .3ex minus .2ex
+\newskip\betweenInvAndInitSkip
+ \betweenInvAndInitSkip=.5ex plus .3ex minus .2ex
+
+%----------------------------------------------------------------
+%
+% Composite Objects
+%
+
+% literal composition; we have a compose and a composite env.
+
+% single line compose
+\@namedef{composite*}#1{\kw{compose }$\relax#1\relax$\kw{ of }$\relax}
+\@namedef{endcomposite*}{\relax$\kw{ end}}
+
+% multiple line version
+\def\composite#1{\bgroup\vskip\preCompositeSkip
+ \@beginVerticalVDM
+ \moveright\VDMindent\vtop\bgroup
+ \@beginHorizontalVDM
+ \kw{compose }#1\kw{ of}%
+ \@endHorizontalVDM
+ \@makeColonActive\@changeLineSeparator
+ \expandafter\halign\expandafter\bgroup\expandafter\qquad
+ \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
+\def\endcomposite{\crcr\egroup % closes \halign
+ \kw{end}\egroup % ends the \vtop
+ \vskip\postCompositeSkip\egroup}
+
+\def\scompose#1#2{\@nameuse{composite*}{#1}{#2}\@nameuse{endcomposite*}}
+
+\newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
+\newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex
+
+% record composites; likewise we have a short and a long form
+\newtoks\@recordName
+
+\def\record#1{%
+ \InvEncountered@false \InitEncountered@false
+ \@invTokens={}\@initTokens={}
+ \@recordName{#1}
+ \par\preRecordHook
+ \vskip\preRecordSkip
+ \@beginVerticalVDM
+ \moveright\VDMindent\hbox\bgroup
+ \setbox0=\hbox{$#1$\enspace::\enspace}%
+ \@makeColonActive\@changeLineSeparator
+ \advance\hsize by-\wd0 \box0
+ \@restoreMargins
+ %
+ % the \expandafters are necessary because TeX doesn't expand
+ % \halign specs when scanning for # and &
+ \vtop\bgroup\expandafter\halign\expandafter\bgroup
+ \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
+
+\def\endrecord{\crcr\egroup% closes halign
+ \egroup% closes vtop
+ \egroup% closes hbox
+ \ifInvEncountered@
+ \betweenRecordAndInvHook
+ \vskip\betweenRecordAndInvSkip
+ \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{%
+ \the\@invTokens}
+ \fi
+ \ifInitEncountered@
+ \betweenInvAndInitHook
+ \vskip\betweenInvAndInitSkip
+ \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{%
+ \the\@initTokens}
+ \fi
+ \par\postRecordHook
+ \vskip\postRecordSkip}
+
+\def\inv{\global\InvEncountered@true \global\@invTokens=}
+\def\init{\global\InitEncountered@true \global\@initTokens=}
+
+\newif\ifInvEncountered@
+\newif\ifInitEncountered@
+\newtoks\@invTokens
+\newtoks\@initTokens
+\def\betweenRecordAndInvHook{}
+\def\betweenInvAndInitHook{}
+\newskip\betweenRecordAndInvSkip
+ \betweenRecordAndInvSkip=0.5ex plus 0.2ex minus 0.1ex
+\newskip\betweenInvAndInitSkip
+ \betweenInvAndInitSkip=0.5ex plus 0.2ex minus 0.1ex
+
+% the user can decide on the exact alignment of the field names
+\newtoks\@recordAlign
+\def\leftRecord{\@recordAlign={$##$\hfil}}
+\def\rightRecord{\@recordAlign={\hfil$##$}}
+\rightRecord
+
+% more catcode trickery
+\def\defrecord{\bgroup\@makeColonActive\@defrecord}
+\def\@defrecord#1#2{\record{#1}#2\endrecord\egroup}
+
+\newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
+\newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
+\newcount\preRecordPenalty \preRecordPenalty=0
+\newcount\postRecordPenalty \postRecordPenalty=-100
+\def\preRecordHook{\penalty\preRecordPenalty }
+\def\postRecordHook{\penalty\postRecordPenalty }
+
+% \chg: mu function on composites
+\def\chg#1#2#3{\mu(#1,#2\mapsto#3)}
+
+%----------------------------------------------------------------
+%
+% Hooks
+%
+% hooked identifiers --- these are taken from the TeXbook, p.357, 359
+\def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
+ \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
+ \mkern-6mu \mathord\minus$} % p.357, \leftarrowfill
+
+\def\overleftharpoonup#1{{%
+ \boxmaxdepth=\maxdimen % this fixes Lamport's figures, but isn't necessary
+ % for versions after 15 Dec 87
+ \vbox{\ialign{##\crcr % p.359, \overleftarrow
+ \leftharpoonupfill\crcr\noalign{\kern-\p@\nointerlineskip}
+ $\hfil\displaystyle{#1}\hfil$\crcr}}}}
+
+\let\hook=\overleftharpoonup % c'est simple comme bonjour
+
+%-----------------------------------------------------------------
+%
+% General formula environment, a bit like \[ \] but is
+% indented to \VDMindent and will take \\
+%
+%
+\def\form#1{\formula #1\endformula}
+
+\def\formula{\par\preFormulaHook
+ \vskip\preFormulaSkip
+ \@beginVerticalVDM
+ \bgroup
+ \moveright\VDMindent\vtop\bgroup\@beginHorizontalVDM}
+\def\endformula{\@endHorizontalVDM\egroup % ends the vtop
+ \egroup % ends the overall group
+ \par\postFormulaHook
+ \vskip\postFormulaSkip}
+
+\newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
+\newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
+\newcount\preFormulaPenalty \preFormulaPenalty=0
+\newcount\postFormulaPenalty \postFormulaPenalty=-100
+\def\preFormulaHook{\penalty\preFormulaPenalty }
+\def\postFormulaHook{\penalty\postFormulaPenalty }
+
+%----------------------------------------------------------------
+%
+% Formula within a box, when width is unknown
+%
+% equivalent to \parbox[t]{\hsize}{\@beginHorizontalVDM
+% ...\@endHorizontalVDM}
+%
+\def\formbox{\vtop\bgroup\@beginHorizontalVDM}
+\def\endformbox{\strut\@endHorizontalVDM\egroup}
+
+%----------------------------------------------------------------
+%
+% special font for constants
+%
+\def\constantFont{\sc}
+\def\const#1{\hbox{\constantFont{#1}\/}}
+
+%----------------------------------------------------------------
+%
+% line break and indent
+%
+\def\T#1{\\\hbox to #1em{}}
+
+%----------------------------------------------------------------
+%
+% line break and push line after to RHS
+%
+\def\R{\\\hspace*{\fill}}
+
+%----------------------------------------------------------------
+%
+% Proofs
+%
+% a proof environment for typesetting proofs in the "natural
+% deduction" style.
+
+\newdimen\ProofIndent \ProofIndent=\VDMindent
+\newdimen\ProofNumberWidth \ProofNumberWidth=\parindent
+
+\def\proof{\par\preProofHook
+ \vskip\preProofSkip
+ \let\&=\@proofLine
+ \moveright\ProofIndent\vtop\bgroup
+ \@indentLevel=1
+ \advance\linewidth by-\ProofIndent
+ \begin{tabbing}%
+ \hbox to\ProofNumberWidth{}\=\kill} % template line
+\def\endproof{\end{tabbing}\advance\linewidth by\ProofIndent
+ \egroup % ends the \vtop
+ \par\postProofHook
+ \vskip\postProofSkip}
+
+\newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
+\newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex
+
+\newcount\preProofPenalty \preProofPenalty=-100
+\newcount\postProofPenalty \postProofPenalty=0
+\def\preProofHook{\penalty\preProofPenalty }
+\def\postProofHook{\penalty\postProofPenalty }
+
+\def\From{\@indentProof\kw{from }\=%
+ \global\advance\@indentLevel by 1
+ \@enterMathMode}
+\def\Infer{\global\advance\@indentLevel by-1
+ \@indentProof\kw{infer }\@enterMathMode}
+\def\@proofLine{\@indentProof\@enterMathMode}
+\def\by{\`}
+
+\newcount\@indentLevel
+\newcount\@indentCount
+\def\@indentProof{% do \>, \@indentLevel times
+ \global\@indentCount=\@indentLevel
+ \@gloop \>\global\advance\@indentCount by-1
+ \ifnum\@indentCount>0
+ \repeat}
+
+% need special loop macros that works in across boxes
+\def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
+\def\@giterate{\@body \global\let\@gloopNext=\@giterate
+ \else \global\let\@gloopNext=\relax \fi \@gloopNext}
+
+% this enters math mode and sets the LaTeX macros \@stopfield up
+% to exit math mode
+\def\@enterMathMode{\def\@stopfield{$\egroup}$}
+
+%----------------------------------------------------------------
+\def\VDMauthor{M.Wolczko,
+CS Dept.,
+Univ. of Manchester, UK.
+mario@cs.man.ac.uk
+uknet!man.cs!mario}
+
+\def\VDMversion{vdm3.0}
+
+\typeout{BSI VDM style option <9 Jun 1992>}
+%----------------------------------------------------------------
+%
+% Global changes
+%
+% All things that have to be invoked before the user's stuff appears
+% should go here.
+%
+% by default the math spacing and changes to @ and _ apply everywhere
+\@changeOtherMathcodes \@changeGlobalCatcodes
+%
+%-------------------the end--------------------------------------
+\endinput
+%
+% Summary of penalties
+%
+% Penalties in vertical mode
+%
+% \preOperationPenalty before an op begins
+% \preExternalPenalty between the header and externals of an op
+% \prePreConditionPenalty before the precondition
+% \prePostConditionPenalty before the postcondition
+% \postOperationPenalty at the end of an op
+%
+% \preFunctionPenalty before a fn begins
+% \betweenSignatureAndBodyPenalty -guess
+% \postFunctionPenalty after a fn ends
+%
+% \preRecordPenalty before a record
+% \postRecordPenalty after a record
+%
+% etc for formula, proof
+%
+% Penalties in horizontal mode in boxes
+%
+% \linepenalty 101 \@raggedRight
+% `if mm-exp ^ then..' 0 \SIf
+% `if ... then mm-exp ^ else' -100 \SIf
+% `let mm-exp in ^ ...' -100 \SLet
+% `map mm-exp ^ to ...' -50 \map
+% ^\iff -50 \iff
+% ^\implies -35 \implies
+% func(args) \DEF^ -100 \begin{fn}
+% \binoppenalty 10000
+% \relpenalty 10000
+% \hyphenpenalty -100 \suchthat
+% ^\to -100 \to
+% _^ 100 \@VDMunderscore
+%
diff --git a/macros/latex/contrib/vdm/vdm.tex b/macros/latex/contrib/vdm/vdm.tex
new file mode 100644
index 0000000000..ddce8336f3
--- /dev/null
+++ b/macros/latex/contrib/vdm/vdm.tex
@@ -0,0 +1,1562 @@
+%%% ====================================================================
+%%% @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}
+