Semantics of straight-line programs (Draft Chap.4)

Copyright Notice

The following manuscript

EWD 910: Semantics of straight-line programs

is an early draft of Chapter 7 of

E.W. Dijkstra and C.S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, 1990.

Permission to reproduce the manuscript here has been granted by Springer-Verlag New York.

Semantics of straight-line programs. (Draft Chap.4)

Program execution as change of machine state

This is a monograph about a theory of program- ming language semantics. A "programming language" is usually identified with all programs that can be written in it and the "semantics" refers to what would happen each time, were such a program fed into an appropriate computer.

Remark We regret the terminology we used in the preceding paragraph, but the terminology is by now so firmly established that there seems to be no point anymore in deviating from it. In retrospect we would have been much happier, had programming languages never been called "languages". Admittedly, the metaphor has been helpful in the very beginning: the linguistic analogy gave a hint what aspects to distinguish and provided a terminology for identity. By using them. Our regret comes from the fact that, beyond that initial service, the linguistic analogy has been more confusing than helpful. The term "pro-gramming language" was first a symptom of, and once established - a driving force behind the habit of describing computing systems in anthropomorphic terminology, a habit we have to shed for all its misleading connotations if a mature computing science is to emerge. (End of Remark.)

Now, one aspect of doing science consists in ignoring what is chosen to be considered irrelevant, and the question is: what are we going to ignore and what are we going to take into account when referring to "what would happen, were such a program fed into a computer"?

We are going to ignore all physical characteristics of the computer: its technology, its size, its weight, its power consumption, its reliability, its maintenance contract, and its manufacturer, just to mention a few irrelevantia. Presumably the machine has a manual, but in that case we do not regard it as the manual's task to describe the machine, but as the machine's task to provide a -hopefully correct- physical model of the manual's contents. In case of a discrepancy, we would blame the machine and not the manual: it is the abstract machine we can think about that matters.

Having decided that it is the thinkable machine that really matters in our heads, we go one step further and ignore all sorts of constraints that are hard to avoid in physical machines, such as storage size and word length: in the machine we think about -also known as "the Good Lord's Machine"-any integer can be increased by 1. To simplify matters further, we ignore all devices for input and output of information: the value of the input absorbed by a computation is deemed

to be captured by the initial state of the machine -i.e. the state in which the machine starts the computation-, the value of the output is similarly deemed to be captured by the final state of the machine -i.e. the state in which the machine is left upon completion of the computation-.

Our next step is a little bit more radical. In the beginning we were very preoccupied with the machines; as a result, it was viewed as the task of the programs to instruct our machines, and the final state was not only viewed but actually defined as the result of the computation evoked under control of the program. In those days, the semantics of pro-gramming languages were defined in terms of the computational steps that would take place during the executions of the programs, the final state reflecting the cumulative effect of all the steps of a computation. Such an approach is now called "an operational definition" of the semantics.

Nowadays, we are no longer so preoccupied with the machines; we are more interested in our programs and view it as the task of the machines to execute our programs, i.e. to bring themselves, for any given initial state and given program, into a corresponding final state. We are not so interested any more in what happens during the computation, provided it establishes the desired nett effect. Accordingly we shall no longer define the semantics via the defour

of the nett effect of the computations a program may evoke; instead we shall define more directly how for any program in the language initial and final states are connected.

We do so, because such a non-operational definition of semantics has clear technical advantages. For instance, in order to establish the equivalence of two different programs, we can derive for both of them how initial and final states are connected and if those connections are the same, the programs are equivalent. The fact that, when executed, they establish the same nett effect via possibly different computations no longer complicates our reasoning since we don't need to consider the individual computations any more.

(Besides assisting us in reasoning about given programs - for instance to establish their equivalence- the non-operational definition of programming language semantics also serves as a basis for a calculus for the derivation of programs, their required nett effects being given. But that is another story.)

