Guarded Command Language
Encyclopedia
The Guarded Command Language (GCL) is a language defined by Edsger Dijkstra
for predicate transformer semantics
. It combines programming concepts in a compact way, before the program is written in some practical programming language. Its simplicity makes proving the correctness of programs easier, using Hoare logic
.
, 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.
of the form G
S, where
If G is true, the guarded command may be written simply S.
Semantics
At the moment G is encountered in a calculation, it is evaluated.
s.
or
v0, v1, ... , vn := E0, E1, ... , En
where
Selection
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 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.
S0
| G1
S1
...
| Gn
Sn
fi
:
In guarded command language:
if a < b
c := true
| a ≥ b
c := false
fi
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.
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.
S0
| G1
S1
...
| Gn
Sn
od
Original Euclidean algorithm
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.
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) .
of Guarded Commands into a lattice
has led to Refinement Calculus
. This has been mechanized in Formal Methods
like B-Method
that allow to formally derive programs from their specifications.
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 (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.
programming language, which is used by the SPIN model checker
. SPIN verifies correct operation of concurrent software applications.
Edsger Dijkstra
Edsger Wybe Dijkstra ; ) was a Dutch computer scientist. He received the 1972 Turing Award for fundamental contributions to developing programming languages, and was the Schlumberger Centennial Chair of Computer Sciences at The University of Texas at Austin from 1984 until 2000.Shortly before his...
for predicate transformer semantics
Predicate transformer semantics
Predicate transformer semantics was introduced by Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate...
. It combines programming concepts in a compact way, before the program is written in some practical programming language. Its simplicity makes proving the correctness of programs easier, using Hoare logic
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...
.
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 propositionProposition
In logic and philosophy, the term proposition refers to either the "content" or "meaning" of a meaningful declarative sentence or the pattern of symbols, marks, or sounds that make up a meaningful declarative sentence...
, which must be true before the statement is executed
Execution (computers)
Execution in computer and software engineering is the process by which a computer or a virtual machine carries out the instructions of a computer program. The instructions in the program trigger sequences of simple actions on the executing machine...
. 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
Computer program
A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...
meets the specification. The statement is often another guarded command.
Syntax
A guarded command is a statementStatement (programming)
In computer programming a statement can be thought of as the smallest standalone element of an imperative programming language. A program written in such a language is formed by a sequence of one or more statements. A statement will have internal components .Many languages In computer programming...
of the form G
S, where
- G is a propositionPropositionIn logic and philosophy, the term proposition refers to either the "content" or "meaning" of a meaningful declarative sentence or the pattern of symbols, marks, or sounds that make up a meaningful declarative sentence...
, called the guard - S is a statement
If G is true, the guarded command may be written simply S.
SemanticsSemanticsSemantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
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 (in any case, do not execute S)
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 stateState (computer science)
In computer science and automata theory, a state is a unique configuration of information in a program or machine. It is a concept that occasionally extends into some forms of systems programming such as lexers and parsers....
s.
Syntax
v := Eor
v0, v1, ... , vn := E0, E1, ... , En
where
- v are program variables
- E are expressions of the same data typeData typeIn computer programming, a data type is a classification identifying one of various types of data, such as floating-point, integer, or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of...
as their corresponding variables
SelectionConditional statementIn computer science, conditional statements, conditional expressions and conditional constructs are features of a programming language which perform different computations or actions depending on whether a programmer-specified boolean condition evaluates to true or false...
: 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 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
Snfi
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.Simple
In pseudocodePseudocode
In computer science and numerical computation, pseudocode is a compact and informal high-level description of the operating principle of a computer program or other algorithm. It uses the structural conventions of a programming language, but is intended for human reading rather than machine reading...
:
- if a < b then c := True
- else c := False
In guarded command language:
if a < b
c := true| a ≥ b
c := falsefi
Use of Skip
In pseudocode:- if error = True then x := 0
In guarded command language:
if error = true
x := 0| error = false
skipfi
If the second guard is omitted and error = False, the result is abort.
More guards true
if a ≥ b max := a| b ≥ a
max := bfi
If a = b, either a or b is chosen as the new value for the maximum, with equal results. However, someone implementing
Implementation
Implementation is the realization of an application, or execution of a plan, idea, model, design, specification, standard, algorithm, or policy.-Computer Science:...
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.
Repetition: do
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
Snod
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.Original Euclidean algorithmEuclidean algorithmIn mathematics, the Euclidean algorithm is an efficient method for computing the greatest common divisor of two integers, also known as the greatest common factor or highest common factor...
a, b := A, B;do a < b
b := b - a| b < a
a := a - bod
This repetition ends when a = b, in which case a and b hold the greatest common divisor
Greatest common divisor
In mathematics, the greatest common divisor , also known as the greatest common factor , or highest common factor , of two or more non-zero integers, is the largest positive integer that divides the numbers without a remainder.For example, the GCD of 8 and 12 is 4.This notion can be extended to...
of A and B.
Extended Euclidean algorithmExtended Euclidean algorithmThe extended Euclidean algorithm is an extension to the Euclidean algorithm. Besides finding the greatest common divisor of integers a and b, as the Euclidean algorithm does, it also finds integers x and y that satisfy Bézout's identityThe extended Euclidean algorithm is particularly useful when a...
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
Bézout's identity
In number theory, Bézout's identity for two integers a, b is an expressionwhere x and y are integers , such that d is a common divisor of a and b. Bézout's lemma states that such coefficients exist for every pair of nonzero integers...
: xA + yB = gcd(A,B) .
Programs correct by construction
Generalizing the observational congruenceCongruence relation
In abstract algebra, a congruence relation is an equivalence relation on an algebraic structure that is compatible with the structure...
of Guarded Commands into a lattice
Lattice (order)
In mathematics, a lattice is a partially ordered set in which any two elements have a unique supremum and an infimum . Lattices can also be characterized as algebraic structures satisfying certain axiomatic identities...
has led to Refinement Calculus
Refinement Calculus
Refinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable "program", which is then refined by a series of correctness-preserving transformations into an...
. This has been mechanized in Formal Methods
Formal methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
like B-Method
B-Method
The B method is method of software development based on B, a tool-supported formal method based around an abstract machine notation, used in the development of computer software. It was originally developed by Jean-Raymond Abrial in France and the UK. B is related to the Z notation and supports...
that allow to formally derive programs from their specifications.
Asynchronous Circuits
Guarded commands are suitable for Quasi Delay InsensitiveQuasi Delay Insensitive
In digital logic design, Quasi Delay-Insensitive circuits are a class of almost delay-insensitive asynchronous circuits which are invariant to the delays of any of the circuit's wires or elements, except to assume that certain fanouts are isochronic...
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 := 0PullUpGuard
y := 1PullDownGuard 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.
Model Checking
Guarded commands are used within the PromelaPromela
PROMELA is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, communication via message channels can be defined to be synchronous , or asynchronous...
programming language, which is used by the SPIN model checker
SPIN model checker
SPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980...
. SPIN verifies correct operation of concurrent software applications.