Guarded Command Language#Selection: if

A guarded command consists of a boolean condition or guard, and a statement "guarded" by it. The statement is only executed if the guard is true, so when reasoning about the statement, the condition can be assumed true. This makes it easier to prove the program meets a specification.

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

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

• If G evaluates to true, S is eligible to be executed. In most GCL constructs, multiple guarded commands may have guards that are true, and exactly one of them is chosen arbitrarily to be executed.
• If G is false, S will not be executed.

skip and abort are important statements in the guarded command language. abort is the undefined instruction: do anything. It 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 often used when the syntax requires a statement but the state should not change.

skip

abort

• skip: do nothing
• abort: do anything

Assigns values to variables.

v := E

or

v{{sub|0}}, v{{sub|1}}, ..., v{{sub|n}} := E{{sub|0}}, E{{sub|1}}, ..., E{{sub|n}}

where

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

Statements are separated by one semicolon (;)

The selection (often called the "conditional statement" or "if statement") is a list of guarded commands, of which one is chosen to execute. If more than one guard is true, one statement whose guard is true is arbitrarily chosen to be executed. If no guard is true, the result is undefined, that is, equivalent to abort. Because at least one of the guards must be true, the empty statement skip is often needed. The statement if fi has no guarded commands, so there is never a true guard. Hence, if fi is equivalent to abort.

if G0 → S0

□ G1 → S1

...

□ Gn → Sn

fi

Upon execution of a selection, the guards are evaluated. If none of the guards is true, then the selection aborts, otherwise one of the clauses with a true guard is chosen arbitrarily and its statement is executed.

GCL does not specify an implementation. Since guards cannot have side effects and the choice of clause is arbitrary, an implementation may evaluate the guards in any sequence and choose the first true clause, for example.

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

□ {{not}}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.

Execution of this repetition, or loop, is shown below.

do G0 → S0

□ G1 → S1

...

□ Gn → Sn

od

Execution of the repetition consists of executing 0 or more iterations, where an iteration consists of arbitrarily choosing a guarded command {{math|Gi → Si}} whose guard {{math|Gi}} is true and executing the command {{math|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

□ c

AI

x, y = 1, 1;

Generalizing the observational congruence of Guarded Commands into a lattice has led to Refinement Calculus.{{cite web | title=On the Correctness of Refinement Steps in Program Development (Phd-Thesis) | last=Back | first=Ralph J | authorlink=Ralph-Johan_Back | url=http://crest.abo.fi/publications/public/1978/OnTheCorrectnessOfRefinementStepsInProgramDevelpmentTR.pdf | year=1978 | url-status=dead | archiveurl=https://web.archive.org/web/20110720175255/http://crest.abo.fi/publications/public/1978/OnTheCorrectnessOfRefinementStepsInProgramDevelpmentTR.pdf | archivedate=2011-07-20 }} 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

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 [https://metacpan.org/module/Commands::Guarded Commands::Guarded] implements a deterministic, rectifying variant on Dijkstra's guarded commands.