NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing
transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its
accessibility to textreading software. It will be replaced by a fully markedup version when time permits. —HR
When messages may crawl, II (A sequel to EWD708).
In EWD708 I wrote “the messages are essentially empty envelopes;
allowing the envelopes to contain something was felt to be a minor
complication that we could postpone for the time being”. The purpose of this
note is to investigate how minor or major this complication turns out to be.
We modify the program by distinguishing the different messages from
C to D by a subscript i and the ones in the opposite direction by a
subscript j :

{P} do B1C_{i},→ S1_{i}; S1D_{i} {P} 
  
▯ B2Dj → S2Dj; S2Cj {P} 
 
od 
and its correctness proof now comprises the (many) theorems

P and B1C_{i} ⇒ wp(“S1C_{i}; S1D_{i}”, P)  (2_{i})


P and B2D_{j} ⇒ wp(“S2D_{j}; S2C_{j}”, P) .  (3_{j})

In this note we regard the way in which the difference between
different messages from C to D has been indicated by the implementation as
irrelevant: the contents of the messages may differ, they may be sent along
different channels that can be distinguished, or any mixture thereof. It is
an implementation detail, from which we are allowed to abstract.
In analogy to EWD708, the following program is regarded to be
representative for the corresponding mail system:

{P} (A j: c_{j}:= 0); (A i: d_{i}:= 0); {M} 

do B1C_{i} → S1C_{i} ; d_{i}:= d_{i} + 1 {M} 
 
▯ d_{i} > 0 → d_{i}:= d_{i}  1; S1D_{i} {M} 
 
▯ B2D_{j} → S2D_{j}; c_{j}:= c_{j} + 1 {M} 
 
▯ c_{j} > 0 → c_{j}:= c_{j}  1; S2C_{j} {M} 

od 
with the corresponding proof obligations

(E j: c_{j} ≠ 0) or (E i: d_{i} ≠ 0) or P = M  (4)


M and B1C_{i} ⇒wp(“S1C_{i}; d_{i}:= d_{i} +1”, M)  (5_{i})


M and d_{i} > 0 ⇒ wp(“d_{i}:= d_{i}  1; S1D_{i}”, M)  (6_{i})


M and B2D_{j} ⇒ wp(“S2D_{j}; c_{j}:= c_{j} + 1”, M)  (7_{j})


M and c_{j} > 0 ⇒ wp(“c_{j}:= c_{j}  1; S2C_{j}”, M)  (8_{j})

With the same notational convention —(9) and (10)— from EWD708, we
can satisfy (4), (6
_{i}), and (8
_{j}) by choosing for M
M: 
wp(“(A i: S1D_{i} ↑ d_{i}); (A j: S2C_{j} ↑ c_{j})”, P)  (11)

provided that (11) makes sense. In analogy to EWD708 this implies
(
A j: c
_{j} ≥ 0)
and (
A i: d
_{i} ≥ 0) ,
but this invariance is duly maintained by the above representation of the
mail system. But for (11) to make sense, we must require that (
A i: S1D
_{i} ↑ d
_{i})
and (
A j: S2C
_{j} ↑ c
_{i}) are defined, i.e. we must require

(A i1,i2: "SlD_{i1} ↑ d_{i1}; SlD_{i2} ↑ d_{i2}" = "S1Di2 ↑ d_{i2}; S1D_{i1} ↑ d_{i1}")  (16)

and 
(A jl,j2: "S2C_{j1} ↑ c_{j1}; S2C_{j2} ↑ c_{j2}" = "S2Cj2 ↑ c_{j2}; S2C_{j1} ↑ c_{j1}")  (17)

(This curious way of numbering results from my desire to give similar
formulae in this note and in EWD708 the same number.)
Salvo errore et omissione I have come to the conclusion that properties
(12) and (13) are stronger than necessary, and so are their consequences (14)
and (15), as mentioned in EWD708. In order to prove (5i) from (2i) the
weaker assumptions

(A j: B1C_{i} ⇒ wp("S2C_{i} ↑ c_{i}", BlC_{i})) (  14)

and 
(A j: BlC_{i} and wp("S2C_{j} ↑ c_{j}; S1C_{i}", R) ⇒ wp("S1C_{i}; S2C_{j} ↑ c_{j}", R))
 (15)

suffice. (The absence of the beginning term “E1C” in (13) and (15) of
EWD708 is, in retrospect, just an omission.)
One way of proving (14) and (15) is to show —as suggested in EWD708—
for each (i,j)pair

B1C_{i} ⇒ wp(“S2C_{j}”, B1C_{i})
 (12)


B1C_{i} and wp(“S2C_{j}; S1C_{i}’, R) ⇒wp(”S1C_{i}; S2C_{j}“, R) .  (13)

Properties (12) and (13) have the attraction that they are local
properties of node C of the telex system. Note that relations (14) and
(15) are also a consequence of

B1C_{j} ⇒ (c_{j} = 0) .  (18)

Similarly, in the spirit of EWD708, we would try to prove for any
(j1,j2)pair

”S2C_{j1}; S2C_{j2}“ = ”S2C_{j2}; S2C_{j1}“  (19)

from which (17) follows. Again we should note the existence of the
alternative: c
_{j1} = 0
or c
_{j2} = 0 .
Summarizing our proof obligation with respect to node C , we have to show:

(A i, j; BlC_{i} ⇒ wp("S2C_{j}, BlC_{i}) or c_{j} = 0)  (20)


(A i, j: BlC_{i} and wp("S2C_{j}; S1C_{i}", R) ⇒ wp("SlC_{i}; S2C_{j}", R) or c_{j} = 0)  (21)


(A jl,j2: "S2C_{j1}; S2C_{j2}" = "S2C_{j2}; S2C_{j1}" or c_{j1} = 0 or c_{j2} = 0)  (22)

With respect to node D we have, mutatis mutandis, the same obligations.
The weakening of our proof obligations, as represented by (20), (21),
and (22) leaves me with mixed feeling. Each time we have to make essential
use of the weakening, we have to prove that under certain circumstances
“exponents” are zero, and those are global properties that are not directly
reflected —at least for the time being I don’t see how— in the original telex
system. I console myself with the thought that, if a mail system is our
eventual target, they are not very desirable properties: in order to make
a mail system it is customary to make message receptions commute if possible.
One advantage of conditions (20), (21), and (22) is certainly that they give
the designer of a mail system a clear summary of his options.
Plataanstraat 5  prof.dr.Edsger W.Dijkstra

5671 AL NUENEN  Burroughs Research Fellow

The Netherlands 

Transcribed by Martin P.M. van der Burgt
Last revision
20150218
.