The guarded command is the most important element of the guarded command language. In a guarded command, just as the name says, the command is "guarded". The guard is a proposition, which must be true before the statement is executed. At the start of that statement's execution, one may assume the guard to be true. Also, if the guard is false, the statement will not be executed. The use of guarded commands makes it easier to prove the program meets the specification. The statement is often another guarded command.
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
Skip and Abort
Skip and Abort are very simple as well as important statements in the guarded command language. Abort is the undefined instruction: do anything. The abort statement does not even need to terminate. It is used to describe the program when formulating a proof, in which case the proof usually fails. Skip is the empty instruction: do nothing. It is used in the program itself, when the syntax requires a statement, but the programmer does not want the machine to change states.
Selection">Conditional (programming)">Selection: if
The selection is a list of guarded commands, of which one is chosen to execute. If more than one guard is true, one statement is nondeterministically chosen to be executed. If none of the guards are true, the result is undefined. Because at least one of the guards must be true, the empty statement "skip" is often needed.
Syntax
if G0 → S0 | G1 → S1 ... | Gn → Sn fi
Semantics
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.
Examples
Simple
In pseudocode: In guarded command language: if a < b → c := true | a ≥ b → c := false fi
Use of skip
In pseudocode: In guarded command language: if error = true → x := 0 | error = false → skip fi If the second guard is omitted and error = False, the result is abort.
More guards true
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, someone implementing this, may find that one is easier or faster than the other. Since there is no difference to the programmer, he is free to implement either way.
The repetition executes the guarded commands repeatedly until none of the guards are true. Usually, there is only one guard.
Syntax
do G0 → S0 | G1 → S1 ... | Gn → Sn od
Semantics
Upon execution of a repetition all guards are evaluated. If all guards evaluate to false then skip is executed. Otherwise, one of the guards that has value true is chosen non-deterministically and the corresponding statement is executed after which the repetition is executed again.
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.
Non-deterministic sort
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 proof: 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 ≤ f → x := x+1 | | f ≥ f → y := x; x := x+1 | fi od This algorithm finds the value 1 ≤ y ≤ n for which a given integer functionf is maximal. Not only the computation but also the final state is not necessarily uniquely determined.
Applications
Programs correct by construction
Generalizing the observational congruence of Guarded Commands into a lattice has led to Refinement Calculus. This has been mechanized in Formal Methods like B-Method that allow one to formally derive programs from their specifications.
Asynchronous circuits
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 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.
