The Guarded Command Language
If your goal is to reason about programs, ordinary languages fight you at every turn:
break, fall-through switch, side-effecting expressions, subtle rules about which
branch runs. Dijkstra's response was radical — design a tiny language whose sole purpose is to be
reasoned about, with a semantics given directly by
weakest
preconditions. That language is the Guarded Command Language, or GCL, and it
is the vehicle for his 1976 book A Discipline of Programming.
GCL is deliberately spartan: assignment, sequencing, and two control structures built from a single new
idea — the guarded command. Its most startling feature is that it is
nondeterministic on purpose. That is not sloppiness; it is a design tool, as we will see.
The guarded command
A guarded command pairs a boolean guard with a statement:
g \;\rightarrow\; S
Read it "when g holds, S is eligible to
run." A guard is just a predicate over the program variables; the statement is only permitted to execute
when its guard is true. On its own a guarded command is inert — it becomes a program only inside one of the
two GCL control structures, which collect several guarded commands together.
Alternation: if … fi
The alternative construct lists guarded commands between if and fi, separated by
the fat bar \;[\!]\; ("or"):
if g1 -> S1
[] g2 -> S2
[] g3 -> S3
fi
To execute it: evaluate all the guards, and from those that are true, pick
one — any one — and run its statement. This is where the nondeterminism lives. If two
guards hold, the language does not say which fires; both are legal executions.
- If no guard holds, the construct aborts — it fails, the strongest
possible bad outcome. So an
if…fi carries an implicit obligation: the guards must be
exhaustive.
- If several guards hold, the choice among them is arbitrary (demonic — you must make the program
correct for every choice).
- Its weakest precondition is
\operatorname{wp}(\texttt{IF}, Q) = \Bigl(\bigvee_i g_i\Bigr) \;\wedge\; \bigwedge_i \bigl(g_i \Rightarrow \operatorname{wp}(S_i, Q)\bigr).
The first conjunct forbids abort (some guard must hold); the second says every enabled branch
must be able to establish Q.
Compare this with a conventional if b then C1 else C2: there, exactly one branch runs and the
guards b, \neg b are automatically exhaustive. GCL makes exhaustiveness a
proof obligation you can see — and lets you write symmetric, overlapping guards when the choice
genuinely does not matter.
// max of x and y, with deliberately overlapping guards
if x >= y -> m := x
[] y >= x -> m := y
fi
// when x = y both guards hold; either assignment is correct, so we don't care which fires
Iteration: do … od
The repetitive construct has the same shape but loops:
do g1 -> S1
[] g2 -> S2
od
Execute it by repeatedly picking an enabled guarded command and running it — over and over — until no
guard holds, at which point the loop terminates normally. Unlike if…fi, an empty guard
set is not an abort here: it is exactly the exit condition.
- The loop keeps going while some guard is true; it stops (successfully) when
\neg(g_1 \vee \cdots \vee g_n).
- A single-guard \texttt{do } b \rightarrow S \texttt{ od} is just the
familiar \texttt{while } b \texttt{ do } S.
- Its weakest precondition is defined as a limit over the number of iterations: informally,
\operatorname{wp}(\texttt{DO}, Q) holds in states from which the loop is
guaranteed to halt (finitely many steps) with Q true. In practice
you never unfold that limit — you reason with an
invariant
plus a variant,
just as in Hoare logic.
Multiple guards shine in symmetric algorithms. Here is the classic subtractive gcd, written with
two guards that mirror each other:
// gcd(a, b) for positive a, b, using repeated subtraction
do a > b -> a := a - b
[] b > a -> b := b - a
od
// terminates when a = b, and then a = gcd of the originals
Neither branch is "the main case." When a > b only the first is enabled; when
b > a only the second; when a = b both guards fail
and the loop exits. The nondeterminism never actually bites here because the guards are disjoint — but the
form expresses the symmetry of Euclid's algorithm perfectly.
Nondeterminism as under-specification
Why would you want a language that refuses to say what happens? Because at design time you often
do not care, and pretending you do forces an arbitrary decision into your code. GCL lets you write
exactly what you mean and no more.
- Under-specification: overlapping guards say "any of these is acceptable." You have
described a set of correct behaviours, not committed to one.
- Refinement: later, an implementation may resolve the nondeterminism any way
it likes — pick the cheaper branch, exploit the hardware — and it is guaranteed correct, because you
proved every resolution correct. A more deterministic program that stays within the allowed
set is called a refinement of the specification.
- Derivation: because the semantics is the wp calculus, you can develop the
program and its proof together —
deriving
correctness by construction rather than verifying after the fact.
This is the deep payoff. In GCL the guards are not just runtime tests — they are the joints at which a
proof clicks together, and the nondeterminism is the freedom you retain until the proof tells you how to
spend it.
A conventional if with no matching case usually just does nothing and slides on — and
that silent fall-through is the source of countless bugs, because the programmer thought the cases
were exhaustive and was wrong. Dijkstra's if…fi makes that assumption explicit and
checkable: "no guard holds" is a loud failure, and the wp rule literally requires
g_1 \vee \cdots \vee g_n as a conjunct of the precondition. You cannot prove the
program correct without proving the guards exhaust the cases you claim to handle. The abort is not a wart;
it is the language refusing to let you skip a case by accident. (Contrast the loop: there, "no guard holds"
is the whole point — it is how you get out.)
A GCL if…fi with two true guards may pick either branch — but this is not a coin
flip, and you must not reason "each is taken with probability ½." The choice is demonic:
an unseen adversary picks the branch, and it may pick the worst one for you, differently every
time, with no probabilities attached. That is exactly why your proof obligation is
\bigwedge_i (g_i \Rightarrow \operatorname{wp}(S_i, Q)) — every enabled
branch must establish Q, because you are not allowed to hope a lucky one runs.
Do not confuse this with a
randomised
algorithm, where choices really are probabilistic and you reason about expectations. GCL's
nondeterminism is about what you left unspecified, not about chance.