%%% ==================================================================== %%% @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 %