- Guarded Command Language
The Guarded Command Language (GCL) is a language defined by
Edsger Dijkstrafor predicate transformer semanticscite web | last=Dijkstra | first=Edsger W | authorlink=E. W. Dijkstra | url=http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD472.PDF | title=EWD472: Guarded commands, non-determinacy and formal. derivation of programs. | accessdate=August 16 | accessyear=2006] . The language is strictly theoretical, no compilers exist. 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.
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. Syntax
A guarded command is a statement of the form G S, where
* G is a
proposition, called the guard
* S is a statement
If G ≡ true, the guarded command may be written simply S.
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)
kip 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.
* Skip: do nothing
* Abort: do anything
Assigns values to
v := Eor v0, v1, ... , vn := E0, E1, ... , En
* v are program variables
* E are expressions of the same
data typeas their corresponding variables Concatenation
Assignments are separated by one semicolon (;)
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.
if G0 S0  G1 S1 ...  Gn Sn fi
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. cite | author=Anne Kaldewaij | title=Programming: The Derivation of Algorithms | publisher=Prentice Hall | date=1990]
pseudocode::if a < b then c := True:else c := False
In guarded command language: if a < b c := true  a ≥ b c := false fi
Use of Skip
In pseudocode::if error = True then x := 0
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.
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, 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.
The repetition executes the guarded commands repeatedly until none of the guards are true. Usually there is only one guard.
do G0 S0  G1 S1 ...  Gn Sn od
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.
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 divisorof 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) .
Guarded commands are suitable for
Quasi Delay Insensitivecircuit design because the repetitionallows 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 classicalcircuit 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 descriptionto be entirely satisfactory. Common restrictions include stability, non-interference, and absenceof self-invalidating commands.cite web | title=Synthesis of Asynchronous VLSI Circuits|last=Martin | first=Alain J | url=http://resolver.caltech.edu/CaltechCSTR:1991.cs-tr-93-28 ]
Guarded commands are used within the
Promelaprogramming language, which is used by the SPIN model checker. SPIN verifies correct operation of concurrent software applications.
The Perl module [http://search.cpan.org/perldoc/Commands::Guarded Commands::Guarded] implements a deterministic, rectifying variant on Dijkstra's guarded commands.
Wikimedia Foundation. 2010.
Look at other dictionaries:
language — /lang gwij/, n. 1. a body of words and the systems for their use common to a people who are of the same community or nation, the same geographical area, or the same cultural tradition: the two languages of Belgium; a Bantu language; the French… … Universalium
RAF Coastal Command — Royal Air Force Coastal Command … Wikipedia
Edsger W. Dijkstra — Edsger Wybe Dijkstra Born May 11, 1930(1930 05 11) Rotterdam, Netherl … Wikipedia
Quantum programming — is a set of computer programming languages that allow the expression of quantum algorithms using high level constructs. The point of quantum languages is not so much to provide a tool for programmers, but to provide tools for researchers to… … Wikipedia
Structured programming — can be seen as a subset or subdiscipline of procedural programming, one of the major programming paradigms. It is most famous for removing or reducing reliance on the GOTO statement.Historically, several different structuring techniques or… … Wikipedia
Lenguaje de Comandos Guardados — El Lenguaje de Comandos Guardados (GCL, Guarded Command Language), o de Órdenes Guardadas, es un modelo de lenguaje definido por Edsger Dijkstra para semántica de transformación de predicados (una extensión lógica diseñada para proporcionar una… … Wikipedia Español
GCL — can mean:* Galaxy Communications Ltd * Ganglion cell layer, a layer of the Retina * GNU Common Lisp * Golden Concorde Ltd., a renewable energy company in China. * Government Category List * Grand Companion of the Order of Logohu * Granule cell… … Wikipedia
GaCeLa — (Del ár. gazala.) ► sustantivo femenino ZOOLOGÍA Pequeño mamífero rumiante del grupo de los antílopes, muy estilizado y de cuello largo, pelo corto de color canela, orejas largas, muy veloz, que habita en las estepas africanas y asiáticas.… … Enciclopedia Universal
Actor model and process calculi — In computer science, the Actor model and process calculi are two closely related approaches to the modelling of concurrent digital computation. See Actor model and process calculi history.There are many similarities between the two approaches,… … Wikipedia
Actor model and process calculi history — The Actor model and process calculi share an interesting history and co evolution.Early workThe Actor model, first published in 1973, [Carl Hewitt, Peter Bishop and Richard Steiger. A Universal Modular Actor Formalism for Artificial Intelligence… … Wikipedia