diff options
Diffstat (limited to 'macros/generic/tex-ewd/dotnot.tex')
-rw-r--r-- | macros/generic/tex-ewd/dotnot.tex | 182 |
1 files changed, 182 insertions, 0 deletions
diff --git a/macros/generic/tex-ewd/dotnot.tex b/macros/generic/tex-ewd/dotnot.tex new file mode 100644 index 0000000000..24031e2a42 --- /dev/null +++ b/macros/generic/tex-ewd/dotnot.tex @@ -0,0 +1,182 @@ +% These macros are based on plain TeX. Use them to typeset +% calculational proofs and programs written in what Dijkstra called ``dot +% notation''. Dijkstra described the proof format in EWD 1300 and +% the programming language in ``A Discipline of Programming''. +% Don't hesitate to contact me: +% Wolfgang Helbig helbig@lehre.ba-stuttgart.de +% Stauferstr. 22 http://wwwlehre.ba-stuttgart.de/~helbig +% 71334 Waiblingen November 2008 + +% Sets and quantified operators +% The first two parameters are delimited by `: ', they provide the +% the quantifier and the range. The last parameter defines the term. +% It is delimited by `\>'. If the range is empty, the two colons will not +% be separated by space. The quantifier may be empty to give you a set. + +\def\<#1: #2: #3\>{\langle #1\;:\if#2\empty\else\;#2\;\fi:\;#3\rangle} +\let\mx\uparrow % maximum +\let\mn\downarrow % minimum +\let\fa\forall % universal quantifier +\let\ex\exists % existential quantifier +\let\su\Sigma % sum +\def\nbr{\#} % number of + +% Space surrounding binary operators. +% The lower the precedence of a operator the more space should surround it. +% Plain TeX provides \qquad = 36u; \quad = 18u; \; = 5u; \> = 4u; \, = 3u; +% \!=-3u where one u is em/18. + +% logical operators (use mxx for operator xx surrounded by space) +\let\eq\equiv +\def\meq{\qquad\eq\qquad} % equivalence surrounded by 36u +\let\ff\Leftarrow % "follows from" +\def\mff{\quad\ff\quad} % "follows from" surrounded by 18u +\let\impl\Rightarrow +\def\mimpl{\quad\impl\quad} % "implies" surrounded by 18u +\let\and\land +\def\mand{\;\,\and\;\,} % "and" surrounded by 9u +%\let\or\lor +\def\mor{\;\,\lor\;\,} % "or" surrounded by by 9u + +% For most arithmetic operators, we use what plain TeX provides, namely +% mathrel is surrounded by 5u space (see p. 170 in The TeXbook) +% mathbin is surrounded by 4u space +% mathpunct is followed by 3u space + +% Plain TeXs classification needs some correction however. +% ``\mathcode "cfpp'' encodes class, font family and position in the font. +% Plain TeX treats '*' as a bin operator, we need it as an ordinary symbol. +\mathcode`\*="0203 % class was 2 (binary) + +% Plain TeX treats ':' as a rel operator, we need it as an ordinary symbol. +\mathcode`\:="003A % class was 3 (relation) + +% \div and \mod should be surrounded by very little space, since +% they have a high precedence +\def\halfthinneg{\mskip-.5\thinmuskip} +\def\div{\mathbin{\halfthinneg\hbox{\bf div}\halfthinneg}} +\def\mod{\mathbin{\halfthinneg\hbox{\bf mod}\halfthinneg}} +\def\gcd{\hbox{\bf gcd}} + +% Indented formulas and proofs +% A proof is a succession of formula lines and hint lines. + +% A formula line has one parameter which is deliminated by \\ +% Use as `\f formula \\' +\def\f#1\\{\tabalign&&$#1$\cr} % like `\f E=mc^2\\' + +% A hint line has two parameters, a relational operator and a hint. +% Use as `\h\eq {hint why the relation holds}' +\def\h#1#2{\tabalign&$#1$&&$\{\,$#2$\,\}$\cr} % hint line +\def\heq#1{\h\eq {#1}} % Abbreviation for `\h\eq {easily seen}' + +% A named formula has two parameters: The name, deliminated by +% `:' and the formula, deliminated by `\\'. +% Use as `\nf R1: formula \\' +\def\nf #1:#2\\{\tabalign$#1:$&&$#2$\cr} % like `\nf Einstein: E=mc^2\\' + +% A numbered formula is similar, it typesets a parenthesized number at +% the left side, e.g., `\nrf 1 E=mc^2\\' +% Use as `\nrf 1 formula \\' +\def\nrf #1#2\\{\tabalign(#1)&&$#2$\cr} % numbered formula + +% To typeset formulas, named formulas, and hints in double columns, use +% the `d'-versions that take twice as much parameters. +\def\dnf #1:#2\\#3:#4\\{\tabalign$#1:$&&$#2$&&$#3:$&&$#4$\cr} % named formula +\def\df#1\\#2\\{\tabalign&&$#1$&&&&$#2$\cr} % double formula +% Use `\dh \relax \relax = {hint}' for empty left columns +\def\dh#1#2#3#4{\tabalign&$#1$&&\condhint{#2}&&$#3$&&$\{\,$#4$\,\}$\cr} +\def\condhint#1{\ifx#1\relax\else$\{\,$#1$\,\}$\fi} % left column empty + +% Here are the alignments of (double column) formulas and hint lines. +\def\+{\tabalign} % we don't want \outer\def +\def\setcols{\settabs\+\qquad&\quad&\qquad&\hskip .5\hsize\hskip-5em& + \qquad&\quad&\qquad&\cr} + +% Macros for programs +% comments are specified as `\co {some text}' +\def\co#1{\;\{\,#1\,\}} % comment +\def\cofl#1{\{\,#1\,\}} % comment flush left + +% Indententation of a program line is controlled by \& and \decind. +% \& sets the indentation of the following lines to its current position. +% \decind decrements the indentation level of the following lines +\newcount\nskips % holds number of tabstops +\def\skipn{\ifcase\nskips\def\j{&}\or\def\j{&&}\or\def\j{&&&} + \or\def\j{&&&&}\or\def\j{&&&&&}\or\def\j{&&&&&&}\or\def\j{&&&&&&&} + \else\def\j{}\fi\j} % skip nskips tabstops +\def\skipnmone{\global\advance\nskips by -1 \skipn\global\advance\nskips by 1} + +% Set a tabstop, succeeding lines will be left aligned to the new tabstop. +\def\&{$\cleartabs&\global\advance\nskips by 1$}% + +% Decrement indentation, succeeding lines will be left aligned to the tabstop +% preceding the current one. +\def\decind{$\global\advance\nskips by -1$} + +% The active character ^^M (end of line) both formats a program line and +% deliminates it. +\def\eatfirst#1{} +\catcode`\^^M=\active % +\def\programline#1{\ifx;#1\def\next##1^^M{\+\skipnmone\hfill$;\;$&$##1$\cr^^M}% + \else\ifx\eblock#1\def\next{\eblock}% + \else\ifx\cofl#1\def\next##1^^M{\+\skipn$\cofl{##1}$\cr^^M}% + \else\ifx\od#1\def\next##1^^M{\+\skipnmone\hfill$\rawod$&$##1$\decind\cr^^M}% + \else\ifx\FI#1\def\next##1^^M{\+\skipnmone\hfill$\rawfi$&$##1$\decind\cr^^M}% + \else\ifx\|#1\def\next##1^^M{\+\skipnmone\hfill$\rawbar\;\;$&$##1$\cr^^M}% + \else\ifx\]#1\def\next##1^^M{\+\skipnmone\hfill$]\;$&$##1$&\decind\cr^^M}% + \else\def\next##1^^M{\+\skipn$#1##1$\cr^^M}\fi\fi\fi\fi\fi\fi\fi\next}% +% +% Enclose a block of program lines between \bblock and \eblock. +\def\bblock{\doparskip\nskips=0\catcode`\^^M=\active \let^^M=\programline }% +\def\eblock{\catcode`\^^M=5 \setcols }% +\catcode`\^^M=5 % + +% Identation is controlled automatically be some tokens as follows: + +% `\[', `\do', and `\IF' set a tabstop right of them and increment +% the indent level. The corresponding closing tokens decrement the +% indent level. The `;', the `|', the \od and the \]| tokens at the +% beginning of a new line are typeset slightly left of the current +% identation level. + +% Tokens in our programming language +% block +\def\[{[\;\&} +\def\nomenclature#1{\mathbin{\hbox{\bf#1}}\>} +\def\glocon{\nomenclature{glocon}} +\def\glovar{\nomenclature{glovar}} +\def\vircon{\nomenclature{vircon}} +\def\virvar{\nomenclature{virvar}} +\def\pricon{\nomenclature{pricon}} +\def\privar{\nomenclature{privar}} +\def\]{\;]\decind} +% primitive initializing statement +\def\vir{${\bf\ vir }$} +\def\array{${\bf\ array}$} +% assignment +\def\:#1{\mathord{\>\,:\!=\>\,}} % use as `\:=' +% guarded command list +\def\-#1{\;\;\mathord{\rightarrow}\;\;} % use as '\->' +\def\|{\;\rawbar\;} +% if statement +\def\IF{\rawif\&} +\def\FI{\;\;\rawfi\decind} +% do statement +\def\do{\rawdo\&} +\def\od{\;\;\rawod\decind} + +% internal use +\def\rawbar{|\hskip -1.4pt]} +\def\rawdo{\hbox{\bf do}\;\;} +\def\rawod{\hbox{\bf od}\;\;} +\def\rawfi{\hbox{\bf fi}\;\;} +\def\rawif{\hbox{\bf if}\;\;} + +% format definitions +\parindent=0pt +\parskip=6pt plus 2pt minus 2pt +\def\unparskip{\vskip-\parskip} +\def\doparskip{\vskip \parskip} +\def\bi{\hfil\break\hbox{\qquad}} +\setcols |