The only things of interest that remain are the initial state, the final state and how a program connects them. As computations no longer enter the picture, we can now forget about machines and treat programs as mathematical objects in their own right, temporarily ignoring that they

admit the interpretation of executable code.

The semantics of a program

One way of trying to capture the semantics of a given program $s$ is to consider the final state as a function of the initial state in which $s$ is started. This way has been followed (extensively), but it suffers from two disadvantages.

The one disadvantage is that there may be initial states for which S, when started, fails to terminate, i.e. the final state, considered as function of the initial one, is not defined for all points of state space. We then have two options, either we pay the price of dealing with what are called "partial functions" - i.e. functions defined on a smaller domain than the one under consideration - or we make them total functions by extending the state space by adding a special "point" - usually called "bottom" - that can be interpreted as "stuck in an endless computation". Both have their disadvantages. (The latter is really a coding trick: it buys the advantage of dealing with total functions at the price of destroying the homogeneity of the state space.)

The other disadvantage is more serious: the approach is really geared to what are called "de

ferministic programs , i.e. programs for which the

determined by the initial state in which the program has been started. For a variety of reasons

• about which probably more later- we would like to include in our considerations nondeterministic

programs as well (e.g. programs that could be

implemented by occasionally tossing a coin).

and such nondeterministic programs don't fit nicely in the functional framework. People ha

tried it in various ways, such as treating the "oin" as some sort of hidden input - again a

coding trick! - or by introducing functions

states to subsets of states. The cleanest approach

along these lines is probably to capture the seman.

tics of a program as a relation between initial and final state; it has at least the advantage

that the relational calculus as such is available. (Experience with the relational calculus has,

however, not been too favourable in this context: firstly, "bottom" enters the picture constantly.

Secondly, many quantifications over the state space have to be written down explicitly, and, thirdly,

it has proved to be conducive to errors: in the relational calculus the two arguments of a

relation are treated on the same footing and,

as a result, the essential asymmetry between

initial and final state is insufficiently reflected.)

The long and the short of it is that we want to

capture the semantics of a program differently.

Consider a program $S$ and a predicate $X$ on the (final) state space; the predicate $X$ then defines a dichotomy of the state space: in those states in which $X$ does not hold, if $X$ holds. Then each possible execution of $S$ falls in precisely one of the following three - mutually exclusive - classes:

"S gets stuck": the execution of S fails to terminate -does not lead to a final state-

"Stablishes X": the execution of S terminates -leads to a final state-in a state in which $X$ holds

"Stablishes $¬ X$ ": the execution of $S$ terminates - leads to a final state - in a state in which $¬ X$ holds.

The three classes are clearly mutually exclusive and exhaustive. Note that, since there are no states in which false holds, the class "s establishes false" had better be empty.

We now take the view that we know everything that is to be known about the semantics of $S$ if we know for any predicate $X$ and for any initial state which of the three executions are possible or, equivalently, which of the three executions are impossible.

To each class corresponds a dichotomy of the initial state space, viz. whether in such a state as starting point an execution of that class is possible or not. We characterize -as always- these dichotomies by predicates. The first one, corresponding to "s gets stuck" is independent of $x$ .

TS : holds in all initial states for which

"St gets stuck" is impossible

TST : holds in all initial states for which

"S gets stuck " is possible.

-1wlp $\left(S,X\right)$ : holds in all initial states for which

"Stablishes $x''$ is impossible

wlp ${}^{ * }\left( {S,X}\right)$ : holds in all initial states for which

"Stablishes $x''$ is possible

(and similarly for $x$ : just replace $x$ by $x$ ).

From the fact that the execution class "s establishes false" had better be empty , we deduce from the above that wlp had better satisfy [wlp*(S, False) = false] or, equivalently, [wlp(S, true) = true], or, for short

(0) $\left\lbrack {\operatorname{wlp}\left( {S,\text{true}}\right) }\right\rbrack$

