When messages may crawl, II (A sequel to EWD708)

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 text-reading software. It will be replaced by a fully marked-up 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 :

(1)

{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

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 2015-02-18 .