%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%$Id: vpp.sty,v 1.18 2006/03/15 23:56:40 vdmtools Exp $
% @(#)vpp.sty   1.4 (C++): LaTeX style for VDM++, (c) Cap Volmac 94/12/21
%
% Contact: afrodite@capints.uucp
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\typeout{VDM++ style option <00/07/19> version 1.6}
\RequirePackage{vdmsl-2e-nms}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Definition of VDM++ keywords.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\makeNewKeyword{\kAct}{\#act }
\makeNewKeyword{\kActive}{\#active }
\makeNewKeyword{\kAll}{all}
\makeNewKeyword{\kAssumption}{assumption }
\makeNewKeyword{\kClass}{class }
\makeNewKeyword{\kDel}{del }
\makeNewKeyword{\kDelay}{delay }
\makeNewKeyword{\kDuration}{duration }
\makeNewKeyword{\kCycles}{cycles }
\makeNewKeyword{\kEffect}{effect }
\makeNewKeyword{\kFin}{\#fin }
\makeNewKeyword{\kGeneral}{general }
\makeNewKeyword{\kInput}{input }
\makeNewKeyword{\kInstanceVarDef}{instance variables }
\makeNewKeyword{\kINYS}{is not yet specified}
\makeNewKeyword{\kISO}{is subclass of }
\makeNewKeyword{\kIsofbaseclass}{isofbaseclass}
\makeNewKeyword{\kIsofclass}{isofclass}
\makeNewKeyword{\kISR}{is subclass responsibility}
\makeNewKeyword{\kMutex}{mutex}
\makeNewKeyword{\kNew}{new}
\makeNewKeyword{\kObjectstate}{objectstate }
\makeNewKeyword{\kPer}{per }
\makeNewKeyword{\kPeriodic}{periodic }
\makeNewKeyword{\kReq}{\#req }
\makeNewKeyword{\kSamebaseclass}{samebaseclass}
\makeNewKeyword{\kSameclass}{sameclass}
\makeNewKeyword{\kSelf}{self}
\makeNewKeyword{\kStart}{start}
\makeNewKeyword{\kStartlist}{startlist }
\makeNewKeyword{\kSync}{sync }
\makeNewKeyword{\kTimePost}{time post }
\makeNewKeyword{\kThreadDef}{thread }
\makeNewKeyword{\kTopology}{topology}
\makeNewKeyword{\kWaiting}{\#waiting }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Redefinitions of macros/environments in vdmsl.sty that contain bugs or are
% not adequate to be used in vpp.sty.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%
% Redefinition of `\const' to ensure a proper treatment of '_'.
%

%Removed LTO \def\const#1{\hbox{$\ConstantFont #1$\/}}

%
% Redefinition of `\return'; it causes a lot of unwanted white space in
% some circumstances in its original version.
%

\def\return#1{\@expl@Def\kw@indent{return }\ifmmode#1\else$#1$\fi\sub@kw@indent{return }}

%
% Redefinition of `\inv' in vdmsl.sty to add some indentation when the 
% invariant follows a type definition.
%

\def\inv#1#2{\add@indent{\w@IIndent}\hspace{\w@IIndent}\invfn{#1}#2\ignorespaces\endinvfn\sub@indent{\w@IIndent}}
%
% Redefinition of the keyword `undefined' to avoid the generation of 
% undesired white space after the keyword.
%

\@mNK\Undefined{undefined}

%
% Redefinition of `\blockstmt'.
%

\def\@hardlf{\par\relax\leavevmode\lnout@oi}
\newdimen\@rbl\setbox\tmp@box=\hbox{$\strut(\strut$}\@rbl=\wd\tmp@box\relax
\def\blockstmt{\@expl@Def\add@indent{\w@IIndent}\add@indent{\@rbl}\Lp\ignorespaces\hspace{\w@IIndent}}
\def\endblockstmt{\ignorespaces\sub@indent{\w@IIndent}\sub@indent{\@rbl}\sub@indent{\@rbl}\\\Rp\ignorespaces\add@indent{\@rbl}}

%
% Redefinition of `\@compr@expr' to avoid generation of the (default) predicate
% `true' with the macros `\setcomp', `\seqcomp' and `\mapcomp'.
%

\def\@compr@expr#1#2]{\add@DI \ifx #2\printtrue\else\Dot\strut #1#2\fi\sub@DI\sub@DI\@rb@sb\endgroup}

%
% Redefinition of `\such' to avoid unnecessary generation of the default
% predicate `true' with the original macro. See also the section on known
% bugs in the manual. The old macro is available as `\@such'.
%

\let\@such=\such
\def\such#1#2{\ifx #2\printtrue{\@such{#1}}\else{\@such{#1}[#2]}\fi}

%
% Redefinition of def-statement (and def-expression) to reflect the current
% VDM-SL syntax.
%

\def\semicolonAM@bls{\ifmmode\semicolonIM@bls\else\semicolonMM@bls\fi}
\def\semicolonIM@bls{\let\M@bl@one=\@empty\let\M@bl@two=\@empty
  \let\F@bl@cl=\F@semicolon@linebr}
\def\semicolonMM@bls{\let\M@bl@one=$\let\M@bl@two=$%
  \let\F@bl@cl=\F@semicolon@pl}
\def\F@semicolon@pl{%
        \ifpunct@set@it@
                \global\punct@set@it@false
                \@par@linebr
        \else
                \ifFirst@ 
                        \global\First@false 
                \else
                        ;%
                        \@par@linebr
                \fi
        \fi}
\def\F@semicolon@linebr{%
        \ifpunct@set@it@
                \global\punct@set@it@false
                \@linebr
        \else
                \ifFirst@ 
                        \global\First@false 
                \else;%
                     \@linebr 
                \fi
        \fi}
\def\@defstmt{\def\@sep{=}\First@true\let\eqdef=\F@bls\semicolonAM@bls
  \kw@indent{def }\ignorespaces}
\def\enddefstmt{\sub@kw@indent{def }\ \kIn}
\def\defexpr{\defstmt}
\def\enddefexpr{\enddefstmt}

%
% Redefinition of `\Gmap'.
%

% ueki
%\def\Gmap{\buildrel m \over \To}
%\def\Gmap{\ \kw{to}\ }
% ueki

%
% Redefinition of `\ind@by' in vdmsl.sty to avoid generation of LaTeX code
% for `by 1' in index-for loops.
%

%\def\ind@by#1]{\ifnum#1=1\else{\kw@indent{by }#1\sub@kw@indent{by }}\fi$\@Do}

%
% Redefinition of `\pre' and `\post' in vdmsl.sty.
%

\def\pre#1{\ifx #1\printtrue\@ignorespaces\else\kw@indent{pre }\ifmmode#1\else$#1$\@ignorespaces\sub@kw@indent{pre }\\\fi\fi}
\def\post#1{\kw@indent{post
}\ifmmode#1\else$#1$\fi\@ignorespaces\sub@kw@indent{post }}

%
% Redefinition of `\endexceptions' in vdmsl.sty to add some indentation before
% the `[' of the enclosing topology or specification statement.
%

\def\endexceptions{\ \sub@kw@indent{errs }\@ignorespaces}

\def\@fnsemicolon{%
      \ifpunct@set@it@
           \global\punct@set@it@false
      \else
           \iffn@in@let@
                \@comma
           \else
                \@fncustomcolon
           \fi
      \fi}

\def\@fncustomcolon{%
        \ifpunct@set@it@
                \global\punct@set@it@false
        \else
                \ifDef@% 
                        \ifFirstDef@% 
                                \global\FirstDef@false%
                        \else%
                                ;%
                                \@linebr
                        \fi%
                \else% 
                        \vdm% 
                \fi
        \fi}              

\def\op{%
  \@fncustomcolon\let\e@parms=\e@op@parms
  \@ifoptarg{\@if@i@e{\@op}{\@op}}{\Implicit@true\@op}}

%
% redefinition of `\@@ext', `\@externals' and `\endexternals'.
%

\def\@@ext#1#2:#3\\{\F@linebr
  \hbox to \wi@wr{#1\hss}\add@indent\wi@wr
  \if#3''{\b@id@indent{}{#2}#3\e@id@indent}\else{\b@id@indent{:}{#2}#3\e@id@indent}\fi
  \sub@indent\wi@wr\@rd@wr}
\def\@externals{\kw@indent{ext }\First@true$\@rd@wr}
\def\endexternals{$\sub@kw@indent{ext }\\\@ignorespaces}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% New definitions.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%
% Class environment
%

\def\indinh#1{[#1]}
\@newSkips{Class}{2ex plus .5ex minus .3ex}{2ex plus .5ex minus .3ex}
\@emptyHooks{Class}
\def\class{\@ifoptarg\@class\@smplclass}
\def\@smplclass#1{
   \global\wi@indent=\z@
\def\endclass{\leavevmode\sub@indent{\w@Indent}\lnout@\\ \kEnd $#1$%
   \e@Macro\postClassHook\postClassSkip}
   \b@Macro\preClassSkip\preClassHook\lnout@m
   \kClass $#1$
   \add@indent{\w@Indent}\def\ei@module{\sub@indent{\w@Indent}}}
\def\@class#1]#2{
   \global\wi@indent=\z@
\def\endclass{\leavevmode\sub@indent{\w@Indent}\lnout@\\ \kEnd $#2$%
   \e@Macro\postClassHook\postClassSkip}
   \b@Macro\preClassSkip\preClassHook\lnout@m
   \kClass $#2$ \if{#1}{no}\else{\kISO }$#1$\fi
   \add@indent{\w@Indent}\def\ei@module{\sub@indent{\w@Indent}}}

%
% Inheritance
%

\@newSkips{InhDef}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\@emptyHooks{InhDef}
\def\inhdef{\@ifoptarg\@inhdef{\@inhdef\w@IIndent]}}
\def\@inhdef#1]{\Def@true\FirstDef@true
  \b@Kw@II{inherit}{\preInhDefSkip}{\preInhDefHook}{#1}}
\def\endinhdef{\e@Kw@II\postInhDefHook\postInhDefSkip}
\def\inherit#1#2{\@semicolon\@hardlf\kFrom #1$\Dcolon$ \ifx #2\all\kAll\@ignorespaces\else#2\fi}

%
% Instance variables
%

\@newSkips{InstVar}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\@emptyHooks{InstVar}
\def\instvar{\@ifoptarg{\@instvar}{\@instvar\w@IIndent]}}
\def\@instvar#1]{\Def@true\FirstDef@true
  \b@Kw@II{instance variables}\preInstVarSkip\preInstVarHook{#1}}
\def\endinstvar{\e@Kw@II\postInstVarHook\postInstVarSkip}
\@emptyHooks{VarDcl}
\@newSkips{VarDcl}{0ex}{0ex}
\def\vardcl{\b@vardcl \setw@id\@vardcl}
\def\@vardcl#1{\@iflinebr{\nl@vardcl{#1}}{\sl@vardcl{#1}}}
\def\sl@vardcl#1#2{\ifx \Inyd #2 \b@id@indent{}{#1}#2%
  \else \b@id@indent{:}{#1}#2\fi \e@id@indent \e@vardcl}
\def\nl@vardcl#1#2{%
  \ifx #2\Inyd #1\else#1 :\fi\add@DI\\#2\sub@DI\e@vardcl}
\def\b@vardcl{\begingroup \@semicolon \b@Macro\preVarDclSkip\preVarDclHook\lnout@oi $}
\def\e@vardcl{$\ifDef@ \postVarDclHook%
  \else \e@Macro\postVarDclHook\postVarDclSkip\fi\endgroup\ignorespaces}
\@emptyHooks{InstInit}
\@newSkips{InstInit}{0ex}{0ex}
\def\instinit{\b@instinit \setw@id\@instinit}
\def\@instinit#1{\@iflinebr{\nl@instinit{#1}}{\sl@instinit{#1}}}
\def\sl@instinit#1#2{\kInit \ifx\Inyd #2\b@id@indent{}{#1}#2%
  \else\b@id@indent{\Fdef}{#1}#2\fi \e@id@indent \e@instinit}
\def\nl@instinit#1#2{%
  \kInit \ifx #2\Inyd #1\else#1 \Fdef \fi\add@DI\\#2\sub@DI\e@instinit}
\def\b@instinit{\begingroup \@semicolon \b@Macro\preInstInitSkip\preInstInitHook\lnout@oi $}
\def\e@instinit{$\ifDef@ \postInstInitHook%
  \else \e@Macro\postInstInitHook\postInstInitSkip\fi\endgroup\ignorespaces}


%new instinv: VDM++ language adjustment 980903
\@emptyHooks{instInvfn}
\@newSkips{instInvfn}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\def\instinv#1{\instinvfn#1\endinstinvfn}
\def\instinvfn{%
  $\kw@indent{inv } }
\def\endinstinvfn{\sub@kw@indent{inv }$\@ignorespaces\@par@linebr%
}

\def\issubclassresp{\@expl@Def$\kw@indent{is subclass responsibility}\sub@kw@indent{is subclass responsibility}$}


%old instinv \@emptyHooks{InstInv}
%old instinv \@newSkips{InstInv}{0ex}{0ex}
%old instinv \def\instinv{\b@instinv \setw@id\@instinv}
%old instinv \def\@instinv#1{\@iflinebr{\nl@instinv{#1}}{\sl@instinv{#1}}}
%old instinv \def\sl@instinv#1#2{\kInv \ifx \Inyd #2 \b@id@indent{}{#1}#2%
%old instinv   \else \b@id@indent{\Fdef}{#1}#2\fi \e@id@indent \e@instinv}
%old instinv \def\nl@instinv#1#2{%
%old instinv   \kInv \ifx #2\Inyd #1\else#1 \Fdef \fi\add@DI\\#2\sub@DI\e@instinv}
%old instinv \def\b@instinv{\begingroup \@semicolon \b@Macro\preInstInvSkip\preInstInvHook\lnout@oi $}
%old instinv \def\e@instinv{$\ifDef@ \postInstInvHook%
%old instinv   \else \e@Macro\postInstInvHook\postInstInvSkip\fi\endgroup\ignorespaces}
%old instinv 


%
% Method environment
%

\@newSkips{MethDef}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\@emptyHooks{MethDef}
\def\methdef{\@ifoptarg\@methdef{\@methdef\w@IIndent]}}
\def\@methdef#1]{\Def@true\FirstDef@true
\global\First@true%
  \b@Kw@II{methods}{\preMethDefSkip}{\preMethDefHook}{#1}}
\def\endmethdef{\e@Kw@II\postMethDefHook\postMethDefSkip}

%
% Methods
%

\def\methvalue#1{\ \kValue\ifmmode#1\else$#1$\fi}
\@newSkips{Method}{0ex}{0ex}
\@emptyHooks{Method}
\newtoks\t@fnop@name
\newif\ifSignatured@            \Signatured@false
\newif\ifImplicit@              
\newif\ifSignature@             \Signature@false
\def\method{\op}
\def\endmethod{\endop}

%
% Preliminary method definition; definition of `\Inys' and `\Iscr'.
%

\def\Inys{\kINYS}
\def\Iscr{\kISR}

%
% VDM++ dedicated expressions; definition of `\isofclass', `\isofbaseclass',
% `\sameclass' and `\samebaseclass'.
%

\def\isofclass#1#2{\expex{\kIsofclass}{#1, #2}}
\def\isofbaseclass#1#2{\expex{\kIsofbaseclass}{#1, #2}}
\def\sameclass#1#2{\expex{\kSameclass}{#1, #2}}
\def\samebaseclass#1#2{\expex{\kSamebaseclass}{#1, #2}}

%
% Specification statement; definition of the `specification' environment.
%

\newdimen\@sbl\setbox\tmp@box=\hbox{$\strut[\strut$} \@sbl=\wd\tmp@box\relax
\def\specification{\@expl@Def\add@indent{\@sbl}\add@indent{\@sbl}[}
\def\endspecification{\@ignorespaces\sub@indent{\@sbl}\sub@indent{\@sbl}]}

%
% Topology statement; definition of the `topology' environment.
%

\newdimen\@topology\setbox\tmp@box=\hbox{$\strut\kTopology\ \strut$}\@topology=\wd\tmp@box\relax
\def\topology{\@expl@Def\add@indent{\@topology}\kTopology}
\def\endtopology{\@ignorespaces\sub@indent{\@topology}}

%
% Method invocation; definition of `\invoke'.
%

\def\invoke#1#2{\ifx{#1}{self}\kSelf \else\ifmmode#1\else$#1$\fi\fi%
!%
\ifx{#2}{new}\kNew \else\ifx{#2}{start}\kStart \else\ifmmode#2\else$#2$\fi\fi\fi}

%
% Definition `\self'.
%

\def\self{\kSelf}

\def\mutex#1{\@hardlf\kMutex($#1$)}

%
% New expression; definition `\new'.
%

%\def\new#1{{\kNew{\kw{ }}#1 ()}}
% ueki
%\def\new#1{{\kNew{\kw{ }}#1 }} % modify for Constructors. They have arguments.
\def\new#1{{\kNew{\kw{\ }}#1 }} % modify for Constructors. They have arguments.
% ueki

%
% Start statement; definition of `\start'.
%

\def\start#1{{\kStart}(#1)}

%
% Startlist statement; definition `\startlist'.
%

\def\startlist#1{\kStartlist $#1$}

%
% Delay statement; definition `\delay'.
%

\def\delay#1{\kDelay ($#1$)}

%
% Duration statement; definition `\duration'.
%

\def\duration#1#2{\kDuration ($#1$) #2}

%
% Cycles statement; definition `\cycles'.
%

\def\cycles#1#2{\kCycles ($#1$) #2}

%
% Synchronisation constraints; definition of `syncdef' environment.
%

\@newSkips{SyncDef}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\@emptyHooks{SyncDef}
\def\syncdef{\@ifoptarg\@syncdef{\@syncdef\w@IIndent]}}
\def\@syncdef#1]{\Def@true\FirstDef@true
  \b@Kw@II{sync}{\preSyncDefSkip}{\preSyncDefHook}{#1}}
\def\endsyncdef{\e@Kw@II\postSyncDefHook\postSyncDefSkip}

%
% Permission predicate; definitions of `\per', `\act', `\active', `\fin',
% `\req' and `\waiting'.
%

\def\per#1#2{\@hardlf\kPer $#1 \Implies #2$}
\def\act#1{\expex{\kAct}{#1}}
\def\actminusfin#1{\expex{\kActive}{#1}}
\def\fin#1{\expex{\kFin}{#1}}
\def\req#1{\expex{\kReq}{#1}}
\def\reqminusact#1{\expex{\kWaiting}{#1}}

%
% Threads; definition of `threaddef' and 'thread' environments.
%

\@newSkips{Thread}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\@emptyHooks{Thread}
\def\threaddef{\@ifoptarg{\@threaddef}{\@threaddef\w@IIndent]}}
\def\@threaddef#1]{\Def@true\FirstDef@true
 \b@Kw@II{thread}{\preThreadSkip}{\preThreadHook}{#1}}
\def\endthreaddef{\e@Kw@II\postThreadHook\postThreadSkip}

\@newSkips{Thread}{2ex plus .4ex minus .2ex}{2ex plus .4ex minus .2ex}
\@emptyHooks{Thread}
\def\thread{\@ifoptarg{\@thread}{\@thread{0ex}]}}
\def\@thread#1]{
  \add@indent{#1}\relax
  \def\endthread{\sub@indent{#1}\e@Macro\postThreadHook\postThreadSkip}
  \parindent=\z@ \let\par=\@@par%
  \vdm%
  \b@Macro\preThreadSkip\preThreadHook\lnout@
  \ignorespaces}

%
% Periodic obligation; definition of `\periodic'.
%

%\def\periodic#1#2{\F@comma\@linebr\kPeriodic \pex{#1}\pex{#2}}
\def\periodic#1#2{\@hardlf\kPeriodic \pex{#1}\pex{#2}\@linebr}

%
% Real-time
%

\@newSkips{TimePost}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\@emptyHooks{TimePost}
\@newSkips{TimeVar}{1ex plus .3ex minus .2ex}{1.75ex plus .4ex minus .2ex}
\@emptyHooks{TimeVar}
\def\timepost#1{\kw@indent{time post }\ifmmode#1\else$#1$\fi\@ignorespaces\sub@kw@indent{time post }}
\def\Approx{\approx}
\def\timevar{\@ifoptarg{\@timevar}{\@timevar\w@IIndent]}}
\def\@timevar#1]{\Def@true\FirstDef@true
  \b@Kw@II{time variables}\preTimeVarSkip\preTimeVarHook{#1}}
\def\endtimevar{\e@Kw@II\postTimeVarHook\postTimeVarSkip}
\@emptyHooks{TimeVarDcl}
\@newSkips{TimeVarDcl}{0ex}{0ex}
\def\timevardcl{\b@timevardcl \setw@id\@timevardcl}
\def\@timevardcl#1{\@iflinebr{\nl@timevardcl{#1}}{\sl@timevardcl{#1}}}
\def\sl@timevardcl#1#2{\ifx \Inyd #2 \b@id@indent{}{#1}#2%
  \else \b@id@indent{:}{#1}#2\fi \e@id@indent \e@timevardcl}
\def\nl@timevardcl#1#2{%
  \ifx #2\Inyd #1\else#1 :\fi\add@DI\\#2\sub@DI\e@timevardcl}
\def\b@timevardcl{\begingroup \@semicolon \b@Macro\preTimeVarDclSkip\preTimeVarDclHook\lnout@oi $}
\def\e@timevardcl{$\ifDef@ \postTimeVarDclHook%
  \else \e@Macro\postTimeVarDclHook\postTimeVarDclSkip\fi\endgroup\ignorespaces}
\@emptyHooks{Assumption}
\@newSkips{Assumption}{0ex}{0ex}
\def\assumption{\b@assumption \setw@id\@assumption}
\def\@assumption#1{\@iflinebr{\nl@assumption{#1}}{\sl@assumption{#1}}}
\def\sl@assumption#1#2{\kAssumption \ifx\Inyd #2\b@id@indent{}{#1}#2%
  \else\b@id@indent{\Fdef}{#1}#2\fi \e@id@indent \e@assumption}
\def\nl@assumption#1#2{%
  \kAssumption \ifx #2\Inyd #1\else#1 \Fdef \fi\add@DI\\#2\sub@DI\e@assumption}
\def\b@assumption{\begingroup \@semicolon \b@Macro\preAssumptionSkip\preAssumptionHook\lnout@oi $}
\def\e@assumption{$\ifDef@ \postAssumptionHook%
  \else \e@Macro\postAssumptionHook\postAssumptionSkip\fi\endgroup\ignorespaces}
\@emptyHooks{Effect}
\@newSkips{Effect}{0ex}{0ex}
\def\effect{\b@effect \setw@id\@effect}
\def\@effect#1{\@iflinebr{\nl@effect{#1}}{\sl@effect{#1}}}
\def\sl@effect#1#2{\kEffect \ifx \Inyd #2 \b@id@indent{}{#1}#2%
  \else \b@id@indent{\Fdef}{#1}#2\fi \e@id@indent \e@effect}
\def\nl@effect#1#2{%
  \kEffect \ifx #2\Inyd #1\else#1 \Fdef \fi\add@DI\\#2\sub@DI\e@effect}
\def\b@effect{\begingroup \@semicolon \b@Macro\preEffectSkip\preEffectHook\lnout@oi $}
\def\e@effect{$\ifDef@ \postEffectHook%
  \else \e@Macro\postEffectHook\postEffectSkip\fi\endgroup\ignorespaces}

%
% Definition of `\name', `\charlit' and `\textlit'.
%

% removed by LTO
%\catcode`\_=13
%\def_{\sb}
%\def\name{\hbox\bgroup\def_{\_}\@name}
%\def\@name#1{\ifmmode#1\else$#1$\@ignorespaces\fi\egroup}
%\def\charlit{\hbox\bgroup\def_{\_}\@charlit}
%\def\@charlit#1{\Quote{\MathTextFont#1\/}\Quote\egroup}
%\def\textlit{\hbox\bgroup\def_{\_}\@textlit}
%\def\@textlit#1{\Dquote{\MathTextFont#1\/}\Dquote\egroup}

%
% Definition of `\printtrue' and `\printfalse' to correctly print the boolean
% literals true and false.
%

\def\printtrue{\True}
\def\printfalse{\False}

%
% Definition of `\Tto' (symbol to indicate total function types).
%

\def\Tto{\stackrel{t}{\To}}

%
% Default values
%

\setlength{\preAssumptionSkip}{0ex}
\setlength{\postAssumptionSkip}{2ex}
\setlength{\preClassSkip}{2ex}
\setlength{\postClassSkip}{2ex}
\setlength{\preEffectSkip}{0ex}
\setlength{\postEffectSkip}{2ex}
\setlength{\preInhDefSkip}{2ex}
\setlength{\postInhDefSkip}{0ex}
\setlength{\preValuesdefSkip}{2ex}
\setlength{\postValuesdefSkip}{0ex}
\setlength{\preValueSkip}{0ex}
\setlength{\postValueSkip}{0ex}
\setlength{\preTypesdefSkip}{2ex}
\setlength{\postTypesdefSkip}{0ex}
\setlength{\preTypeSkip}{0ex}
\setlength{\postTypeSkip}{0ex}
\setlength{\preInstVarSkip}{2ex}
\setlength{\postInstVarSkip}{0ex}
\setlength{\preInvfnSkip}{0ex}
\setlength{\postInvfnSkip}{0ex}
\setlength{\preInitfnSkip}{2ex}
\setlength{\preMethDefSkip}{2ex}
\setlength{\postMethDefSkip}{0ex}
\setlength{\preMethodSkip}{0ex}
\setlength{\postMethodSkip}{0ex}
\setlength{\preOperdefSkip}{2ex}
\setlength{\postOperdefSkip}{0ex}
\setlength{\preOpSkip}{0ex}
\setlength{\postOpSkip}{0ex}
\setlength{\preSyncDefSkip}{2ex}
\setlength{\postSyncDefSkip}{0ex}
\setlength{\preThreadSkip}{2ex}
\setlength{\postThreadSkip}{0ex}
\setlength{\preFuncdefSkip}{2ex}
\setlength{\postFuncdefSkip}{0ex}
\setlength{\preFnSkip}{0ex}
\setlength{\postFnSkip}{0ex}
\setlength{\prePrecondSkip}{0ex}
\setlength{\prePostcondSkip}{0ex}
\setlength{\preTimePostSkip}{0ex}
\setlength{\postTimePostSkip}{0ex}
\setlength{\preTimeVarSkip}{2ex}
\setlength{\postTimeVarSkip}{0ex}
\setlength{\preTimeVarDclSkip}{0ex}
\setlength{\postTimeVarDclSkip}{0ex}
\setlength{\postSignatureSkip}{0ex}
\setlength{\preExceptionsSkip}{0ex}
\nolinenumbering

%
% Instance variables assigndef
%
\def\F@semicolon@pl{%
        \ifpunct@set@it@
                \global\punct@set@it@false
                \@par@linebr
        \else
                \ifFirst@ 
                        \global\First@false 
                \else
                        ;%
                        \@par@linebr
                \fi
        \fi}

\def\parlinebr{\@par@linebr}

\def\insvar{\@expl@Def\setw@bl{\@insvar}}
\def\endinsvar{;\@par@linebr}
\def\@insvar{\First@true\def\@sep{:}\MM@bls
  \ignorespaces}

\def\instinit#1{\F@semicolon@pl\t@bl@one={#1}$\@iflinebr{\ml@instinit}{\sl@instinit}}
\def\sl@instinit#1{\let\ei@instinit=\e@bl\b@bl#1\add@DI
  \@iflinebrarg{\Ass\\\arg@instinit}{\e@instinit}{\Ass\arg@instinit}{\e@instinit}}
\def\ml@instinit#1{\m@bl\add@DI\let\ei@instinit=\sub@DI\\#1\add@DI
  \@iflinebrarg{\Ass\\\arg@instinit}{\e@instinit}{\Ass\arg@instinit}{\e@instinit}}
\def\arg@instinit#1]{#1\e@instinit}
\def\e@instinit{\ei@instinit\sub@DI$\ignorespaces}