Moreover, since $\left\lbrack {{w}{p}\left( {S,X}\right) \equiv {7}^{ * }{w}{p}{}^{ * }\left( {S,{7X}}\right) }\right\rbrack$ we deduce

wlp(S,X): holds in all initial states for which "s establishes "x" is impossible

But since the three classes are exhaustive and mutually exclusive, we can also formulate

wlp(S,X) : holds for all initial states for which for which the possibilites are restricted to "s gets stuck" and "s establishes X".

or holds for all initial states for which s establishes X if it does not get stuck.

Since an execution belonging to both classes "s establishes X" and "s establishes Y" belongs to the class "s establishes XY" as well, and vice versa, i.e.

[ w l p (S, X) \wedge w l p (S, Y) \equiv w l p (S, X \wedge Y) ]

the predicate transformer wlp(S,?) had better be conjunctive, and in view of (0) even universally so.

In the sequel we shall define -recursively via the grammar - for any program $S$ of a model programming language wlp(S,?) . In view of the above we accept the obligation to prove for each extension of the language that Theorem 4.0 continues to hold.

Theorem 4.0 For any program $s$ , the predicate transformer wlp $(S, ?)$ is universally conjunctive.

Its proof will be distributed through this monograph.

The second predicate transformer associated with

[ w p (S, X) \equiv T S \wedge w l p (S, X) ]

from which we derive, by substituting $x =$ true, on

[ w p (S, t r u e) \equiv T S ]

The name TS can thus be eliminated; it is customary to define the predicate transformer $w_{p}(S,?)$ by

(1) $\left\lbrack {{wp}\left( {S,X}\right) \equiv {wp}\left( {S,{true}}\right) ∧ w\rbrack p\left( {S,X}\right) }\right\rbrack$

In view of the definition of TS we have wp (S,X): holds for all initial states in which "S establishes X" is guaranteed (being the only class) wp(S,X): holds for all initial states in which "S gets stuck" or "S establishes ¬X" are among the possibilites, i.e. all initial states in which S might fail to establish X

(The names ${wp}$ and ${Wp}$ are short for "weakest precondition" and "weakest liberal precondition" respectively. These names having been in use now for more than a decade , we shall stick to them.)

Since $S$ can be started in any initial state, and the ensuing execution falls in one of the three classes, everywhere in state space executions from at least one of the three classes had better be possible, i.e.

[ ¬ T S \vee w l p ^ {} (S, X) \vee w l p ^ {} (S, ¬ X) ]

should hold. Thanks to [TS ≡ wp(true) ], de Morgan's Law and the definition of the conjugate, the above condition is equivalent to

