summaryrefslogtreecommitdiff
path: root/obsolete/macros/latex209/contrib/vdm/vdm.sty
diff options
context:
space:
mode:
Diffstat (limited to 'obsolete/macros/latex209/contrib/vdm/vdm.sty')
-rw-r--r--obsolete/macros/latex209/contrib/vdm/vdm.sty1413
1 files changed, 1413 insertions, 0 deletions
diff --git a/obsolete/macros/latex209/contrib/vdm/vdm.sty b/obsolete/macros/latex209/contrib/vdm/vdm.sty
new file mode 100644
index 0000000000..f0cdd35731
--- /dev/null
+++ b/obsolete/macros/latex209/contrib/vdm/vdm.sty
@@ -0,0 +1,1413 @@
+%%% ====================================================================
+%%% @LaTeX-style-file{
+%%% author = "Mario Wolczko",
+%%% version = "3.01",
+%%% date = "21 May 1992",
+%%% time = "21:05:48 BST",
+%%% filename = "vdm.sty",
+%%% address = "Dept of Computer Science
+%%% The University of Manchester
+%%% Oxford Road
+%%% Manchester M13 9PL
+%%% UK",
+%%% telephone = "+44-61-275-6146",
+%%% FAX = "+44-61-275-6236",
+%%% checksum = "32169 1413 3689 43831",
+%%% email = "mario@cs.man.ac.uk (Internet)",
+%%% codetable = "ISO/ASCII",
+%%% keywords = "LaTeX, VDM specification language",
+%%% supported = "yes",
+%%% docstring = "LaTeX macros for typesetting VDM
+%%% specifications.",
+%%% }
+%%% ====================================================================
+%
+% BSI VDM documentstyle option for LaTeX
+%
+% M. Wolczko
+%
+% Last edited: Thu May 21 21:05:52 1992 by mario (Mario Wolczko) on madarch
+%
+% 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)
+%
+% Can use either the AMS ms[ab]m fonts or the MoreMath font if
+% available: follow the instructions near the string FONT-CUSTOMIZING.
+%
+%
+%
+%----------------------------------------------------------------
+%
+% Installation-dependent features
+%
+\let\vdm\relax % signal to ps-amsfonts
+
+\newif\ifams@% use AMS fonts?
+\newif\ifps@ % PostScript-based?
+\newif\ifmoremath@ % use MoreMath font?
+\newif\ifnfss@ % NFSS?
+
+% NFSS code is enabled if \selectfont is defined;
+% this is the usual test for the nfss.
+\ifx\selectfont\@undefined
+ \global\nfss@false
+\else
+ \global\nfss@true
+\fi
+
+\ifnfss@
+ % This is a patch for an NFSS bug, from Frank Mittelbach.
+ % It applies to the versions of lfonts.new of NFSS up to
+ %\def\fileversion{v1.3a}
+ %\def\filedate{91/11/27}
+ %\def\docdate {90/01/28}
+
+ \def\extract@alph@from@version#1#2{%
+ % #1 = alph id (cs)
+ % #2 = version (string)
+ \expandafter\extract@alph@from@version@\expandafter
+ #1\csname mv@#2\endcsname}
+
+ \def\extract@alph@from@version@#1#2{%
+ % #1 = alph id (cs)
+ % #2 = version (cs)
+ \def\extract@help##1\gdef#1##2##3\@nil{%
+ \def\@tempa####1{\gdef#2{##1####1##3}}%
+ \def\content@part{##2}}%
+ \expandafter\extract@help#2\@nil
+ \def\extract@group@no@etc\select@group#1##1##2##3\@nil{%
+ % ##1 group no
+ % ##2 extra part
+ % ##3 fam/ser/sha
+ \@tempa{%
+ \getanddefine@fonts{##1}##3%
+ \gdef#1{\use@mathgroup##2{##1}}}}%
+ \expandafter\extract@group@no@etc\content@part\@nil}
+
+ \def\select@group#1#2#3#4{\relax \ifmmode
+ \begingroup
+ \let \math@fonts \@empty
+ \escapechar \m@ne
+ \getanddefine@fonts #2#4%
+ \globaldefs \@ne
+ \math@fonts
+ \endgroup
+ \gdef #1{\use@mathgroup #3{#2}}%
+ \expandafter\extract@alph@from@version
+ \expandafter#1\expandafter{\math@version}%
+ \expandafter #1\fi }
+\fi
+
+\def\@fmtname{lplain}
+\def\@psfmtname{pslplain}
+
+\def\@testcmsy{\if@usecmsy \else
+ \@latexerr{Can't use vdm with this PSLaTeX}%
+ {This PSLaTeX does not have the CMSY symbols
+ available, and cannot be used with VDM style. Get
+ a guru to rebuild PSLaTeX with the CMSY and CMMI
+ fonts included.}\fi}
+\def\@testcmmi{\if@usecmmi \else
+ \@latexerr{Can't use vdm with this PSLaTeX}%
+ {This PSLaTeX does not have the CMMI symbols
+ available, and cannot be used with VDM style. Get
+ a guru to rebuild PSLaTeX with the CMSY and CMMI
+ fonts included.}\fi}
+
+\global\ps@false
+\ifx\fmtname\@psfmtname
+ \global\ps@true \@testcmsy \@testcmmi
+\fi
+
+
+
+% FONT-CUSTOMIZING
+% Decide under which conditions, you want to use which fonts.
+% You need to set either ams@true or ams@false, and either moremath@true or
+% moremath@false.
+% If in doubt, set both to false.
+
+% This uses moremath if pslatex/NFSS is in use , AMS fonts otherwise.
+\global\moremath@false \global\ams@true
+\ifps@
+ \ifnfss@ \global\moremath@true \global\ams@false \fi
+\else\ifx\fmtname\@fmtname
+\else \global\ams@false % don't use AMS for SliTeX
+\fi\fi
+
+\ifnfss@
+ \ifams@
+ % Firstly we call amsfonts.sty to load the AMS fonts for us.
+ \ifps@
+ \input ps-amsfonts.sty
+ \else
+ \input amsfonts.sty
+ \fi
+ \edef\msx@{\hexnumber@\msa@group}
+ \edef\msy@{\hexnumber@\msb@group}
+ \else\ifmoremath@
+ \new@mathgroup\mm@group
+ \define@mathgroup\mv@normal\mm@group{mm}{m}{n}
+ \edef\mm@{\hexnumber@\mm@group}
+ % FONT-CUSTOMIZING
+ % substitute correct name of MoreMath font here
+ \new@fontshape{mm}{m}{n}{%
+ <5>pmmr at5pt%
+ <6>pmmr at6pt%
+ <7>pmmr at7pt%
+ <8>pmmr at8pt%
+ <9>pmmr at9pt%
+ <10>pmmr at10pt%
+ <11>pmmr at10.95pt%
+ <12>pmmr at12pt%
+ <14>pmmr at14.4pt%
+ <17>pmmr at17.28pt%
+ <20>pmmr at20.74pt%
+ <25>pmmr at24.88pt}{}
+ \extra@def{mm}{}{}
+ \fi\fi
+ % \itfam is only defined if oldlfonts is in force, so if it is not defined,
+ % define it.
+ \ifx\itfam\@undefined
+ \new@mathgroup\itfam
+ \ifps@
+ \new@internalmathalphabet\mathit\itfam{times}{m}{it}
+ \else
+ \new@internalmathalphabet\mathit\itfam{cmr}{m}{it}
+ \fi
+ \fi
+ \ifx\math@bgroup\@empty
+ % nomargid synatax, \mathit will just switch the \fam if the font is
+ % already loaded, but will load the font the first time.
+ \def\vdm@it{\mathit}
+ \else
+ % margid syntax, as for nomargid, but here the scope of \mathit is its
+ % argument, so we call it with a null argument to make sure the font is
+ % loaded, then switch \fam in the old way.
+ \def\vdm@it{\mathit{}\fam\itfam}
+ \fi
+\else
+ \ifams@
+ % kludges for \newfam necessary because it's \outer
+ \csname newfam\endcsname\msxfam
+ \csname newfam\endcsname\msyfam
+
+ % this is lifted from amssymbols.sty
+ \ifcase\@ptsize
+ \font\tenmsx=msam10
+ \font\sevenmsx=msam7
+ \font\fivemsx=msam5
+ \font\tenmsy=msbm10
+ \font\sevenmsy=msbm7
+ \font\fivemsy=msbm5
+ \or
+ \font\tenmsx=msam10 scaled \magstephalf
+ \font\sevenmsx=msam8
+ \font\fivemsx=msam5 scaled \magstephalf
+ \font\tenmsy=msbm10 scaled \magstephalf
+ \font\sevenmsy=msbm8
+ \font\fivemsy=msbm5 scaled \magstephalf
+ \or
+ \font\tenmsx=msam10 scaled \magstep1
+ \font\sevenmsx=msam8
+ \font\fivemsx=msam5 scaled \magstephalf
+ \font\tenmsy=msbm10 scaled \magstep1
+ \font\sevenmsy=msbm8
+ \font\fivemsy=msbm5 scaled \magstephalf
+ \fi
+
+ \textfont\msxfam=\tenmsx \scriptfont\msxfam=\sevenmsx
+ \scriptscriptfont\msxfam=\fivemsx
+ \textfont\msyfam=\tenmsy \scriptfont\msyfam=\sevenmsy
+ \scriptscriptfont\msyfam=\fivemsy
+
+ \def\hexnumber@#1{\ifnum#1<10 \number#1\else
+ \ifnum#1=10 A\else\ifnum#1=11 B\else\ifnum#1=12 C\else
+ \ifnum#1=13 D\else\ifnum#1=14 E\else
+ \ifnum#1=15 F\fi\fi\fi\fi\fi\fi\fi}
+ \def\msx@{\hexnumber@\msxfam}
+ \def\msy@{\hexnumber@\msyfam}
+ \else\ifmoremath@
+ \csname newfam\endcsname\mmfam
+ \edef\mm@{\hexnumber@\mmfam}
+ \else\fi
+ \fi
+ % NFSS-change
+ % The previous version placed \fam\itfam in \everymath to get text italic
+ % in math mode. This does not work if this font has not yet been loaded.
+ % With oldlatex, most text italic sizes are preloaded, but \huge\it may not
+ % be.
+ % With the nfss, things may be set up so almost no fonts are preloaded.
+ % we will put \vdm@it into \everymath later, here we give the definition
+ % for oldlatex, \fam\itfam as before.
+ \def\vdm@it{\fam\itfam}
+\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}
+\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
+
+% If the user really wants the normal codes, she can call \defaultMathcodes
+\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
+\ifps@
+ \def\@changeOtherMathcodes{\mathcode`\:="603A \textminus
+ \mathcode`\|="327C \mathchardef\Or="32DA % this is a rel to get 5mu spacing
+ \mathcode`\f="0166} % normal letter spacing
+\else
+ % 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
+\fi
+
+% 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 \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
+ \catcode`\"=\active \let"=\@mathText}
+ \gdef\underscoreoff{% make _ a normal char
+ \catcode`\_=\active \let_=\@VDMunderscore}
+ \gdef\underscoreon{% restore underscore to usual meaning
+ \catcode`\_=8}
+ \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
+
+\ifnfss@
+ \def\mathTextFont{\mathrm}
+\else
+ \def\mathTextFont{\rm}
+\fi
+%----------------------------------------------------------------
+%
+% 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@
+ \mathchardef\Bool="0\msy@42 % Booleans
+ \mathchardef\Nat="0\msy@4E % Natural numbers
+ \def\Nati{\Nat_1} % Positive natural numbers
+ \mathchardef\Int="0\msy@5A % Integers
+ \mathchardef\Real="0\msy@52 % Reals
+ \mathchardef\Rat="0\msy@51 % Rationals
+\else\ifmoremath@
+ \mathchardef\Bool="0\mm@42 % Booleans
+ \mathchardef\Nat="0\mm@4E % Natural numbers
+ \def\Nati{\Nat_1} % Positive natural numbers
+ \mathchardef\Int="0\mm@5A % Integers
+ \mathchardef\Real="0\mm@52 % Reals
+ \mathchardef\Rat="0\mm@51 % Rationals
+\else
+ \def\Bool{\hbox{\bf B\/}}
+ \def\Nat{\hbox{\bf N\/}}
+ \def\Nati{\hbox{$\hbox{\bf N}_1$}}
+ \def\Int{\hbox{\bf Z\/}}
+ \def\Real{\hbox{\bf R\/}}
+ \def\Rat{\hbox{\bf Q\/}}
+\fi\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
+\ifps@
+ \def\DEF{\raise.5ex
+ \hbox{\footnotesize\underline{$\mathchar"3\cmsy@34$}}}% a \triangle
+\else
+ \def\DEF{\raise.5ex
+ \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle
+\fi
+
+% 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
+%
+\ifps@
+ \mathchardef\Exists="0224
+ \mathchardef\Forall="0222
+ \mathchardef\suchthat="22D7
+\else
+ \mathchardef\Exists="0239
+ \mathchardef\Forall="0238
+ \mathchardef\suchthat="2201
+\fi
+\def\exists{\@ifstar{\@splitExists}{\@normalExists}}
+\ifams@
+ \mathchardef\@nexists="0\msy@40 % crossed out existential quantifier
+\else\ifps@
+ \def\@nexists{\hbox to 0pt{\kern0.2ex\raise0.1ex\hbox{/}\hss}\Exists}
+\else
+ \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
+\fi\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)
+\ifmoremath@
+ \def\term#1{\thinspace\mathchar"4\mm@ D2\relax#1\mathchar"5\mm@ D4\thinspace}
+\else
+ \def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
+\fi
+% 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
+\ifps@
+ \mathchardef\minus="222D
+\else
+ \mathchardef\minus="2200
+\fi
+\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}
+
+\ifmoremath@
+ \mathchardef\dres="2\mm@ B2
+ \mathchardef\rres="2\mm@ B3 % the right hand version
+\else
+ \let\dres=\lhd
+ \let\rres=\rhd
+\fi
+
+% domain subtraction
+\ifmoremath@
+ \mathchardef\dsub="2\mm@ F8
+% what a horror -- some people will insist on these daft symbols...
+\else\ifps@
+ \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-3mu\hbox{$\dres$}$}}}
+\else
+ \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
+ \lower.1ex\hbox{$\dres$}$}}}
+\fi\fi
+
+% range subtraction
+\ifmoremath@
+ \mathchardef\rsub="2\mm@ F9
+\else\ifps@
+ \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu\rres$}}}
+\else
+ \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
+ \lower.1ex\hbox{$\rres$}$}}}
+\fi\fi
+
+\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
+\ifmoremath@
+ \mathchardef\sconc="2\mm@63
+\else\ifams@
+ \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\mathchar"2\msy@79$}}}}
+\else
+ % this is truly yukky
+ \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
+ \raise0.2ex\hbox{\it\char"12}}}}
+\fi\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
+\ifps@
+ \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
+ \cleaders\hbox{$\mkern-2mu \mathchar"0\cmsy@00 \mkern-2mu$}\hfill
+ \mkern-6mu \mathchar"0\cmsy@00$} % p.357, \leftarrowfill
+\else
+ \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
+ \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
+ \mkern-6mu \mathord\minus$} % p.357, \leftarrowfill
+\fi
+\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 <1 May 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
+%