The Guarded Command Language (GCL) is a
programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming ...
defined by
Edsger Dijkstra
Edsger Wybe Dijkstra ( ; ; 11 May 1930 – 6 August 2002) was a Dutch computer scientist, programmer, software engineer, systems scientist, and science essayist. He received the 1972 Turing Award for fundamental contributions to developing progra ...
for
predicate transformer semantics
Predicate transformer semantics were introduced by Edsger 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 ''st ...
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
Nondeterminism or nondeterministic may refer to:
Computer science
*Nondeterministic programming
*Nondeterministic algorithm
*Nondeterministic model of computation
**Nondeterministic finite automaton
**Nondeterministic Turing machine
*Indeterminacy ...
. For example, in the if-statement, several alternatives may be true, and the choice of which to choose is done 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
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
In logic and linguistics, a proposition is the meaning of a declarative sentence. In philosophy, " meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same meaning. Equivalently, a proposition is the no ...
, which must be true before the statement is
executed
Capital punishment, also known as the death penalty, is the state-sanctioned practice of deliberately killing a person as a punishment for an actual or supposed crime, usually following an authorized, rule-governed process to conclude that t ...
. 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
Program, programme, programmer, or programming may refer to:
Business and management
* Program management, the process of managing several related projects
* Time management
* Program, a part of planning
Arts and entertainment Audio
* Progra ...
meets the
specification
A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard.
There are different types of technical or engineering specificati ...
. The statement is often another guarded command.
Syntax
A guarded command is a
statement of the form G → S, where
* G is a
proposition
In logic and linguistics, a proposition is the meaning of a declarative sentence. In philosophy, " meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same meaning. Equivalently, a proposition is the no ...
, called the guard
* S is a statement
Semantics
Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comp ...
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 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 used in the program itself, when the syntax requires a statement but the
state
State may refer to:
Arts, entertainment, and media Literature
* ''State Magazine'', a monthly magazine published by the U.S. Department of State
* ''The State'' (newspaper), a daily newspaper in Columbia, South Carolina, United States
* ''Our S ...
should not change.
Syntax
skip
abort
Semantics
* skip: do nothing
* abort: do anything
Assignment
Assignment, assign or The Assignment may refer to:
* Homework
* Sex assignment
* The process of sending National Basketball Association players to its development league; see
Computing
* Assignment (computer science), a type of modification to ...
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
Selection may refer to:
Science
* Selection (biology), also called natural selection, selection in evolution
** Sex selection, in genetics
** Mate selection, in mating
** Sexual selection in humans, in human sexuality
** Human mating strateg ...
: 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 nondeterministically chosen to be executed. If no guard is true, the result is undefined. 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 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.
Examples
Simple
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
Use of skip
In pseudocode:
if error is True then set x to 0
In guarded command language:
if error → x := 0
□ error → skip
fi
If the second guard is omitted and error is False, the result is abort.
More guards true
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
Implementation is the realization of an application, or execution of a plan, idea, model, design, specification, standard, algorithm, or policy.
Industry-specific definitions
Computer science
In computer science, an implementation is a real ...
may find that one is easier or faster than the other. Since there is no difference to the programmer, any implementation will do.
Repetition
Repetition may refer to:
* Repetition (rhetorical device), repeating a word within a short space of words
*Repetition (bodybuilding), a single cycle of lifting and lowering a weight in strength training
*Working title for the 1985 slasher film '' ...
: ''do''
Execution of this repetition, or loop, is shown below.
Syntax
do G0 → S0
□ G1 → S1
...
□ Gn → Sn
od
Semantics
Execution of the repetition consists of executing 0 or more ''iterations'', where an iteration consists of (nondeterministically) choosing a guarded command whose guard evaluates to true and executing the command . 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.
Examples
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
In mathematics, the greatest common divisor (GCD) of two or more integers, which are not all zero, is the largest positive integer that divides each of the integers. For two integers ''x'', ''y'', the greatest common divisor of ''x'' and ''y'' is ...
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.
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
In mathematics, Bézout's identity (also called Bézout's lemma), named after Étienne Bézout, is the following theorem:
Here the greatest common divisor of and is taken to be . The integers and are called Bézout coefficients for ; they ...
: 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 proof: it will not stop while the elements are not sorted and that each step it sorts at least 2 elements.
Arg max
In mathematics, the arguments of the maxima (abbreviated arg max or argmax) are the points, or elements, of the domain of some function at which the function values are maximized.For clarity, we refer to the input (''x'') as ''points'' and t ...
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.
Applications
Programs correct by construction
Generalizing the observational
congruence of Guarded Commands into a
lattice
Lattice may refer to:
Arts and design
* Latticework, an ornamental criss-crossed framework, an arrangement of crossing laths or other thin strips of material
* Lattice (music), an organized grid model of pitch ratios
* Lattice (pastry), an orna ...
has led to
Refinement Calculus.
This has been mechanized in
Formal Methods
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...
like
B-Method The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.
Overview
B was originally developed in the 1980s by Jean-Raymond Abr ...
that allow one to formally derive programs from their specifications.
Asynchronous circuits
Guarded commands are suitable for
quasi-delay-insensitive circuit
In digital logic design, an asynchronous circuit is quasi delay-insensitive (QDI) when it operates correctly, independent of gate and wire delay with the weakest exception necessary to be turing-complete.
Overview
Pros
* Robust to process varia ...
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.
Model checking
Guarded commands are used within the
Promela
PROMELA (Process or Protocol Meta Language) is a verification modeling language introduced by Gerard J. Holzmann. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems. In PROMELA models, c ...
programming language, which is used by the
SPIN model checker
SPIN is a general tool for verifying the correctness of concurrent 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 ...
. SPIN verifies correct operation of concurrent software applications.
Other
The Perl modul
Commands::Guardedimplements a deterministic, rectifying variant on Dijkstra's guarded commands.
References
{{Edsger Dijkstra
Logic programming
Edsger W. Dijkstra