Guarded Command Language

A guarded command is a statement of the form G → S, where

• G is a proposition, called the guard
• S is a statement

At the moment G is encountered in a calculation, it is evaluated.

• If G is true, execute S
• If G is false, look at the context to decide what to do (in any case, do not execute S)

skip

abort

• skip: do nothing
• abort: do anything

v := E

or

v0, v1, ..., vn := E0, E1, ..., En

where

• v are program variables
• E are expressions of the same data type as their corresponding variables

if G0 → S0
 □ G1 → S1
...
 □ Gn → Sn
fi

Upon execution of a selection all guards are evaluated. If none of the guards evaluates to true then execution of the selection aborts, otherwise one of the guards that has the value true is chosen non-deterministically and the corresponding statement is executed.

In pseudocode:

if a < b then set c to True
else set c to False

In guarded command language:

if a < b → c := true
 □ a ≥ b → c := false
fi

In pseudocode:

if error is True then set x to 0

In guarded command language:

if error → x := 0
 □ ${\displaystyle \neg }$error → skip
fi

If the second guard is omitted and error is False, the result is abort.

if a ≥ b → max := a
 □ b ≥ a → max := b
fi

If a = b, either a or b is chosen as the new value for the maximum, with equal results. However, the implementation may find that one is easier or faster than the other. Since there is no difference to the programmer, any implementation will do.

do G0 → S0
 □ G1 → S1
...
 □ Gn → Sn
od

Execution of the repetition consists of executing 0 or more iterations, where an iteration consists of (nondeterministically) choosing a guarded command Gi → Si whose guard Gi evaluates to true and executing the command Si. Thus, if all guards are initially false, the repetition terminates immediately, without executing an iteration. Execution of the repetition do od, which has no guarded commands, executes 0 iterations, so do od is equivalent to skip.

a, b := A, B;
do a < b → b := b - a
 □ b < a → a := a - b
od

This repetition ends when a = b, in which case a and b hold the greatest common divisor of A and B.

Dijkstra sees in this algorithm a way of synchronizing two infinite cycles a := a - b and b := b - a in such a way that a≥0 and b≥0 remains true.

a, b, x, y, u, v := A, B, 1, 0, 0, 1;
do b ≠ 0 →
   q, r := a div b, a mod b;
   a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v
od

This repetition ends when b = 0, in which case the variables hold the solution to Bézout's identity: xA + yB = gcd(A,B) .

do a>b → a, b := b, a
 □ b>c → b, c := c, b
 □ c>d → c, d := d, c
od

The program keeps on permuting elements while one of them is greater than its successor. This non-deterministic bubble sort is not more efficient than its deterministic version, but easier to prove: it will not stop while the elements are not sorted and that each step it sorts at least 2 elements.

x, y = 1, 1;
do x≠n →
   if f(x) ≤ f(y) → x := x+1
    □ f(x) ≥ f(y) → y := x; x := x+1
   fi
od

This algorithm finds the value 1 ≤ y ≤ n for which a given integer function f is maximal. Not only the computation but also the final state is not necessarily uniquely determined.

Generalizing the observational congruence of Guarded Commands into a lattice has led to Refinement Calculus.[2] This has been mechanized in Formal Methods like B-Method that allow one to formally derive programs from their specifications.

Guarded commands are suitable for quasi-delay-insensitive circuit design because the repetition allows arbitrary relative delays for the selection of different commands. In this application, a logic gate driving a node y in the circuit consists of two guarded commands, as follows:

PullDownGuard → y := 0
PullUpGuard → y := 1

PullDownGuard and PullUpGuard here are functions of the logic gate's inputs, which describe when the gate pulls the output down or up, respectively. Unlike classical circuit evaluation models, the repetition for a set of guarded commands (corresponding to an asynchronous circuit) can accurately describe all possible dynamic behaviors of that circuit. Depending on the model one is willing to live with for the electrical circuit elements, additional restrictions on the guarded commands may be necessary for a guarded-command description to be entirely satisfactory. Common restrictions include stability, non-interference, and absence of self-invalidating commands.[3]

Guarded commands are used within the Promela programming language, which is used by the SPIN model checker. SPIN verifies correct operation of concurrent software applications.

The Perl module Commands::Guarded implements a deterministic, rectifying variant on Dijkstra's guarded commands.