構文

ガード付きコマンドは、 ${\displaystyle G\rightarrow {S}}$ という形式の文であり、ここで

• ${\displaystyle G}$ は、ガードと呼ばれる命題である。
• ${\displaystyle S}$ は文である。

${\displaystyle G\equiv {\mbox{True}}}$ なら、ガード付きコマンドは単に ${\displaystyle S}$ と記述される。

意味論

計算の流れで ${\displaystyle G}$ が出てくると、それを評価する。

• ${\displaystyle G}$ が真なら ${\displaystyle S}$ を実行する。
• ${\displaystyle G}$ が偽なら、コンテキストに従って次にすべきことを決定する。

構文

• Skip
• Abort

意味論

• Skip: 何もしない
• Abort: 何もしない

構文

• ${\displaystyle v:=E}$
• ${\displaystyle v_{0},v_{1},...,v_{n}:=E_{0},E_{1},...,E_{n}}$

ここで

• v はプログラムの変数（群）
• E は対応する変数と同じデータ型の式

構文

${\displaystyle {\mbox{if}}}$

${\displaystyle G_{0}\rightarrow S_{0}}$

${\displaystyle []\ G_{1}\rightarrow S_{1}}$

${\displaystyle ...}$

${\displaystyle []\ G_{n}\rightarrow S_{n}}$

${\displaystyle {\mbox{fi}}}$

意味論

• どのガードも真でない場合: Abort と同じ
• 1つの ${\displaystyle G_{x}}$ だけが真の場合、${\displaystyle S_{x}}$ を実行
• ${\displaystyle G_{x_{0}}\ ...\ G_{x_{m}}}$ がいずれも真の場合、任意の ${\displaystyle S_{x_{y}}}$（ただし ${\displaystyle 0\leq y\leq m}$）を実行

例

構文

${\displaystyle {\mbox{do}}}$

${\displaystyle G_{0}\rightarrow S_{0}}$

${\displaystyle []\ G_{1}\rightarrow S_{1}}$

${\displaystyle ...}$

${\displaystyle []\ G_{n}\rightarrow S_{n}}$

${\displaystyle {\mbox{od}}}$

意味論

• 全てのガードが真でない場合: Skip
• ${\displaystyle G_{x}}$ だけが真の場合: ${\displaystyle S_{x}}$ を実行し、再度ガード群を評価する
• ${\displaystyle G_{x_{0}}\ ...\ G_{x_{m}}}$ が真の場合: いずれかの ${\displaystyle S_{x_{y}}}$ （ただし、${\displaystyle 0\leq y\leq m}$）を実行し、再度ガード群を評価する

例

非同期回路

GCLでは、異なるコマンドの選択による様々な遅延を許容した繰り返しが可能であるため、QDIモデル（Quasi Delay Insensitive）に基づいた回路設計に適している。この場合、以下のようにノード y を駆動する論理ゲートは2つのガード付きコマンドで表現される。

${\displaystyle PulldownGuard\rightarrow y:=0}$

${\displaystyle PullupGuard\rightarrow y:=1}$

PulldownGuard と PullupGuard はその論理ゲートの入力の関数であり、それぞれゲートの出力を上げたり下げたりする。古典的な回路評価モデルとは異なり、（非同期回路に対応した）ガード付きコマンド群の繰り返しは、正確にその回路の全ての動的振る舞いを説明できる。モデルによっては、ガード付きコマンドに何らかの制限を加える必要があるだろう。典型的な制限としては、安定性、非干渉、自己無効化コマンドを許さない、などがある^[2]。

モデル検査

ガード付きコマンドは Promela というプログラミング言語で使われている。Promela はSPINモデルチェッカで使われている。SPINは並行ソフトウェアアプリケーションのモデル検査用ツールである。

その他

Perlの Commands::Guarded モジュールは、ダイクストラのガード付きコマンドを決定論的に修正したバージョンである。