new generic package tex-ewd (11nov08)

git-svn-id: svn://tug.org/texlive/trunk@11261 c570f23f-e606-0410-a88d-b1316a301751

8 files changed, 765 insertions, 1 deletions

diff --git a/Master/texmf-dist/doc/generic/tex-ewd/README b/Master/texmf-dist/doc/generic/tex-ewd/README
new file mode 100644
index 00000000000..73758127457
--- /dev/null
+++ b/Master/texmf-dist/doc/generic/tex-ewd/README
@@ -0,0 +1,19 @@
+TeX-EWD is a set of plain TeX macros that helps typesetting formulas,
+calculational proofs, and programs written in Dijkstra's style. See
+  http://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1300.html
+for the `dot notation', i.e., the style for formulas and proofs, and the book
+  Dijkstra, "A Discipline of Programming", Prentice Hall, 1976
+for the `guarded commands language'.
+
+The file dotnot.tex contains the (generic) macros and hints how to
+use them, the files t1.tex and p0.tex demonstrate their usage.
+
+The macros where testet using TeX-GPC.
+
+This software is licensed to you under the terms of a BSD-style license,
+see bsdlic.txt for details.
+
+Enjoy,
+Wolfgang Helbig                              helbig@lehre.ba-stuttgart.de
+Stauferst. 22                     http://wwwlehre.ba-stuttgart.de/~helbig
+71334 Waiblingen                                            November 2008
diff --git a/Master/texmf-dist/doc/generic/tex-ewd/bsdlic.txt b/Master/texmf-dist/doc/generic/tex-ewd/bsdlic.txt
new file mode 100644
index 00000000000..873ab296811
--- /dev/null
+++ b/Master/texmf-dist/doc/generic/tex-ewd/bsdlic.txt
@@ -0,0 +1,24 @@
+Copyright (c) 2008, Wolfgang Helbig
+All rights reserved.
+
+Redistribution and use with or without modification are permitted
+provided that the following conditions are met:
+
+* Redistributions must retain the above copyright notice, this list
+  of conditions and the following disclaimer.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND
+CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES,
+INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.
+IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGE.
diff --git a/Master/texmf-dist/doc/generic/tex-ewd/p0.tex b/Master/texmf-dist/doc/generic/tex-ewd/p0.tex
new file mode 100644
index 00000000000..0524281185c
--- /dev/null
+++ b/Master/texmf-dist/doc/generic/tex-ewd/p0.tex
@@ -0,0 +1,463 @@
+% This software is licensed to you under the terms of a BSD-style license,
+% see bsdlic.txt for details.
+\input dotnot
+\headline{\ifnum\count0=1\hfil\else\centerline\title\fi}
+\def\title{A Short Program Whose Construction Isn't}
+\def\out{{\it out:\/}}
+\centerline{\bf \title}
+
+\beginsection Introduction
+
+This is a construction of a {\it Simple Program Whose Proof Isn't},
+as D.~E.~Knuth titled his contribution to {\it Beauty Is Our
+Business, A Birthday Salute to Edsger W. Dijkstra}.  Knuth's program
+is module 103 from \TeX. Given integer $n$ it prints a decimal
+fraction that approximates $n/2^{16}$ using just enough digits such
+that the fraction determines $n$ uniquely.  Both David Gries (in
+{\it Binary to Decimal, One More Time}) and Knuth presented proofs
+in the same volume that use unique properties of $2^{16}$. But this
+program provides a nontrivial generalization, it complies to the
+requirements for any $q > n \ge 0$.  We call it ``\out''.
+
+\beginsection Notation
+
+For program construction, that is developing the program {\it and\/} its
+proof hand in hand, Dijkstra proposed both a notation (see EWD
+1300) and a programming language (see {\it A Discipline Of
+Programming}) that we are going to use here---however, slightly
+modified, blocks are deliminated by $[$ and $]$.
+A dot denotes function application, like ``$f.x$'' for ``$f(x)$''.
+Dot and colon have the same precedence and are left associative;
+e.g., ``$d:hiext.i$'' means ``$(d:hiext).i$''.  The precedence is
+higher than that of any other operator, e.g., ``$\neg(d \:= a).R0$''
+means ``$\neg\bigl((d \:= a).R0\bigr)$''.
+
+For expressions $E$, $F$, and $G$ we notate substitution of $E$ by
+$F$ in $G$ as ``$(E \:= F).G$'', e.g.,
+\f (x \:= x+y).(x > 0) \meq x+y > 0\qquad,\hbox{or}\\
+\f \bigl((10+5) \:= 7\bigr).\bigl((10+5) * 2\bigr)\qquad=\qquad 14\qquad.\\
+The last example shows that we don't constraint the
+substituion function to predicates but apply it to any expression,
+in this case to an integer expression, and that we allow any
+expression left of $\:=$, not only program variables.
+
+We denote a conventionally written set $\{t.x \mid r.x\}$ as $\<x :
+r.x : t.x\>$. The three colon separated fields denote the dummy
+variable ($x$), the range of the dummy ($r.x$) and the terms ($t.x$),
+that is the elements of the set.  Quantified operators applied to
+a set are written just after the $\langle$, e. g., $\<\mx i : i <
+10 : i\>$ is the maximum integer exceeded by ten, and $\<\nbr i :
+0 \le i < 10 : i\>$ is the number of naturals exceeded by 10.
+
+Throughout this paper, the type of $m$, $n$, $i$, $j$, and $p$ is
+integer and of $q$ positive integer and of $r$ rational. The
+variables $d$ and $a$ are of type integer array with the lower
+bound of its domain being one.
+
+\beginsection Integer Artithmetic
+
+This construction of \out\ is based on
+\proclaim Theorem 0.
+A half open interval of length $j$ contains exactly $j$ integers.
+
+As programmers we all know this theorem for intervals with integral
+end points but its extension to arbitray end points might come as
+a surprise. We'll use the following corollaries in this paper.
+
+\proclaim Corollary 0.
+$m = \< \mx i : i \le p/q : i\>\meq p/q-1 < m \le p/q$
+
+\proclaim Corollary 1.
+$m = \< \mx i : i < p/q : i\>\meq p/q-1 \le m < p/q$
+
+\proclaim Corollary 2.
+$ p\div q = \< \mx i : i*q \le p : i\>$
+
+\proclaim Corollary 3.
+$(p-1)\div q = \< \mx i : i*q < p : i\>$
+
+\beginsection Specification of \out
+
+Given integers $n$, $q$ with $0 \le n < q$, \out\ computes a decimal
+representation of $n/q$. It stores the digits in an array $d$ with
+$d.lob = 1$. For any integer array $a$ with $a.lob=1$ let $a.s$
+be the sum
+\f a.s = \< \su i : a.lob \le i \le a.hib : a.i/10^i\>\\
+
+{\it d.s is close enough to $n/q$\/}:
+\nf R0:   (n-1/2)/q \le d.s < (n+1/2)/q\\
+
+{\it The length of $d$ is minimal\/}:
+\nf R1:   \< \fa a : a.hib < d.hib : \neg(d \:= a).R0 \>\\ 
+
+{\it
+If there is more than one approximation that is close enough to
+$n/q$ and yielded by an array of minimal length, $d.s$ is the closest one\/}:
+\nf R2: \<\nbr a : (d \:= a).R0 \mand a.hib = d.hib : a.s \> > 1
+\mimpl |n/q - d.s| \le | n/q - a.s|\\
+
+{\it d contains decimal digits\/}:
+\nf R3:   \< \fa i : d.lob \le i \le d.hib : 0 \le d.i < 10\>\\
+
+\beginsection Construction of \out
+
+For brevity, we define expressions that depend implicitly on $d$, the only
+variable in the state space of \out.
+\dnf L: d.hib\\Q: 10^L\!/q\\
+\dnf N: 10^L*d.s\\J: \<r : (n-1/2)*Q \le r < (n+1/2)*Q : r\>\\
+
+We introduced $N$ because it is an integer and $J$ because it is
+a half open interval of length $Q$. They are related to $R0$ by
+\nrf0 R0 \meq N \in J\qquad.\\
+
+For the proof of (0) we observe
+\f R0 \\
+\heq {multiply by $10^L$, definition of $N$ and $Q$}
+\f (n-1/2)*Q \le N < (n+1/2)*Q\\
+\heq {Def. of $J$}
+\f N \in J\\
+
+We construct a loop that starts with an empty array $d$, appends an
+integer to $d$ in each iteration and terminates
+with $R0 \mand R1$.
+
+Applying the Linear Search Theorem to find the minimal length
+we introduce the loop guard
+\nf G0: \< \fa a : a.hib = L : \neg(d \:= a).R0 \>\qquad.\\
+
+Since $N$ is an integer and $J$ depends on $L$ only, not on the entries
+of $d$, (0) lets us conclude
+\f G0 \mff \<\nbr i : i \in J : i\> = 0\qquad.\\
+\filbreak
+To test for $\<\nbr i : i \in J : i\> > 0$, we use a wittness $N$
+that is in $J$ whenever $J$ contains an integer at all. Two candidates for
+$N$ come to mind:
+\df N = \< \mx i : i < (n+1/2)*Q : i\>\\  N = \< \mn i : (n-1/2)*Q\le i : i\>\\ 
+\df \;\mand\\                               \;\mand \\
+\df \<\nbr i : i \in J : i\> = 0\\         \<\nbr i : i \in J : i\> = 0\\
+\dh\eq {arithmetic}                     \eq {arithmetic}
+\df   N < (n-1/2)*Q                 \\    (n+1/2)*Q \le N        \\
+\filbreak
+We decide for the left alternative. It leads to a nondecreasing
+sequence of the intermediate sums $d.s$, and that is equivalent to
+the entries in $d$ being naturals. We take
+
+\nf P0:  N = \< \mx i : i < (n+1/2)*Q : i \> \\
+\unparskip
+as a loop invariant and replace $G0$ by the loop guard
+\nf G1:  N < (n-1/2)*Q\qquad.\\
+\filbreak
+The program reads---with $E$ chosen such that $wp.``d:hiext.E".P0$ holds:
+\bblock
+   d \vir int \array \:= (1) \co{R1; P0}
+   ;\do G1 \-> d:hiext.E \co{R1; P0} \od
+   \cofl{\neg G1; R1; P0}
+\eblock
+We are going to prove that $P0$ and $R1$ are loop invariants.
+\doparskip
+\dnf P0 \hbox{ is established by the initialization}:\\
+     P0 \hbox{ is maintained}:\\
+\df  wp.``d \:= (1)".P0\\
+     wp.``d:hiext.E".P0\\
+\dh\eq   {$N, L \:= 0,0$}
+   \eq   {choice of $E$}
+\df  0 = \<\mx i : i < (n+1/2)/q : i\>\\
+     true\\
+\heq   {Corollary 1}
+\f  (n+1/2)/q - 1 \le 0 < (n + 1/2)/q\\
+\heq   {$0 \le n$ implies the right $<$}
+\f  n+1/2 \le q\\
+\heq   {$n$, $q$ are integers}
+\f  n < q\\
+\heq   {precondition of \out}
+\f  true\\
+\doparskip
+\dnf R1\hbox{ is established by the initialization}:\\
+     R1\hbox{ is maintained}:\\
+\df  wp.``d \:= (1)".R1\\
+     wp.``d:hiext.E".R1\\
+\dh\eq   {$L \:= 0$}
+   \eq   {$L \:= L+1$}
+\df  \<\fa i : 0 \le i < 0 : \neg(L \:= i).R0 \>\\
+     \< \fa i : 0 \le i < L+1 : \neg(L \:= i).R0 \>\\
+\dh\eq   {predicate calculus: empty range of $\fa$}
+   \eq   {predicate calculus: split range}
+\df  true\\
+     \< \fa  i : 0 \le i < L : \neg(L \:= i).R0 \> \mand \neg(L \:= L).R0\\
+\dh {} {} \eq   {Def. of $R1$}
+\df \\ R1 \mand  \neg R0\\
+\dh{} {} \eq   {$R1$ is precondition}
+\df \\ \neg R0\\
+\dh {} {} \ff  {construction of $G1$}
+\df \\ G1\\
+\dh {} {} \eq   {$G1$ is precondition}
+\df \\ true\\
+
+For the termination proof, we note that $L$ is incremented in each iteration
+and bounded from above:
+\f   10^L < q\\
+\heq   {Def. of $Q$, $q > 0$}
+\f   Q < 1\\
+\h\ff  {$J$ is an half open interval of length $Q$; Theorem 0}
+\f   \<\nbr i : i \in J : i\> = 0\\
+\heq   {$G1 \mand P0$}
+\f   true\\
+
+That finishes the proof of the above program and we are ready to turn to
+\nf R2: \<\nbr a : (d \:= a).R0 \mand a.hib = L : a.s \> > 1
+\mimpl |n/q - d.s| \le | n/q - a.s|\qquad.\\
+
+$R2$'s antecedent reduces to $\<\nbr i : i \in J : i\> > 1$, since
+for any $a$ with $a.hib = L$ the number $a.s*10^L$ is an integer,
+which is contained in $J$ precisely when $(d \:= a).R0$ holds.
+
+$R2$'s consequence is equivalent to
+\f n*Q - 1/2 \le N \le n*Q+1/2\qquad.\\
+Since this condition does not always determine a unique solution
+for $N$, we impose the slightly stronger one constraining $N$ to
+a half open interval of length 1.
+
+\nf R2C: n*Q - 1/2 < N \le n*Q+1/2\qquad.\\
+\filbreak
+$R2C$ looks quite different from $P0$. To avoid appending a "wrong"
+digit according to $P0$, we take a further loop invariant that
+implies the negation of $R2$'s antecedent.
+
+\f \<\nbr i : i \in J : i\> \le 1\\
+\h\ff {$J$ is an half open interval of length $Q$; Theorem 0}
+\nf P1: Q \le 1\\
+
+$P1$ is established by initialization:
+\f   wp.``d \:= (1)".P1 \\
+\heq   {$Q \:= 1/q$}
+\f   1 \le q\\
+\heq   {$0 \le n < q$}
+\f   true\\
+
+We calculate guard $G2$ such that $P1$ is maintained:
+\f   wp.``d:hiext.E".P1\\
+\heq   {$Q \:= 10*Q$}
+\nf G2: 10*Q \le 1\\
+
+With $G2$, the loop might terminate while $G1$ is still true, that is without
+reaching $R0$. In that case, we compute the last digit according to $R2C$.
+
+The program now reads---with $E$ chosen such that $wp.``d:hiext.E".P0$ holds
+and $F$ chosen such that $wp.``d:hiext.F".R2C$ holds:
+
+\bblock
+   d \vir int \array \:= (1) \co{P0\and R1\and P1}
+ ; \do G1 \mand G2 \-> d:hiext.E \co{P0\and R1\and P1} \od
+   \cofl{\neg (G1 \and  G2) \and P0 \and R1 \and P1}
+ ; \IF G1 \-> d:hiext.F \co{R2C} \| \neg G1 \-> skip\FI
+   \cofl{R0\and R1\and R2}
+\eblock
+We will prove that the if-statement establishes the postconditions.
+We already have proven that the loop terminates and establishes
+its postconditions. According to the guards of the if-statement,
+our proof takes two cases:
+
+Case zero: The loop terminates with $\neg G1$: 
+
+Here the if-statement selects the skip statement. Its predicate
+transformer, $wp.skip$, is the identity function.
+
+$R0$ is reached:
+\df   (n-1/2)*Q \le N \\      N < (n+1/2)*Q \\
+\dh\eq {$\neg G1$}        \eq  {$P0$}
+\df   true	\\	      true \\
+
+$R1$ is reached: $R1$ is a precondition of the if-statement.
+
+$R2$ is reached: $P1$ implies the negation of $R2$'s antecedent
+and is a precondition of the if-statement.
+ 
+This ends the proof for case zero.
+\filbreak
+Case one: The loop terminates with $G1$:
+
+$R0$ is reached: We show that $R0$ holds in the state after
+``d:hiext.F''.
+\nf R0: (n-1/2)*Q \le N < (n+1/2)*Q\\
+\heq {towards $R2C$}
+\f n*Q -(1/2)*Q \le N < n*Q + (1/2)*Q\\
+\h \ff {$1<Q$, see (**) below; transitiviy of $<$ and $=$}
+\f n*Q -1/2 \le N \le  n*Q + 1/2\\
+\heq {$F$ chosen sucht that $R2C$ holds}
+\f true\\
+
+(**)$1<Q$ holds because
+\f wp.``d:hiext.F".(1<Q)\\
+\heq {$Q \:= 10*Q$}
+\f 1 < 10*Q\\
+\heq {Definition of $G2$}
+\f \neg G2\\
+\heq {$G1 \mand (\neg G1 \mor \neg G2)$}
+\f true\\
+
+$R1$ is reached: The proof for the invariance of $R1$ can be taken
+verbatim, since here we have the same preconditions ($G1; R1; P0$).
+
+$R2$ is reached: Its consequence $R2C$ is established by the choice of $F$.
+
+That finishes the proof for $R0$, $R1$, and $R2$.  So far, we
+ignored $R3$.  In fact, the final value of $d.s$ and $L$ is uniquely
+defined by the other three conditions.  But the intermediate values
+of $d.s$ and---equivalently the entries of $d$---are not. We can
+only hope that \out\ delivers decimal digits.
+
+We show $0 \le E < 10$ in the state before
+``$d:hiext.E$'', where $wp.``d:hiext.E".P0$ holds.
+\f    wp.``d:hiext.E".P0\\
+\heq     {$N, Q \:= 10*N+E, 10*Q$}
+\f    10*N + E = \<\mx i : i < (n+1/2)*10*Q : i \>\\
+\heq     {simplify}
+\f    E = \<\mx i : i < \bigl((n+1/2)*Q - N\bigr)*10 : i \>\\
+\heq    {Corollary 1}
+\f   \bigl((n+1/2)*Q - N\bigr)*10 - 1 \le E < \bigl((n+1/2)*Q-N\bigr)*10 \\
+
+We observe:
+\f     0 \le E \\
+\heq      {trick, 0 and $E$ are integers}
+\df    -1  < E \\
+       E < 10 \\
+\dh\ff   {above, left end}
+   \ff   {above, right end}
+\df   -1 < \bigl((n+1/2)*Q - N\bigr)*10 - 1 \\
+      \bigl((n+1/2)*Q - N\bigr)*10 \le 10 \\
+\dh \eq  {simplify}
+    \eq  {simplify}
+\df   N < (n+1/2)*Q\\
+      (n+1/2)*Q \le N + 1\\
+\dh \eq  {$P0$, right end}
+    \eq  {$P0$, left end}
+\df  true\\
+     true\\
+\filbreak
+So far so good! Now $F$.
+We show $0 \le F < 10$ in the state before
+``$d:hiext.F$'', where $wp.``d:hiext.F".R2C$ holds.
+\f   wp.``d:hiext.F".R2C \\
+\heq   {$N, Q \:= 10*N+F, 10*Q$}
+\f   (n*Q-N)*10 - 1/2 < F \le (n*Q-N)*10 + 1/2\\
+\filbreak
+We observe:
+\df  0 \le F \\
+     F < 10 \\
+\dh \eq  {trick, 0 and $F$ are integers}
+    \ff  {see above, right end}
+\df  -1 < F\\
+    (n*Q-N)*10 + 1/2 < 10\\
+\dh \ff   {see above, left end}
+    \eq   {heading for $P0$, left end}
+\df  -1 \le (n*Q-N)*10 - 1/2\\
+    (n*Q-1)*10 + 1/2 < N*10\\
+\dh \eq  {simplify}
+    \ff  {$P0$, left end}
+\df  -1/2 \le (n*Q-N)*10\\
+  (n*Q-1)*10 + 1/2 < (n+1/2)*Q*10-10\\
+\dh \ff  {arithmetic}
+    \eq  {simplify}
+\df  N < n*Q\\
+     1/2 < (1/2)*Q*10\\
+\dh\eq   {$G1$}
+   \eq   {$\neg G2$}
+\df true\\
+    true\\
+\filbreak
+
+Now that \out\ is proved correct---lucky as we are, $R3$ holds---,
+we reduce the expressions to integer arithmetics. We start with 
+\nf G2: 10*Q \le 1\\
+\heq {$Q=10^L\!/q$}
+\f 10^{L+1} \le q\\
+\heq {new variable $u$ with invariant $u = 10^{L+1}$}
+\f u \le q\\
+
+The invariant of $u$ is established by $u \:= 10$ and maintained
+by $u \:= 10*u$.
+\filbreak
+Next, we reduce
+\nf G1:  N < (n-1/2)*Q \\
+\heq   {expand with $q$, reuse $u$}
+\f   N*q*10 < (n-1/2)*u\\
+\heq   {think positive}
+\f   u/2 < n*u - N*q*10\\
+\heq   {$u = 10^{L+1}$ is even}
+\f   u \div 2 < n*u - N*q*10\\
+\heq   {new variable $v$ with invariant $v=n*u-N*q*10$}
+\f   u \div 2 < v\\
+\filbreak
+The expressions $n*u$ and $N*q*10$ might take large values. To avoid integer
+overflow, we store their difference in $v$. The invariant of $v$ is established
+by $v \:= 10*n$.
+We calculate $V$ such that $v$'s invariant is maintained by $v \:= V$.
+\f   wp.``d:hiext.E; u, v \:= 10*u, V".(v = n*u - N*q*10)\\
+\heq   {semantics of the semicolon}
+\f   wp.``d:hiext.E".\bigl(wp.``u, v \:= 10*u, V".(v = n*u - N*q*10)\bigr)\\
+\heq   {semantics of the assignment}
+\f   wp.``d:hiext.E".(V = n*10*u - N*q*10)\\
+\heq   {array semantics: $N \:= 10*N+E$}
+\f   V = n*10*u - (10*N+E)*q*10\\
+\heq {simplify}
+\f   V = (n*u - 10*N*q-E*q)*10\\
+\heq     {invariant for $v$}
+\f   V = (v-E*q)*10\\
+\filbreak
+Reducing $E$ and $F$ to $\div$ is straight forward by the well
+known Corollary 2 and the slightly less well known Corollary 3.
+
+\dnf E: \<\mx i : i < \bigl((n+1/2)*Q - N\bigr)*10 : i \>\\
+     F: \<\mx i : i \le (n*Q - N)*10 + 1/2 : i \>\\
+\dh=   {expand with $q$}
+   =    {expand with $q$, reuse $u$}
+\df   \<\mx i : i*q < (n+1/2)*10^{L+1} - N*q*10 : i \>\\
+      \<\mx i : i*q \le n*u - N*q*10 + q/2 : i \>\\
+\dh=    {reuse $u$}
+   =    {reuse $v$}
+\df  \<\mx i : i*q < n*u+ u/2 - N*q*10 : i \>\\
+     \<\mx i : i*q \le v + q/2 : i \>\\
+\dh=    {reuse $v$ , $u$ is even}
+   =    {see (*)}
+\df  \<\mx i : i*q < v + u \div 2 : i \>\\
+     \<\mx i : i*q \le v + q \div 2 : i \>\\
+\dh=    {Corollary 3}
+   =    {Corollary 2}
+\df   (v + u \div 2 - 1) \div q\\
+      (v + q \div 2) \div q\\
+\filbreak
+The equation at (*) holds when $q$ is even, since then $q/2 = q \div 2$.
+And when $q$ is odd, we have $q/2 = q \div 2 + 1/2$ and we observe
+\f    i*q \le v + q/2\\
+\heq     {$q$ is odd}
+\f    i*q \le v + q \div 2 + 1/2\\
+\heq     {$i*q$ and $v + q \div 2$ are integers}
+\f    i*q \le v + q \div 2\\
+\filbreak
+This ends the reduction of \out\ to integer arithmetic and the construction
+of our program.
+\bblock
+ \out\; \[\glocon n, q; \virvar d \co {0 \le n < q}
+; \privar u, v
+; d \vir int \array, u \vir int, v \vir int \:= (1), 10, n*10
+; \do u \div 2 < v  \mand  u \le q \->\&%
+     d:hiext.\bigl((v + u \div 2 - 1) \div q\bigr)
+       ; u, v \:= 10*u, (v - d.high*q)*10 \decind
+  \od
+; \IF u \div 2 < v \-> d:hiext.\bigl((v + q \div 2) \div q\bigr)
+  \| u \div 2 \ge v \-> skip
+  \FI
+\] \co {R0 \mand R1 \mand R2 \mand R3}
+\eblock
+That's it. The program is only proved correct, not tested.  The
+proof and/or the program might contain errors. Please don't hesitate
+to contact me if you found one, or if you know a better way to
+apply Dijkstra's technique to a problem that turned out to be
+surprisingly hard.
+\vfill
+\bi
+Wolfgang Helbig\hfill {\tt helbig@lehre.ba-stuttgart.de}\qquad\bi
+Stauferstr. 22\hfill {\tt wwwlehre.ba-stuttgart.de/\~{}helbig/}\qquad\bi
+71334 Waiblingen\hfill October 2008\qquad\hfill
+\eject
+\end
diff --git a/Master/texmf-dist/doc/generic/tex-ewd/t1.tex b/Master/texmf-dist/doc/generic/tex-ewd/t1.tex
new file mode 100644
index 00000000000..1f69f368011
--- /dev/null
+++ b/Master/texmf-dist/doc/generic/tex-ewd/t1.tex
@@ -0,0 +1,73 @@
+% This software is licensed to you under the terms of a BSD-style license,
+% see bsdlic.txt for details.
+% This file demonstrates usage of the dotnot macros.
+\input dotnot
+\headline{\bf \title}
+\def\title{\centerline{Usage of dotnot}}
+\def\out{\hbox{\it out:\/}}
+
+The greatest common denominator:
+\bblock
+\cofl{m > 0 \land n > 0}
+\[\glocon m, n; \virvar gcd
+  ; \privar i, j
+  ; i \vir int, j \vir int \:= m, n
+  ; \do i \not= j \->\IF i > j \-> i \:= i - j
+                     \| j > i \-> j \:= j - i
+                     \FI 
+    \od
+  ; gcd \vir int \:= i
+\] \co{gcd = \gcd.(n, m)}
+\eblock
+This is the outcome of p0:
+\bblock
+\out\;\[\glocon n, q; \virvar d
+\cofl{0 \le n < q}
+; \privar u, v
+; d \vir int \array, u \vir int, v \vir int \:= (1), 10, n*10
+; \do u \div 2 < v  \mand  u \le q \->\&%
+                                  d:hiext.\bigl((v + u \div 2 - 1) \div q\bigr)
+                                ; u, v \:= 10*u, (v - d.high*q)*10 \decind
+   \od
+; \IF u \div 2 < v \-> d:hiext.\bigl((v + q \div 2) \div q\bigr)%
+  \| v \le u \div 2 \-> skip   % use `%' to combine several input lines
+                                  % into one output line
+  \FI
+\] \co{\hbox{$d$ contains the decimal digits of $n/q$}}
+\eblock
+An alternative program to compute the greatest common denominator:
+\bblock
+\[\glocon m, n; \virvar gcd
+   ;\privar i, j
+   ;i \vir int, j \vir int \:= m, n
+   ;\do i > j \-> i \:= i - j
+     \| i < j \-> j \:= j - i
+    \od
+   ;gcd \vir int \:= (i + j) \div 2
+\]
+\eblock
+This program computes the next higher permutation of c.
+\bblock
+\[ \glovar c; \privar i,j
+  ; i\vir int \:= c.hib -1;\;\do c.i \ge c.(i+1) \-> i \:= i - 1\od
+  ; j\vir int \:= c.hib;\;\do c.j \le c.i \-> j \:= j-1 \od
+  ; c:swap.(i,j)
+  ; i \:= i+1; j \:= c.hib;
+  ; \do i < j \-> c:swap.(i,j); i,j \:= i+1,j-1 \od
+\]
+\eblock
+And this is the famous Dutch flag program:
+\bblock
+\[ \glovar buck; \glocon n; \privar r, w, b
+ ; r \vir int, w \vir int, b\vir int \:= 1, n,n
+ ; \do w \ge r \-> \[ \glovar buck, r, w, b; \pricon col
+                ; col \vir colour \:= buck.w 
+                ; \IF col = red \-> buck:swap.(r,w); r := r+1
+		   \| col = white \-> w \:= w-1
+		   \| col = blue \-> buck:swap.(w,b); w,b \:= w-1, b-1
+		  \FI 
+	       \]
+   \od
+\]
+\eblock
+\bye
diff --git a/Master/texmf-dist/tex/generic/tex-ewd/dotnot.tex b/Master/texmf-dist/tex/generic/tex-ewd/dotnot.tex
new file mode 100644
index 00000000000..24031e2a42a
--- /dev/null
+++ b/Master/texmf-dist/tex/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
diff --git a/Master/tlpkg/bin/ctan2tds b/Master/tlpkg/bin/ctan2tds
index 08afd47578a..479690f04df 100755
--- a/Master/tlpkg/bin/ctan2tds
+++ b/Master/tlpkg/bin/ctan2tds
@@ -1024,6 +1024,7 @@ $standardtex='\.(cfg|sty|clo|ldf|cls|def|fd|cmap|4ht)$';
  'subfigure',	'\.sty|[^c]\.cfg',  # omit ltxdoc.cfg, would be system-wide
  'syntax',	'syntax\.tex',
  'taylor',	'diagrams.tex',
+ 'tex-ewd',	'dotnot.tex',
  'texsis',	'\.txs|TXS.*tex|texsis.tex',
  'ticket',	'\.tdf|' . $standardtex,
  'tools',	'\.cfg|\.sty|\.clo|\.cls|\.def|\.fd$|.?\.tex|^\.tex$',
diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check
index 3d8b5ff7efd..20e71d0027d 100755
--- a/Master/tlpkg/bin/tlpkg-ctan-check
+++ b/Master/tlpkg/bin/tlpkg-ctan-check
@@ -205,7 +205,7 @@ my @WorkingTLP = qw(
         t-angles t2 Tabbing tableaux tablists tablor tabulary tabvar talk 
 	  tamethebeast tdsfrmath
           ted templates-fenn templates-sommer tengwarscript
-          tensor termlist teubner tex-gyre texilikecover texmate
+          tensor termlist teubner tex-ewd tex-gyre texilikecover texmate
           texpower texshade
           textcase textfit textopo textpath textpos
           theoremref thesis-titlepage-fhac
diff --git a/Master/tlpkg/tlpsrc/tex-ewd.tlpsrc b/Master/tlpkg/tlpsrc/tex-ewd.tlpsrc
new file mode 100644
index 00000000000..de89b25d405
--- /dev/null
+++ b/Master/tlpkg/tlpsrc/tex-ewd.tlpsrc
@@ -0,0 +1,2 @@
+name tex-ewd
+category Package