Guarded Command Language（GCL）とは、エドガー・ダイクストラが述語変換意味論向けに定義した言語であるガード付きコマンドはGCLの最重要要素である。ガード付きコマンドは名前の通り、ガードが付いている。ガードは一種の命題であり、その文を実行する前に真でなければならない。文の実行前に、そのガードは真であると仮定される。また、ガードが偽であった場合、その文は実行されない。ガード付きコマンドを使うことで、プログラムがその仕様に適合していることを証明することが容易になる。ガード付きコマンドの本体（実行すべき文）がガード付きコマンドになっていることが多い。ガード付きコマンドは、 formula_1 という形式の文であり、ここでformula_4 なら、ガード付きコマンドは単に formula_3 と記述される。計算の流れで formula_2 が出てくると、それを評価する。Skip と Abort は非常に単純だがガード付きコマンドと同様に重要な要素である。Abort は未定義命令であり、何もしない。Abort は完了することさえ保証されていない。プログラムが何らかの証明の定式化であるとすれば、Abort は証明の失敗に対応する。Skip は空の命令であり、何もしない。文法上、文が必要とされるが、プログラマが状態を変更したくない場合、プログラム内で使われる。代入文は変数に値を代入する。ここで代入文はセミコロン(;)を間に書いて、並べて記述される。選択（一般に、条件文とかif文と呼ばれる）はガード付きコマンドのリストであり、そのうちの1つの文が選択実行される。複数のガードが真である場合、実行する文はランダムまたは非決定的に選択される。どのガードも真でない場合、結果は未定義である。少なくとも1つのガードが真でなければならないので、空文の Skip を使うことが多い。以下のような擬似コードを考える:GCL ではこれが以下のようになる:擬似コード:GCLの場合:2つ目のガードを省いた場合、error = False なら、結果は Abort となる。a = b の場合、max の新たな値として a または b が選ばれるが、結果は同じである。しかし、実装によっては、一方がもう一方より性能的に有利だったり容易だったりする場合もある。プログラマから見れば違いはないので、いかようにも実装してよい。繰り返しは、全てのガードが真でなくなるまでガード付きコマンド群を繰り返し実行する。通常、ガードはひとつだけである。この繰り返しは a = b のとき終了し、その際に a と b には A と B の最大公約数が格納されている。この繰り返しは b = 0 のとき終了し、その際に各変数は xa + yb = gcd(a,b) の解を格納している。GCLでは、異なるコマンドの選択による様々な遅延を許容した繰り返しが可能であるため、QDIモデル（Quasi Delay Insensitive）に基づいた回路設計に適している。この場合、以下のようにノード "y" を駆動する論理ゲートは2つのガード付きコマンドで表現される。"PulldownGuard" と "PullupGuard" はその論理ゲートの入力の関数であり、それぞれゲートの出力を上げたり下げたりする。古典的な回路評価モデルとは異なり、（非同期回路に対応した）ガード付きコマンド群の繰り返しは、正確にその回路の全ての動的振る舞いを説明できる。モデルによっては、ガード付きコマンドに何らかの制限を加える必要があるだろう。典型的な制限としては、安定性、非干渉、自己無効化コマンドを許さない、などがある。ガード付きコマンドは Promela というプログラミング言語で使われている。Promela はSPINモデルチェッカで使われている。SPINは並行ソフトウェアアプリケーションのモデル検査用ツールである。Perlの Commands::Guarded モジュールは、ダイクストラのガード付きコマンドを決定論的に修正したバージョンである。

出典:wikipedia