From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Mon, 2 Sep 2019 13:46:59 +0900 Subject: Initial commit --- macros/latex/contrib/vdm/vdm.pdf | Bin 0 -> 197434 bytes macros/latex/contrib/vdm/vdm.sty | 1185 +++++++++++++++++++++++++++++ macros/latex/contrib/vdm/vdm.tex | 1562 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 2747 insertions(+) create mode 100644 macros/latex/contrib/vdm/vdm.pdf create mode 100644 macros/latex/contrib/vdm/vdm.sty create mode 100644 macros/latex/contrib/vdm/vdm.tex (limited to 'macros/latex/contrib/vdm') diff --git a/macros/latex/contrib/vdm/vdm.pdf b/macros/latex/contrib/vdm/vdm.pdf new file mode 100644 index 0000000000..4c66bbf1c2 Binary files /dev/null and b/macros/latex/contrib/vdm/vdm.pdf 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} + -- cgit v1.2.3