Guarded Command Language
a , b := A , B ; {\displaystyle a,b:=A,B;}
do {\displaystyle {\mbox{do}}} a > b → a := a − b {\displaystyle a>b\rightarrow a:=a-b} [ ] b > a → b := b − a {\displaystyle []\ b>a\rightarrow b:=b-a}
od {\displaystyle {\mbox{od}}}
この繰り返しは a = b のとき終了し、その際に a と b には A と B の最大公約数が格納されている。
Skip: 何もしない
Abort: 何もしない
v := E {\displaystyle v:=E}
v 0 , v 1 , . . . , v n := E 0 , E 1 , . . . , E n {\displaystyle v_{0},v_{1},...,v_{n}:=E_{0},E_{1},...,E_{n}}
ここで
v はプログラムの変数(群)
E は対応する変数と同じデータ型の式
ガード付きコマンドは Promela というプログラミング言語で使われている。Promela はSPINモデルチェッカで使われている。SPINは並行ソフトウェアアプリケーションのモデル検査用ツールである。
GCLでは、異なるコマンドの選択による様々な遅延を許容した繰り返しが可能であるため、QDIモデル(Quasi Delay Insensitive)に基づいた回路設計に適している。この場合、以下のようにノード y を駆動する論理ゲートは2つのガード付きコマンドで表現される。
P u l l d o w n G u a r d → y := 0 {\displaystyle PulldownGuard\rightarrow y:=0}
P u l l u p G u a r d → y := 1 {\displaystyle PullupGuard\rightarrow y:=1}
PulldownGuard と PullupGuard はその論理ゲートの入力の関数であり、それぞれゲートの出力を上げたり下げたりする。古典的な回路評価モデルとは異なり、(非同期回路に対応した)ガード付きコマンド群の繰り返しは、正確にその回路の全ての動的振る舞いを説明できる。モデルによっては、ガード付きコマンドに何らかの制限を加える必要があるだろう。典型的な制限としては、安定性、非干渉、自己無効化コマンドを許さない、などがある。