Guarded Command Language

From Wikipedia, the free encyclopedia

The Guarded Command Language (GCL) is a language defined by Edsger Dijkstra for predicate transformer semantics [1].

Contents

[edit] Guarded command

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.

[edit] Syntax

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

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

If G \equiv \mbox{True}, the guarded command may be written simply S.

[edit] Semantics

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

[edit] 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.

[edit] Syntax

  • Skip
  • Abort

[edit] Semantics

  • Skip: do nothing
  • Abort: do anything

[edit] Assignment

Assigns values to variables.

[edit] Syntax

  • v: = E
  • v0,v1,...,vn: = E0,E1,...,En

where

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

[edit] Concatenation

Assignments are separated by one semicolon (;)

[edit] 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 guards are true, one statement is chosen to be executed (randomly or nondeterministically). 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.

[edit] Syntax

if
G_{0} \rightarrow S_{0}
[]\ G_{1} \rightarrow S_{1}
...
[]\ G_{n} \rightarrow S_{n}
fi

[edit] Semantics

  • If none of the guards are true: abort
  • If only guard Gx is true: execute Sx
  • If guards G_{x_{0}}\ ...\ G_{x_{m}} are true: execute any S_{x_{y}}, where 0 \leq y \leq m

[edit] Examples

[edit] Simple

In pseudocode:

if a < b then c := True
else c := False

In guarded command language:

if
a < b \rightarrow c := True
[]\ a \geq b \rightarrow c := False
fi

[edit] Use of Skip

In pseudocode:

if error = True then x := 0

In guarded command language:

if
error = \mbox{True} \rightarrow x := 0
[]\ error = \mbox{False} \rightarrow \mbox{skip}
fi

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

[edit] More guards true

if
a \geq b \rightarrow max := a
[]\ a \leq b \rightarrow 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.

[edit] Repetition: do

The repetition executes the guarded commands repeatedly until none of the guards are true. Usually there is only one guard.

[edit] Syntax

do
G_{0} \rightarrow S_{0}
[]\ G_{1} \rightarrow S_{1}
...
[]\ G_{n} \rightarrow S_{n}
od

[edit] Semantics

  • If none of the guards are true: skip
  • If only guard Gx is true: execute Sx and test the guards again
  • If guards G_{x_{0}}\ ...\ G_{x_{m}} are true: execute any S_{x_{y}}, where 0 \leq y \leq m and test the guards again

[edit] Examples

[edit] Original Euclidean algorithm

a,b: = A,B;
do
a > b \rightarrow a := a - b
[]\ b > a \rightarrow b := b - a
od

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

[edit] Extended Euclidean algorithm

a,b,x,y,u,v: = A,B,1,0,0,1;
do
b \neq 0 \rightarrow
q, r := a\ \mbox{div}\ b, a\ \mbox{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).

[edit] Applications

[edit] 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 \rightarrow y := 0
PullupGuard \rightarrow 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.[2]

[edit] Model Checking

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.

[edit] Other

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

[edit] References

  1. ^ Dijkstra, Edsger W. EWD472: Guarded commands, non-determinacy and formal. derivation of programs.. Retrieved on August 16, 2006.
  2. ^ Martin, Alain J. Synthesis of Asynchronous VLSI Circuits.
Retrieved from "http://en.wikipedia.org../../../g/u/a/Guarded_Command_Language_382d.html"
In other languages