← CatZep/Engineering Guides/The Science of Programming

The Alternative Command — Guarded Selection (IF)

Dijkstra’s guarded if…fi as Gries develops it: a nondeterministic choice among guarded commands whose weakest precondition makes case-coverage a proof obligation, not a courtesy.

Every conditional you have ever written picks a branch. Dijkstra’s alternative command — the guarded if…fi — does the same, but with two deliberate design choices that a conventional if/else hides from you. First, when several conditions are true it chooses any of them (nondeterminism). Second, when none is true it does not silently fall through — it aborts. Both choices exist to serve the same master the rest of Gries’ book serves: a clean weakest-precondition semantics that turns “did I handle every case?” into a formula you can actually check. This page covers the syntax, the wp rule, why coverage is a proof obligation, how to derive an IF from a specification, and the pitfalls.

Concepts explained in this guide

Read these definitions first, or use the linked terms as you go. The examples and limitations are local to this guide; companion pages are optional.

Dijkstra’s guarded commands

The alternative command is a list of guarded commands separated by the fat bar [] and bracketed by if and fi. Each guarded command is a pair Bi → Si: a boolean guard Bi and the statement Si that runs when it is chosen.

if B1 → S1
[] B2 → S2
[] …
[] Bn → Sn
fi

The operational semantics has three steps:

• Evaluate all guards. Compute B1, …, Bn in the current state.
• Choose one true guard. If at least one guard is true, pick one of the true guards and execute its statement. When more than one guard is true the choice is made nondeterministically — the language does not promise which arm runs, and a correct program must not care.
• Abort if none holds. If no guard is true, the command aborts (equivalent to abort, whose wp is F). It does not quietly do nothing.

Why nondeterminism is a feature, not a bug

Beginners read “the machine may pick either branch” as a liability. It is the opposite. Nondeterminism lets you avoid over-specifying: when two cases genuinely lead to an equally correct result, forcing an arbitrary tie-break (as a sequential if/else does — the first clause always wins) bakes an accident of ordering into the program’s meaning. A guarded IF with overlapping guards says exactly what is true: “in the overlap, either arm is acceptable.”

• It exposes symmetry. The max-of-two below uses x ≥ y and y ≥ x — visibly symmetric. A >/else version breaks the symmetry for no reason and hides that either choice works at x = y.
• It keeps proofs honest. Because the implementation may choose any true guard, your correctness argument must hold for every true guard. You cannot lean on an execution order the semantics never promised.
• It leaves room for the implementer. A compiler or scheduler is free to pick whichever true arm is cheapest, since all true arms are declared correct.

Weakest precondition of IF

Write IF for the whole alternative command. Its weakest precondition for a postcondition R is:

The rule splits cleanly into two parts, and each carries a distinct obligation:

• First conjunct — coverage. (B1 ∨ … ∨ Bn) demands that at least one guard is true in the starting state. If it can be false, execution might reach a state where the command aborts, so wp (which encodes total correctness) cannot hold. This single term is what turns “handle every case” into mathematics.
• Remaining conjuncts — correctness of each branch. Each (Bi ⇒ wp(Si, R)) says: whenever guard Bi could be the one selected, its statement Si must be guaranteed to establish R. Because selection among true guards is nondeterministic, every true guard’s branch must independently work — hence a separate conjunct for each.

Contrast with an ordinary if-then-else

In most languages, if B then S with no else is sugar for if B then S else skip. When B is false, the construct silently does nothing — a skip, whose wp is just R. That is permissive: a forgotten case slides by as a no-op and the bug surfaces far downstream. The guarded IF makes the opposite choice: a missing case is an abort, whose wp is F, which immediately poisons the whole wp. Stricter, yes — and safer, because the proof fails at the point of the omission instead of hiding it.

# if B then S   ==   if B then S else skip
# wp = (B => wp(S,R)) ∧ (¬B => R)
# when B is false: nothing happens, R
# must already hold. A forgotten case
# passes through unnoticed.

if B → S fi
# wp = B ∧ (B => wp(S,R))
#    = B ∧ wp(S,R)
# if B can be false, coverage fails
# and wp collapses to F. The proof
# forces you to state every case.

Coverage is a proof obligation

The first conjunct is not decoration — it is the term most designs get wrong. Consider the maximum of two values. The natural first draft uses strict inequalities, and it has a hole exactly at equality.

# goal R:  m = max(x, y)
if x > y → m := x
[] x < y → m := y
fi
# coverage: (x>y) ∨ (x<y)  ==  x ≠ y
# at x = y neither guard holds → ABORT
# first conjunct is NOT T, so wp fails

# goal R:  m = max(x, y)
if x ≥ y → m := x
[] y ≥ x → m := y
fi
# coverage: (x≥y) ∨ (y≥x)  ==  T   ✓
# at x = y BOTH guards hold — overlap.
# either arm sets m to the common value,
# so both establish R. Nondeterminism
# is harmless here — by design.

