1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
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
|
