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
Copyright Notice
The following manuscript
EWD 472: Guarded commands, non-determinacy and formal derivation of programs
was published in Commun. ACM 18(1975), 8: 453-457.
It is reproduced here by permission.
Guarded commands, non-determinacy and formal derivation of programs.
by Edsger W.Dijkstra *) | |
*) Author’s address: | BURROUGHS |
Plataanstraat 5 | |
NUENEN - 4565 | |
The Netherlands. |
Abstract. So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow non-deterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state. For the formal derivation of programs expressed in terms of these constructs, a calculus will be shown.
Keywords. programming languages, sequencing primitives, program semantics, programming language semantics, non-determinacy, case-construction, repetition, termination, correctness roof, derivation of programs, programming methodology.
CR-category: 4.20, 4.22.
Guarded commands, non-determinacv and formal derivation of programs.
1. Introduction.
In section 2, two statements, an alternative construct and a repetitive construct will be introduced, together with an intuitive (mechanistic) definition of their semantics. The basic building block for both of them is the so-called “guarded command”, a statement list prefixed by a boolean expression: only when this boolean expression is initially true, is the statement list eligible for execution. The potential non-determinacy allows us to map otherwise (trivially) different programs on the same program text, a circumstance that seems largely responsible for the fact that now programs can be derived in a more systematic manner then before.
In section 3, after a prelude defining the notation, a formal definition of the semantics of the two constructs will be given, together with two theorems for each of the constructs (without proof).
In section 4, it will be shown, how upon the above a formal calculus
for the derivation of programs can be founded. We would like to stress
that we do not present “an algorithm” for the derivation of programs: we
have used the term “a calculus” for a formal discipline —a set of rules—
such that, if applied successfully
1) it will have derived a correct program
2) it will tell us that we have reached such a goal.
(We use the term as in “integral calculus”.)
2. Two statements made from guarded commands.
If the reader accepts “other statements” as indicating, say, assignment statements and procedure calls, we can give the relevant syntax in BNF [2]. In the following we have extended BNF with the convention that the braces “{...}” should be read as: “followed by zero or more instances of the enclosed”.
< guarded command > ::= < guard > → < guarded list >
< guard > ::= < boolean expression >
< guarded list > ::= < statement > {; < statement >}
< guarded command set > ::= < guarded command > {▯ < guarded command >}
< alternative construct > ::= if < guarded command set > fi
< repetitive construct > ::= do < guarded command set >od
< statement > ::= < alternative construct > | < repetitive construct > | “other statements” .
The semicolons in the guarded list have the usual meaning: when the guarded list is selected for execution its statements will be executed successively in the order from left to right; a guarded list will only be selected for execution in a state such that its guard is true. Note that a guarded command by itself is not a statement: it is a component of a guarded command set from which statements can be constructed. If the guarded command set consists of more than one guarded command, they are mutually separated by the separator “▯” ; our text is then an arbitrarily ordered enumeration of an unordered set, i.e. the order in which the guarded commands of a set appear in our text is semantically irrelevant.
Our syntax gives two ways for constructing a statement out of a guarded command set. The alternative construct is written by enclosing it by the special bracket pair: if ... fi“. If in the initial state none of the guards is true, the program will abort, otherwise an arbitrary guarded list with a true guard will be selected for execution.
Note. If the empty guarded command set were allowed ”if fi“ would be semantically equivalent to ”abort“ . (End of note.)
An example —illustrating the non-determinacy in a very modest fashion— would be the program that for fixed x and y assigns to m the maximum value of x and y :
if x ≥ y → m:= x | ||
▯ y ≥ x → m:= y | ||
fi . |
The repetitive construct is written down by enclosing a guarded command set by the special bracket pair do ... od” . Here a state in which none of the guards is true will not lead to abortion but to proper termination; the complementary rule, however, is that it will only terminate in a state in which none of the guards is true: when initially or upon completed execution of a selected guarded list one or more guards are true, a new selection for execution of a guarded list with a true guard will take place, and so on. When the repetitive construct has terminated properly, we know that all its guards are false.
Note. If the empty guarded command set were allowed “do od” would be semantically equivalent to “skip” . (End of note.)
An example —showing the non-determinacy in somewhat greater glory— is the program that assigns to the variables q1, q2, q3 and q4 a permutation of the values Q1, Q2, Q3 and Q4, such that q1 ≤ q2 ≤ q3 ≤ q4 . Using concurrent assignment statements for the sake of convenience, we can program
q1, q2, q3, q4 := Q1, Q2, Q3, Q4; | ||
do ql > q2 → ql, q2 := q2, ql | ||
▯ q2 > q3 → q2, q3 := q3, q2 | ||
▯ q3 > q4 → q3, q4 := q4, q3 | ||
od |
To conclude this section we give a program where not only the computation but also the final state is not necessarily uniquely determined. The program should determine k such that for fixed value n (n >0) and a fixed function f(i) defined for O ≤ i < n , k will eventually satisfy:
0 ≤ k < n and (∀i: 0 ≤ i < n: f(k) ≥ f(i)) |
k:= 0; j:= 1; | |||
od j ≠ n → if f(j) ≤ f(k) → j:= j + 1 | |||
▯ f(j) ≥ f(k) → k:= j; j:= j + 1 | |||
fi | |||
od |
Only permissible final states are possible and each permissible final state is possible .
3. Formal definition of the semantics.
3.1. Notational prelude.
In the following sections we shall use the symbols P, Q and R to denote (predicates defining) boolean functions defined on all points of the state space; alternatively we shall refer to them as “conditions”, satisfied by all states for which the boolean function is true. Two special predicates that we denote by the reserved names “T” and “F” play a special role: T denotes the condition that, by definition, is satisfied by all states, F denotes, by definition, the condition that is satisfied by no state at all.
The way in which we use predicates (as a tool for defining sets of initial or final states) for the definition of the semantics of programming language constructs has been directly inspired by Hoare [1], the main difference being that we have tightened things up a bit: while Hoare introduces sufficient pre-conditions such that the mechanisms will not produce the wrong result (but may fail to terminate), we shall introduce necessary and sufficient —i.e. so-ca1led “weakest”— pre-conditions such that the mechanisms are guaranteed to produce the right result.
More specifically: we shall use the notation “wp(S, R)”, where S denotes a statement list and R some condition on the state of the system, to denote the weakest pre-condition for the initial state of the system such that activation of S is guaranteed to lead to a properly terminating activity leaving the system in a final state satisfying the post-condition R . Such a “wp” —which is called “a predicate transformer”, because it associates a pre-condition to any post-condition R — has, by definition, the following properties .
1) For any S, we have for all states
wp(S, F) = F |
2) For any S and any two post-conditions, such that for all states
P ⇒ Q |
wp(S, P) ⇒ wp(S, Q) . |
(wp(S, P) and wp(S, Q)) = wp(S, P and Q). |
(wp(S, P) or wp(S, Q)) = wp(S, P or Q) . |
Together with the rules of propositional calculus and the semantic definitions to be given below, the above four properties take over the role of the “rules of inference” as introduced by Hoare [1].
We take the position that we know the semantics of a mechanism S sufficiently well if we know its predicate transformer, i.e. can derive wp(S, R) For any post-condition R.
Note. We consider the semantics of S only defined for those initial states for which has been established a priori that they satisfy wp(S, T), i.e. for which proper termination is guaranteed (even in the face of possibly non-deterministic behaviour); for other initial states we don’t care. By suitably changing S, if necessary, we can always see to it that wp(S, T) is decidable.(End of note.)
Example 1. The semantics of the empty statement, denoted by ’“skip”, are given by the definition that for any post-condition R, we have
wp(“skip”, R) = R . |
Example 2. The semantics of the assignment statement “x:= E” are given by
wp(“x:= E”, R) = R_{E}^{x} |
Example 3. The semantics of the semicolon “;” as concatenation operator are given by
wp(“S1; S2”, R) = wp(S1, wp(S2, R)) . |
3.2. The alternative construct.
In order to define the semantics of the alternative construct we define two abbreviations. Let “IF” denote
if b_{1} → SL_{1} ▯ ... ▯ B_{n} → SL_{n} fi ; |
(∃i: 1 ≤ i ≤ n: B_{i}) ; |
wp(IF, R) = (BB and (∀i: 1 ≤ i ≤ n: B_{i} ⇒ wp(SL_{i}, R)) . |
(The first term “BB” requires that the alternative construct as such will not lead to abortion on account of all guards false, the second term requires that each guarded list eligible for execution will lead to an acceptable final state.) From this definition we can derive —by simple substitutions—
Theorem 1. From
(∀i: 1 ≤ i ≤ n: (Q and B_{i}) ⇒ wp(SL_{i}, R)) for all states |
(Q and BB) ⇒ wp(IF, R) holds for all states . |
Let “t” denote some integer function, defined on the state space, and let “wdec(S, t)” denote the weakest pre-condition such that activation of S is guaranteed to lead to a properly terminating activity leaving the system in a final state such that the value of t is decreased by at least 1 (compared to its initial value). In terms of “wdec” we can formulate the very similar
Theorem 2. From .
(∀i: 1 ≤ i ≤ n: (Q and B_{i}) ⇒ wdec(SL_{i}, t)) for all states |
(Q and BB) ⇒ wdec(IF, t) holds for all states. |
wp(S, t ≤ t0) |
wdec(S, t) = (tmin(X) ≤ t(X) - 1) = (tmin(X) < t(X)) . |
3.3. The repetitive construct.
As is to be expected, the definition of the repetitive construct
do b_{1} → SL_{1} ▯ ... ▯ B_{n} → SL_{n} od |
Let | H_{0}(R) = (R and non BB) |
and for k > 0: | H_{k}(R) = (wp(IF, H_{k-1}(R)) or H_{0}(R)) |
wp(DO, R) =(∃k: k ≥ 0: H_{k}(R)) . |
Theorem 3. If we have for all states
(P and BB) ⇒ (wp(IF, P) and wdec(IF, t) and t ≥ 0) |
P ⇒ wp(DO, P and non BB) . |
Because T is the condition by definition satisfied by all states, wp(S, T) is the weakest pre-condition guaranteeing proper termination for S . This allows us to formulate an alternative theorem about the repetitive construct, viz.
Theorem 4. From
(P and BB) ⇒ wp(IF, P) for all states, |
(P and wp(DD, T)) ⇒ wp(DO, P and non BB) . |
4. Formal derivation of programs.
The formal requirement of our program performing “m:= max(x, y)” —see above— is that for fixed x and y it establishes the relation
R: | (m = x or m = y) and m ≥ x and m ≥ y . |
Now the Axiom of Assignment tells us that “m:= x” is the standard way of establishing the truth of “m = x” for fixed x, which is a way of establishing the truth of the first term of R. Will “m:= x” do the job? In order to investigate this, we derive and simplify
wp(“m:= x”, R) = (x = x or x = y) and x ≥ x and x ≥ y | ||
= x ≥ y . |
if x ≥ y → m:= x fi |
wp(“m:= y”, R) = y ≥ x ; |
if x ≥ y → m:= x | ||
▯ y ≥ x → m:= y | ||
fi |
As an example of the deriviation of a repetitive construct we shall derive a program for the greatest common divisor of two positive numbers, i.e. for fixed, positive X and Y we have to establish the final relation
x = gcd(x, v) . |
The formal machinery only gets in motion, once we have chosen our invariant relation and our variant function. The program then gets the structure “establish the relation P to be kept invariant”;
do “decrease t as long as possible onder invariance | ||
of P” od . |
Suppose that we choose for the invariant relation
P: | gcd(X, Y) = gcd(x, y) and x > O and y > 0 |
x:= X; y:= Y . |
The most general “something” to be done under invariance of P is of the form
x, y:= E1, E2 |
(P and B) ⇒ wp(“x, y := E1, E2”, P) | ||
= (gcd(X, Y) = gcd(E1, E2) and E1 >0 and E2 >0) . |
Because the guard must be a computable boolean expression and should not contain the computation of gcd(X, Y) —for that was the whole problem!— we must see to it that the expressions E1 and E2 are so chosen. that the first term
gcd(X, Y) = gcd(E1, E2) |
gcd(x, y) = gcd(E1, E2) . |
gcd(x, y) = gcd(x - y, y) |
x:= x - y . |
wp(“x:= x - y”, P) = (gcd(X, Y) = gcd(x - y, y) and x - y > 0 and y > 0) |
x > y |
t = x + y . |
wp(“x:= x - y”, t ≤ t0) = | |
wp(“x:= x - y”. x + y ≤ t0) = (x ≤ t0) |
tmin = x ; |
wdec(“x:= x - y”, t) = (x < x + y) = (y > 0) . |
The requirement of monotonic decrease of t imposes no further restriction of the guard because wdec(“x:= x - y”, t) is fully implied by P and we come at our first effort
x:= X; y:= Y; | |
do x > y → x:= x - y od . |
Alas, this single guard is insufficient: from P and non BB we are not allowed to conclude x = gcd(X, Y). In a completely analogous manner, the alternative y:= y - x will require as its guard y > x and our next effort is
x:= X; y:= Y; | ||
do x > y → x:= x - y | ||
▯ y > x → y:= y - x | ||
od . |
Now the job is done, because with this last program non BB = (x = y) and (P and x = y) ⇒ (X = gcd(X, Y) because gdc(x, x) = x .
Note. The choice of t = x +2y and the knowledge of the fact that the gcd is a symmetric function could have led to the program
x:= X; y:= Y; | ||
do x > y → x:= x - y | ||
▯ y > x → x, y:= y, x | ||
od . |
In both cases the final game has been to find a large enough set of such guarded lists that BB, the disjunction of their guards, was sufficiently weak: in the case of the alternative construct the purpose is avoiding abortion, in the case of the repetitive construct the goal is getting BB weak enough such that P and non BB is strong enough to imply the desired post-condition R .
It is illuminating to compare our first version of Euclid’s Algorithm with what we would have written down with the traditional clauses;
x:= X; y:= Y; (version A) | |
while x ≠ y do if x > y then x:= x - y else y:= y - x od od |
x:= X; y:= Y; (version B) | |||
while x ≠ y do while x > y do x:= x - y od ; | |||
while y > x do y:= y - x od | |||
od |
In the fully symmetric version with the guarded commands the algorithm has been reduced to its bare essentials, while the traditional clauses force us to choose between versions A and B (and others), a choice that can only be justified by making assumptions about the time taken for tests and about expectation values for traversal frequencies. (But even taking the time taken for tests into account, it is not clear that we have lost: the average number of necessary tests per assignment ranges with guarded commands from 1 to 2, equals 2 for version A and ranges from 1 to 2.5 for version B. If the guards of a guarded command set are evaluated concurrently —nothing in our semantics excludes that— the new version is time-wise superior to all the others.) The virtues of the case-construction have been extended to repetition as well.
5. Concluding remarks.
The research, the outcome of which is reported in this article, was triggered by the observation that Euclid’s Algorithm could also be regarded as synchronizing the two cyclic processes “do x:= x - y od” and “do y:= y - x od” in such a way that the relation x > 0 and y > 0 would be kept invariantly true. It was only after this observation that we saw that the formal techniques we had already developed for the derivation of the synchronizing conditions that ensure the harmonious co-operation of (cyclic) sequential processes, such as can be identified in the total activity of operating systems, could be transferred lock, stock and barrel to the development of sequential programs as shown in this article. The main difference is that while for sequential programs the situation “all guards false” is a desirable goal —for it means termination of a repetitive construct—, one tries to avoid it in operating systems —for there it means deadlock.
The second reason to pursue these investigations was my personal desire to get a better appreciation, which part of the programming activity can be regarded as a formal routine and which part of it seems to require “invention”. While the design of an alternative construct now seems to be a reasonably straightforward activity, that of a repetitive construct requires what I regard as “the invention” of an invariant relation and a variant function. My presentation of this calculus should, however, not be interpreted as my suggestion that all programs should be developed in this way: it just gives us another handle.
The calculus does, however, explain my preference for the axiomatic definition of programming language semantics via predicate transformers above other definition techniques: the definition via predicate transformers seems to lend itself most readily to being forged into a tool for the goaldirected activity of program composition.
Finally I would like to add a word or two about the potential nondeterminacy. Having worked mainly with hardly self-checking hardware, with which non-reproducing behaviour of user programs is a very strong indication of a machine malfunctioning, I had to overcome a considerable mental resistance, before I found myself willing to consider non-deterministic programs seriously. It is, however, fair to say that I could never have discovered the calculus before having taken that hurdle: the simplicity and elegance of the above would have been destroyed by requiring the derivation of deterministic programs only. Whether non-determinacy is eventually removed mechanically —in order not too mislead the maintenance engineer— or (perhaps only partly) by the programmer himself because, at second thought, he does care —e.g. for reasons of efficiency— which alternative is chosen, is something I leave entirely to the circumstances. In any case we can appreciate the non-deterministic program as a helpful steppingstone.
Acknowledgements.
In the first place my acknowledgements are due to the members of the IFIP Working Group W.G.2.3 on “Programming Methodology”. Besides them, W.H.J.Feijen, D.E.Knuth, M.Rem and C.S.Scholten have been directly helpful in one way or another. I should also thank the various audiences —in Albuquerque (courtesy NSF), in San Diego and Luxembourg (courtesy Burroughs Corporation)— that have played their role of critical sounding board beyond what one is entitled to hope.
[1] Hoare, C.A.R., An Axiomatic Basis for Computer Programming, Comm.ACM 12
(Oct. 1969) 575 - 583.
[2] Naur, Peter, (Ed.) Report on the Algorithmic Language ALGOL 60,
Comm.ACM 3 (May 1960) 299 - 314
27th January 1975 | prof.dr.Edsger W.Dijkstra |
NUENEN | Burroughs Research Fellow |
Transcribed by Martin P.M. van der Burgt
Last revision