Guarded Command Language
Guarded Command Language（GCL）とは、エドガー・ダイクストラが述語変換意味論向けに定義した言語である
ガード付きコマンド
ガード付きコマンドはGCLの最重要要素である。ガード付きコマンドは名前の通り、ガードが付いている。ガードは一種の命題であり、その文を実行する前に真でなければならない。文の実行前に、そのガードは真であると仮定される。また、ガードが偽であった場合、その文は実行されない。ガード付きコマンドを使うことで、プログラムがその仕様に適合していることを証明することが容易になる。ガード付きコマンドの本体（実行すべき文）がガード付きコマンドになっていることが多い。
Skip と Abort
Skip と Abort は非常に単純だがガード付きコマンドと同様に重要な要素である。Abort は未定義命令であり、何もしない。Abort は完了することさえ保証されていない。プログラムが何らかの証明の定式化であるとすれば、Abort は証明の失敗に対応する。Skip は空の命令であり、何もしない。文法上、文が必要とされるが、プログラマが状態を変更したくない場合、プログラム内で使われる。
代入
代入文は変数に値を代入する。
連結
代入文はセミコロン(;)を間に書いて、並べて記述される。
条件文: if
選択（一般に、条件文とかif文と呼ばれる）はガード付きコマンドのリストであり、そのうちの1つの文が選択実行される。複数のガードが真である場合、実行する文はランダムまたは非決定的に選択される。どのガードも真でない場合、結果は未定義である。少なくとも1つのガードが真でなければならないので、空文の Skip を使うことが多い。
繰り返し: do
繰り返しは、全てのガードが真でなくなるまでガード付きコマンド群を繰り返し実行する。通常、ガードはひとつだけである。
モデル検査
ガード付きコマンドは Promela というプログラミング言語で使われている。Promela はSPINモデルチェッカで使われている。SPINは並行ソフトウェアアプリケーションのモデル検査用ツールである。
その他
Perlの Commands::Guarded モジュールは、ダイクストラのガード付きコマンドを決定論的に修正したバージョンである。