Editing Guarded Command Language (section)

== Applications ==
=== Programs correct by construction ===

Generalizing the observational [[Congruence relation|congruence]] of Guarded Commands into a [[Lattice (order)|lattice]] has led to [[Refinement Calculus]].<ref>{{cite web | title=On the Correctness of Refinement Steps in Program Development (Phd-Thesis) | last=Back | first=Ralph J | authorlink=Ralph-Johan_Back | url=http://crest.abo.fi/publications/public/1978/OnTheCorrectnessOfRefinementStepsInProgramDevelpmentTR.pdf | year=1978 | url-status=dead | archiveurl=https://web.archive.org/web/20110720175255/http://crest.abo.fi/publications/public/1978/OnTheCorrectnessOfRefinementStepsInProgramDevelpmentTR.pdf | archivedate=2011-07-20 }}</ref> This has been mechanized in [[Formal Methods]] like [[B-Method]] that allow one to formally derive programs from their specifications.

=== 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 → 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.<ref name="synthesis_tr">{{cite web | title=Synthesis of Asynchronous VLSI Circuits|last=Martin | first=WILLIAM | url=http://resolver.caltech.edu/CaltechCSTR:1991.cs-tr-93-28 }}</ref> AI

=== 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.

=== Other ===
The Perl module [https://metacpan.org/module/Commands::Guarded Commands::Guarded] implements a deterministic, rectifying variant on Dijkstra's guarded commands.