diff options
Diffstat (limited to 'Master')
| -rw-r--r-- | Master/texmf-dist/doc/generic/tex-ewd/README | 19 | ||||
| -rw-r--r-- | Master/texmf-dist/doc/generic/tex-ewd/bsdlic.txt | 24 | ||||
| -rw-r--r-- | Master/texmf-dist/doc/generic/tex-ewd/p0.tex | 463 | ||||
| -rw-r--r-- | Master/texmf-dist/doc/generic/tex-ewd/t1.tex | 73 | ||||
| -rw-r--r-- | Master/texmf-dist/tex/generic/tex-ewd/dotnot.tex | 182 | ||||
| -rwxr-xr-x | Master/tlpkg/bin/ctan2tds | 1 | ||||
| -rwxr-xr-x | Master/tlpkg/bin/tlpkg-ctan-check | 2 | ||||
| -rw-r--r-- | Master/tlpkg/tlpsrc/tex-ewd.tlpsrc | 2 |
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 |