Guarded Command Language

The Guarded Command Language (GCL) is a programming language defined by Edsger Dijkstra for predicate transformer semantics in EWD472. It combines programming concepts in a compact way. It makes it easier to develop a program and its proof hand-in-hand, with the proof ideas leading the way; moreover, parts of a program can actually be calculated. An important property of GCL is nondeterminism. For example, in the if-statement, several alternatives may be true, and the choice is made at runtime, when the if-statement is executed. This frees the programmer from having to make unnecessary choices and is an aid in the formal development of programs. GCL includes the multiple assignment statement. For example, execution of the statement is done by first evaluating the righthand side values and then storing them in the lefthand variables. Thus, this statement swaps the values of and . The following books discuss the development of programs using GCL: * * * * *

The Guarded Command Language (GCL) is a programming language defined by Edsger Dijkstra for predicate transformer semantics in EWD472. It combines programming concepts in a compact way. It makes it easier to develop a program and its proof hand-in-hand, with the proof ideas leading the way; moreover, parts of a program can actually be calculated. An important property of GCL is nondeterminism. For example, in the if-statement, several alternatives may be true, and the choice is made at runtime, when the if-statement is executed. This frees the programmer from having to make unnecessary choices and is an aid in the formal development of programs. GCL includes the multiple assignment statement. For example, execution of the statement is done by first evaluating the righthand side values and then storing them in the lefthand variables. Thus, this statement swaps the values of and . The following books discuss the development of programs using GCL:

Guarded command

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.

Syntax

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

Semantics

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

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.

Syntax

skip abort

Semantics

skip: do nothing abort: do anything

Assignment

Assigns values to variables.

Syntax

v := E or v , v , ..., v := E , E , ..., E where v are program variables E are expressions of the same data type as their corresponding variables

Catenation

Statements are separated by one semicolon (;)

Selection: if

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.

Syntax

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

Semantics

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.

Implementation

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.

Examples

Simple

In pseudocode: if a a := a - b and b := b - a in such a way that a≥0 and b≥0 remains true.

Extended Euclidean algorithm

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) .

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 prove: it will not stop while the elements are not sorted and that each step it sorts at least 2 elements.

Arg max

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. 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.

Text derived from https://en.wikipedia.org/w/index.php?oldid=1317049628 under CC BY-SA 4.0; modifications have been made.