$\left\lbrack {\operatorname{wp}\left( {S,\text{true}}\right) ∧ \operatorname{wlp}\left( {S,1X}\right) ∧ \operatorname{wlp}\left( {S,X}\right) \equiv {\$ a}^{\prime }\right\rbrack$ ;

$\left\lbrack {\operatorname{wp}\left( {S,\text{true}}\right) ∧ \operatorname{wlp}\left( {S,\text{false}}\right) \equiv \text{false}}\right\rbrack$ which,thanks to (1) can be shortened to

[ w p (S, \mathsf {f a l s e}) \equiv \mathsf {f a l s e} ].

In the sequel we shall define for any program besides the predicate transformer wlp (S,?) the predicate wp(S, true) as well -and hence (see (1)) the predicate transformer wp (S,?)- . In view of the above we accept the obligation to prove for each extension of the language that Theorem 4.1 continues to hold.

Theorem 4.1 For any program $s$

[ w p (S, \mathsf {f a l s e}) \equiv \mathsf {f a l s e} ]

It's proof will be distributed through this mono-graph.

Note Theorem 4.1 is better known as "The law of the Excluded Miracle". (End of Note.)

In the remainder of this chapter we shall define the semantics of a number of statements with which we can write what is known as "straight-line programs" -briefly: programs without repetition or, more generally, recursion- We shall define them by giving for them the predicate transformer wlp(S,?) and the predicate wp(S, true) ; in accordance with the above we shall prove for them the universal conjunc- tivity of wlp (Theorem 4.0) and The law of the Excluded Miracle (Theorem 4.1). In view of later applications, we shall give their disjunctivity properties as well.

S = - h a v o c

Def. [wp(havoc, true) = true]

[ w l p (h a v o c, X) \equiv [ X ] ]

Cms. [wp (havoc, X) ≡ [X]]

This statement is the first one to illustrate a direct

consequence of (1): for a statement S with [wp(S, true)] , the predicate transformers wip and wlp are the same. For reasons that will be. come clear in a moment, most commercially available programming languages do not include the statement havoc (at least not intentionally); its execution should bring the machine in an arbitrary state, i.e. should assign to each variable spanning the state space an unpredictable value. Yet it is good to know the statement havoc , as it provides an important counterexample.

Proof 4.0 for havoc. On account of Lemma 3.10, wlp(havoc,?) is universally conjunctive. (End of Proof 4.0 for havoc.)

Proof 4.1 for havoc

\begin{array}{l} w p (h a v o c, f a l s e) \ = {(1) } \ w p (h a v o c, f r u e) ∧ w l p (h a v o c, f a l s e) \ = {\mathrm {d e f . o f h a v o c} } \ t r u e ∧ [ f a l s e ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ f ^ {p a s e} \ \end{array}

(End of Proof 4.1 for h a v o c .)

Being universally conjunctive, wlp (havoc, ?) is monotonic, but that is, in general, its only disjunctivity property since, in general, wlp (havoc, ?) is neither disjunctive nor or-continuous.

For a state space large enough that there exists an $X$ such that $¬ [X] ∧ ¬ [¬ X]$ - i.e. a state space of 2 points, i.e. spanned by a single bodean variable suffices - we observe for such an $X$

\begin{array}{l} w l p (h a v o c, X \vee ¬ X) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ = {\mathrm {d e f . o p h a v o c} } [ \mathrm {t r u e} ] \ = {p r e d i c a t e c a l c u l u s } \ = {\mathrm {a s s u m p t i o n a b o u t} X } \ ≠ {d e m o r g a n } \ = {\mathrm {d e f . o f h a v o c} } \ \end{array}

w l p (h a v o c, X) \sim w l p (h a v o c, \tau X)

hence havococ is in general not disjunctive.

For a state space spanned by a single integer variable $x$ , the predicates $X.i$ given by $x≤ i$ form a monotonic sequence. Square brackets corresponding to universal quantification over $x$ , we have

\begin{array}{l} w l p (h a v o c, (\underline {{E}} i:: X. i)) \ = \left{ \begin{array}{l} d e f. o f h a v o c \ [ (E i: X, i) ] \end{array} \right} \ ≠ {\mathrm {d e f . o f} X, i } (\equiv_ {i:} [ X, i ]) \ \end{array}

\begin{array}{l} = {\mathrm {d e f . o f h a v o c} } \ (E _ {i}: w l p (h a v o c, X. i)) \ \end{array}

hence havoc is in general not or-continuous.

Note. In the jargon, hovoc is a nondeterministic statement. (It is even the most nondeterministic one of all.) In an infinite state space it is unboundedly nondeterministic, and the above argument shows that unbounded nondeterminism excludes or-continuity of wlp. (End of Note.)

S = a b o r t

Def. [wp(abort, true) = false]

[ w | p (a b o r t, X) \equiv t r u e ]

Cons. [wp (a bort, X) = false]

For reasons that will become clear in a moment, all commercially available programming languages include the statement "abort in one form or another (sometimes quite unintentionally so): it corresponds to the statement whose execution is guaranteed to fail to terminate properly. It is sometimes known under names such as "stop", "alarm", "error message"; as we shall see later we have defined it to be semantically equivalent to the nonterminating repetition.

Proof 4.0 for abort. On account of lemma 3.12, wlp (abort, ?) is universally conjunctive. (End of Proof 4.0 for abort.)

Proof 4.1 forabort

true

\begin{array}{l} = {\mathrm {c o n s e q u e n c e o f d e f . o f a b o r t} } \ (\underline {{A}} X:: [ w p (a b o r t, X) \equiv f a l s e ]) \ ⇒ {\mathrm {i n s t a n t i a t i o n} } \ [ w p (a b o r t, f a l s e) \equiv f a l s e ] \ (E n d o f P r o o f 4. 1 f o r a b o r t.) \ \end{array}

Furthermore we conclude on account of Lemma 3.12 that wlp (abort, ?) is unboundedly disjunctive and that wp (abort, ?) is universally disjunctive.

Note. Alternatively we could have defined the semantics of abort by postulating that its predicate transformers satisfy Theorems 4.0 and 4.1, plus

[ w l p (a b o r t, f a l s e) \equiv \mathrm {t r u e} ]

which is the formal expression of the circumstance that all executions of abort fail to terminate. (End of Note.)

S = s k i p

Def. [wp (skip, true) = true]

[ w | p (s k i p, X) \equiv X ]

C o n s. [ w p (s k i p, X) \equiv X ]

The statement skip is known under many names, such as "the empty statement", "no-op", "continue"; in the syntax of ALGOL 60 the mistake was made of representing it by no character at all.

Since [wp skip, true)], the predicate transformers wp (skip, ?) and wlp (skip, ?) are the same.

Proof 4.0 for skip. On account of Lemma 3.11, wlp (skip, ?) is universally conjunctive. (End of Proof 4.0 for skip.)

\begin{array}{l} \mathrm {P r o o f 4 . 1 p o r s k i p}. \ \mathbf {f r u e} \ = {\mathrm {c o n s e q u e n c e o f d e f . o f s k i p 3} \ (\underline {{A}} X: [ w p (s k i p, X) \equiv X ]) \ ⇒ {\mathrm {i n s t a n t i a t i o n} } \ [ w p (s k i p, f a l s e) \equiv f a l s e ] \ (E n d o f P r o o f 4. 1 f o r s h i p.) \ \end{array}

Furthermore we conclude on account of Lemma 3.11 that wlp (skip,?) and wp (skip,?) are universally disjunctive.

Note. For the definition of the semantics of skip it would have sufficed to postulate

[ w p (s k i p, X) \equiv X ]

which is the formal expression of the circumstance that each execution of ship leaves the machine

state unaffected. (End of Note.)

S = \prime \prime x := E ^ {\prime \prime}

Def. [wp ( " $x := {E}_{p}^{n}$ true) = true]

[ w | p (” x := E", X) = X _ {E} ^ {x} ]

[{w}{p}\left( {{}^{\prime \prime }x = {E}^{\prime \prime },X}\right) \equiv {X}{E}^{x}\rbrack)

Remark on notation If the statement is more complica- ed than a single identifier and should be parsed to retrieve its components, it is customary to surround it by a pair of quotes so as to make clear that the following comma does not belong to it. Though it is not a custom we would like to defend, we shall stick to it the few times it is applicable. (End of Remark on notation.)

The above gives the semantics of the assignment statement in its simplest form. On account of [wp ("x:=E, true)], its wlp and wp are again the same predicate transformer. The definition of wp("x:=E, true) adopted here excludes that the execution of x:=E gets stuck, i.e. requires E to be a total expression. It is tempting to replace its definition by

[ w p (” x := E ”, t r u e) \equiv d e f. E ]

where def. $E$ does not necessarily satisfy [def.E]

and holds precisely in those states for which $E$ is defined. We have resisted that temptation since the introduction of def.E in the definition of the assignment statement does not really solve the problem of partially defined expressions. For instance, what would the value of $X_E^x$ be where $E$ is not defined? And also, if we wish to capture that evaluation of $E$ might lead to a nonterminating computation, shouldn't we also try to capture the possibility that the evaluation of $E$ leads to a nondeterministic process?

We would rather take here the opportunistic view that the use of partially defined expressions is the result of not caring to define them totally (i.e. "outside our domain of interest"), and that the problem of how to prevent that laziness -or "shorthand" if you prefer- from leading us astray in our reason-. ing is a more general problem of formal mathematics that should not clutter up our definition of the semantics of the assignment statement. How not to apply definitions outside their domain of validity is a general problem probably outside the scope of this monograph in which, at least for the time being, all expressions will be total.

Proof 4.0 for " $x \mathrel{\text{:=}} E$ ". On account of Lemma 3.26, wlp (" $x \mathrel{\text{:=}} E$ ", ?) is universally conjunctive. (End of Proof 4.0 for " $x \mathrel{\text{:=}} E$ ".)

\begin{array}{l} \mathrm {P r o o f 4 . 1 f o r} x := E \ w p (x := E ^ {\prime}, \mathrm {f a l s e}) \ = {\mathrm {c o n s e q u e n c e o p d e f . , w i t h} X := \mathrm {f a l s e} } \ = {\mathrm {d e p . o p s u b s t i l u t i o n} } \ f ^ {p a s e} \ \end{array}

(End of Proof 4.1 for " $x$ : $= E$ ".)

We point out that the $x$ in the above need not be one of the programs "concrete" variables, it could be a pair of them, say $(y,z)$ . The assignment statement could then be written

y, z := E _ {0}, E _ {1}

and ${X}{E}^{x}$ would have to be replaced by ${X}{E0,E1}^{y,z}$ , the multiple substitution (sometimes called "the "simultaneous" substitution). This is extendible to

n - fuples.

Disjunctivity missing

S = S _ {0}; S _ {1}

Def. [wp("So;Si", true)] =

w p (S _ {0}, w p (S _ {1}, t r u e)) ]

\begin{array}{l} [ w l p (" s o; s _ {1} ", x) \equiv \ w l p (S _ {0}, w l p (S _ {1}, X)) ] \ \end{array}

Cons. $\left\lbrack {{wp}\left( {{}^{\prime \prime }{So};{S}_{1}{}^{\prime \prime },{X}}\right) \equiv }\right.$

w p (S 0, w p (S 1, X)) ]

Because the Consequence is not immediately obvious we give first the

Proof of Consequence

w p \left(" S _ {0}; S _ {1} ", X\right)

= {(1) }

w p (" S O; S 1", t r u e) ∧ w l p (" S O; S 1", X)

= {\mathrm {d e p . o p} ^ {} S _ {0}; S _ {1} ^ {} }

w p (S _ {0}, w p (S _ {1}, f r u e)) ∧ w l p (S _ {0}, w l p (S _ {1}, X))

= {(1) }

w p (S _ {0}, t r u e) \wedge w l p (S _ {0}, w p (S _ {1}, t r u e)) \wedge w l p (S _ {0}, w l p (S _ {1}, X))

= {w l p (S O, ?) i s c o n j u n c t i v e }

w p (S O, t r u e) ∧ w l p (\tilde {S O}, w p (S 1, t r u e) ∧ w l p (S 1, X))

= {(1) }

w p (S 0, f r u e) ∧ w l p (S 0, w p (S 1, X))

= {(- 1) ^ {3} }

w p (S 0, w p (S 1, X))

(End of Proof of Consequence.)

Compared to our previous definitions of the semantics of statements, our definition of the semantics of the semicolon introduces a novelty in the sense that the semantics of ${S}{0};{S}{1}$ is given terms of those of so and S1 : the properties of the predicate transformer wlp ("So; Si", ?) depend on those of wlp(So,?) and wlp(S1, ?). So we cannot prove that wlp("So; Si", ?) is "always" universally conjunctive: locally we can only give Proof 4.0 for "So; Si" On account of Lemma 3.14,

wlp ("So; Si", ?) is universally conjunctive if both wlp (S0,?) and wlp (Si,?) are. (End of Proof 4.0 for "So; Si".)

We are in a similar position with

Theorem 4.1 For "So; Si". "So; Si" satisfies the Law of the Excluded Miracle if both So and Si do.

Proof 4.1 For "So; S1"

\begin{array}{l} w p (" S 0; S 1", \mathrm {f a l s e}) \ = {\mathrm {c o n s e q u e n c e} o p d e f. " S o; S 1" \mathrm {w i t h} X := \mathrm {f a l s e} } \ w p (S _ {0}, w p (S _ {1}, f a l s e)) \ = {\mathrm {T h e o r e m} 4. 1 \mathrm {h o l d s f o r} S _ {1} } \ w p (s o, f a l s e) \ = {\mathrm {T h e o r e m} 4. 1 \mathrm {h o l d s p o r} 5 0 } \ p a s e. \ \end{array}

(End of Proof 4.1 for "So, Si".)

The above are only the induction steps. However, for each statement introduced all by itself we show the validity of Theorems 4.0 and 4.1; for each statement composed of other statements we show - as we just did- that the Theorems 4.0 and 4.1 are valid for the composite provided they are valid for the components. Via induction ("over the grammar", as the jargon says) we are then allowed to conclude that Theorems 4.0 and 4.1 are valid for all statements of the programming language.

From Lemma 3.14 we furthermore derive that

wlp("So; Si",?) enjoys all disjunctive properties shared by wlp(S0,?) and wlp(S1,?) , and similarly for wp

[S = {1F}]

In this monograph, IF is used to denote "alternative constructs" of the form

\begin{array}{l} i f B O \rightarrow S O F i \ i F B O \rightarrow S O i ^ {\prime} B 1 \rightarrow S 1 F _ {i} \ i f B _ {0} \rightarrow S _ {0} j B _ {1} \rightarrow S _ {1} j B _ {2} \rightarrow S _ {2} i, \ \end{array}

in general $\rho \left( {\mathbb{I}\mathbb{i} : \mathbb{B}.i \rightarrow \mathbb{S}.i}\right) {F}_{i}$ ,where the $i$ are taken from a usually non-empty,usually finite bag.

With the abbreviation ${BB}$ given by $\left\lbrack {{BB} \equiv \left( {{E}{i} : {B}{i}}\right) }\right\rbrack$ ,we have:

Def. $\left\lbrack {{wp}\left( {I{F}{1}{T}^{1}E}\right) \equiv B{B}{1} ∧ \left( {{A}{i} : ¬ {B}{i}Vw\rbrack \left( {{S}_{i},{T}^{1}E}\right) }\right) }\right\rbrack$

[ w l p (I F, X) \equiv (\underline {{A}} i: ¬ B. i \vee w l p (S. i, X)) ]

Cons. $\left\lbrack {{wp}\left( {IF,X}\right) \equiv {BB} ∧ \left( {\underline{A} : : 7B : i \vee {wp}\left( {S.i,X}\right) }\right) }\right\rbrack$ .

(In this case, the verification that the Consequence follows from the Definitions is again left to the reader.

We have to prove Theorem 4.0 for IF Predicate transformer wlp(If,?) is universally conjunctive if all the wlp(Si,?) are.

Proof 4.0 for IF . Because disjunction distributes

over universal quantification

$\left\lbrack {p,X \equiv g.X \vee Y}\right\rbrack$ enjoys each conjunctivily enjoyed

by $g $ - Note: should this have been a lemma of

Chapter 3 , e.g. a replacement of Lemma 3.13? -

1. i v wlp(5.i,?) is universally conjunctive

if $w \mid p\left( {5,i,\widehat{.}}\right)$ is. From Lemma 3.15 it now

follows that wlp (IF, ?) is universally conjunctive.

if all Wlp(S.i,?) are.

(End of Proof 4.0 for ${IF}$ .)

Theorem 4.1 for IF . If satisfies the law of

the Excluded Miracle if all the 's i do

Proof 4.1 For ${IF}$

\begin{array}{l} w p (I F, \mathrm {f a l s e}) \ = {\mathrm {c o n s e q u e n c e o f d e p . I F w i t h} X := \mathrm {f a l s e} } \ B B \wedge (¬ A _ {i}: ¬ B. i \vee w p (S. i, P a l s e)) \ = {\mathrm {M i r a c l e E x c l u d e d f o r a l l S . i} } \ B B \wedge (A _ {i}: ¬ B. i) \ = {\mathrm {d e f . o p} B B } \ B B \wedge ¬ B B \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ p a i s e \ \end{array}

(End of Proof 4.1 for IF.)

From lemma 3.25 it follows that $w|p\left( {{IF},?}\right)$

is or-continuous provided all the wlp (S.i,?)

are and their number is finite. Admission of

an infinite number of alternatives between if and ${F}_{L}$

in general destroys or-continuity! Since conjunction distributes over existential quantification, $wp(If,?)$ is or-continuous if $wlp(If,?)$ is

And this concludes our treatment of straight-line programs.

Comments. In the previous chapter, the formula

For Lemma 3.13 I propose

Lemma 3.13. Let $\mathcal{F}$ be given by $[P, X \equiv g, X \wedge Y]$ ; for arbitrary $Y$ , $P$ enjoys each junctivity enjoyed by $g$ , universal conjunctivity excepted.

Proof 3.13 We observe for non-empty $V$ over which $g$ is conjunctive and any $W$ over which $g$ is

p. (A X: X \in V: X)

= {\mathrm {d e f . o p} P }

g. (\underset {\sim} {A} X: \underset {\sim} {X} \in V: X) \wedge Y

= {g \mathrm {c o n j u n c t i v e} \mathrm {o v e r} V }

(\underset {\sim} {A} X: X \in V: g. X) \wedge Y

= {V n o t. e m p l y }

(\underline {{A}} X: X \in V: g _ {X} X ∧ Y)

= {\mathrm {d e f . o p} \tilde {P} }

(¬ X: X \in V: P X)

\begin{array}{l} P (E X: X \in W: X) \ = {\mathrm {d e f . o p} P } \ g. (E X: X \in W: X) ∧ Y \ = {g \mathrm {d i s j u n c t i v e o v e r} W } \ (E \times : X \in W: g \cdot X) ∧ Y \ = {\mathrm {d i s t r i b u t i o n} } \ (E X: X \in W: g. X ∧ Y) \ = {\mathrm {d e f . o f} p } \ (E X: X \in W: P X) \ \end{array}

(\mathrm {E n d o f P r o o f o f 3 . 1 3})

This draft is still young and so I am reasonably pleased with it. I had a few problems, e.g. how much to elaborate the remark at the bottom of EWD910-0: I know cultures in which no amount of elaboration would suffice, but also cultures in which the remark is super fluous.

Page 0-5 gave rise to a lecture that was greatly appreciated by the audience, which confirms to me such considerations should be included. Pages 6-10 had to be done very slowly, otherwise people get utterly confused about "it is impossible that something will not happen". The negations get a little bit overpowering; it is therefore good that these considerations are confined to a few pages. (Is this the reason why the relational calculus has invited mistakes?)

On p.11, a subchapter heading is missing. The rest is a bit enumerative, but that seems the nature of the topic.

Austin, 11 March 1985

Prof. dr. Edsger W. Dgksra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 United States of America