Two lessons sit inside this small example:

• Overlapping guards are allowed and often desirable. The wp rule never asks the guards to be mutually exclusive — only to cover. Where two guards overlap, the extra conjuncts simply require both arms to establish R, which the equality case here satisfies trivially.
• Coverage and correctness are checked separately. (x ≥ y) ∨ (y ≥ x) reduces to T, discharging coverage; then x ≥ y ⇒ wp(m:=x, R) and y ≥ x ⇒ wp(m:=y, R) discharge the arms. The proof splits exactly the way the design should.

Deriving an IF from a specification

The wp rule is not just a checker — run it backward and it becomes a constructor. To build an IF that establishes postcondition R from precondition Q:

1. Choose guards that cover Q. Pick B1, …, Bn so that Q ⇒ (B1 ∨ … ∨ Bn). This guarantees the coverage conjunct under any state allowed by the precondition — no abort is reachable.
2. Design each branch to establish R under its guard. For every i, build Si so that the triple {Q ∧ Bi} Si {R} holds — equivalently Q ∧ Bi ⇒ wp(Si, R). The guard hands each branch an extra assumption Bi, which is usually exactly what makes the branch easy to write.

Notice how the labor divides: coverage is a property of the guard set as a whole, correctness is a property of each arm in isolation. You never reason about interactions between branches.

Worked example 1 — maximum of two

Establish R: m = max(x, y) from Q: T (works for all states).

# Step 1 — guards must cover Q = T.
#   pick x ≥ y and y ≥ x; their
#   disjunction is T, so coverage holds.
# Step 2 — design each arm:
#   {x ≥ y} m := x {m = max(x,y)}   ✓
#   {y ≥ x} m := y {m = max(x,y)}   ✓
if x ≥ y → m := x
[] y ≥ x → m := y
fi
# {m = max(x, y)}

Worked example 2 — the “if a < b swap” style

A classic use of a single-armed IF paired with a skip arm: order two variables so that afterward a ≥ b. Here you must supply the second guard explicitly — the guarded IF gives you no implicit else, so the “do nothing” case is written out as a guard whose statement is skip.

# R:  a ≥ b   (values of {a,b} unchanged as a set)
# coverage:  (a < b) ∨ (a ≥ b)  ==  T   ✓
if a < b → a, b := b, a   # swap into order
[] a ≥ b → skip          # already ordered
fi
# {a ≥ b}
# NOTE: omitting the a ≥ b arm would abort
# whenever a is already ≥ b — the opposite
# of a conventional guardless "if a < b then swap".

This is the deterministic special case: the two guards a < b and a ≥ b are exactly B and ¬B, so they partition the state space, there is no overlap, and the IF behaves like an ordinary if-then-else — except that the “else” is stated, not assumed.

Worked example 3 — sign of a number (n > 2 guards)

Guarded IF is not limited to two arms. To classify the sign of a into s ∈ {-1, 0, +1}, three guards partition the domain. This shows the rule generalizing to any n.

# R:  (a < 0 ∧ s = -1)
#  ∨ (a = 0 ∧ s =  0)
#  ∨ (a > 0 ∧ s = +1)
# coverage: (a<0) ∨ (a=0) ∨ (a>0) == T  ✓
if a < 0 → s := -1
[] a = 0 → s :=  0
[] a > 0 → s := +1
fi
# {s = sign(a)}

The three guards are mutually exclusive and exhaustive, so the disjunction is T (coverage ✓) and each arm trivially establishes its slice of R. If you had written only a < 0 and a > 0, coverage would reduce to a ≠ 0 and the command would abort at a = 0 — the proof would refuse to close, pointing straight at the omission.

Common patterns & pitfalls

The side-effect rule deserves emphasis: the entire wp derivation treats Bi as a predicate over the starting state that can be evaluated freely and in any order. If evaluating a guard could change the state, “evaluate all guards, then choose” is no longer well defined, and none of the conjuncts in the wp rule mean what they say. Keep guards pure.

Total correctness note

wp encodes total correctness — guaranteed termination in a state satisfying R — so it is worth asking whether the alternative command can fail to terminate. It cannot, on its own account. Given that some guard holds (coverage), the IF evaluates the finite list of guards, selects one true arm, and runs its statement exactly once. It introduces no repetition. So the IF itself always terminates, provided the chosen branch Si terminates.

A selection adds no repetition itself, but an enabled branch can abort, raise an unmodeled error, or fail to terminate. Total correctness requires finite defined guards, coverage, and total correctness of every enabled branch.

Worked example: maximum of equal values

Work through the state changes and the exact claim being checked.

Run and change the example

Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:

python3 guide_labs.py guards
python3 guide_labs.py test

The complete standard-library lab checks the stated finite cases and boundary inputs. Its invariants explain the reasoning; tests alone do not prove all possible inputs.

The program tests its stated finite contracts. It is an educational model, not an implementation of the named production product or a proof of unmodeled distributed faults.

Summary