Guarded Command Language

From Free net encyclopedia

Guarded Command Language (also Guarded commands) is a language defined by Edsger Dijkstra for predicate transformer semantics. It has a special set of conditional and loop statements. The most basic element of the language is the guarded command, composed of two parts: C, the condition or guard; and S, the statement/command.

A guarded command is usually written:

C <math>\rightarrow</math> S

The conditions are expressed as propositions over the variables of the program. Statements change state:

x, z = y, y + 1 the new value of x is y and the new value of z is y + 1

or perform I/O:

print "Output is the greatest!"

Naturally, an implementation of guarded commands may allow arbitrary breadth of both conditions and statements. A guarded command may occur on its own as a statement; for commands that are always executed, the guard may be omitted:

true <math>\rightarrow</math> print 5

is equivalent to:

print 5

Conditional command if

The if command is written:

if

[command1]

[command2]

...

fi

where [command] is a guarded command.

The statement part is executed if and only if the condition is true. Moreover, if more than one command is applicable — that is, its condition is true — only one will be chosen (randomly or nondeterministically).

Example

Given an expression in pseudocode:

if <math>a \ge b</math> then print "More or equal";

else if <math>a < b</math> then print "Less";

The equivalent in guarded commands is:

if

<math>a \ge b \rightarrow</math> print "More or equal"

<math>a < b \rightarrow</math> print "Less"

fi

The power of guarded commands is illustrated in the following expression:

if

<math>a \ge b\rightarrow</math> print "More or equal"

<math>a \le b \rightarrow</math> print "Less or equal"

fi

When <math>a = b</math>, the result of command can be one "More or equal" or "Less or equal".

Loop command do

The do command is written:

do

[command1]

[command2]

...

od

Every applicable command is executed (possibly more than once) until no commands are applicable.

Example

Below are two implementations of the Euclidean algorithm to find the greatest common divisor.

Variant 1:

x, y = X, Y a statement (unguarded)

do a loop command — this loop will terminate when <math>x = y</math>

<math>x \ne y \rightarrow</math>

if a conditional command (itself guarded)

<math>x > y \rightarrow</math> x := x-y a guarded statement in the if

<math>y > x \rightarrow</math> y := y-x

fi

od

print x ; another statement, also unguarded

Variant 2:

x, y = X, Y

do again, termination when <math>x = y</math>

<math>x > y \rightarrow</math> x := x-y

<math>y > x \rightarrow</math> y := y-x

od

print x

Note that this second version takes advantage of do's termination condition, making the if of the first variant implicit.

Applications

Asynchronous Circuits

Guarded commands are suitable for Quasi Delay Insensitive circuit design because the do-od construct 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:

<math>PulldownGuard \rightarrow y := 0</math>

<math>PullupGuard \rightarrow y := 1</math>

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 do-od model for a set of guarded commands (corresponding to an asynchronous circuit) can accurately describe all possible dynamic behaviors of that circuit.

nl:GCL (programmeertaal)