Guarded Command Language

ガード付きコマンドはGCLの最重要要素である。ガード付きコマンドは名前の通り、ガードが付いている。ガードは一種の命題であり、その文を実行する前に真でなければならない。文の実行前に、そのガードは真であると仮定される。また、ガードが偽であった場合、その文は実行されない。ガード付きコマンドを使うことで、プログラムがその仕様に適合していることを証明することが容易になる。ガード付きコマンドの本体（実行すべき文）がガード付きコマンドになっていることが多い。

ガード付きコマンドは、 ${\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 は非常に単純だがガード付きコマンドと同様に重要な要素である。Abort は未定義命令であり、何もしない。Abort は完了することさえ保証されていない。プログラムが何らかの証明の定式化であるとすれば、Abort は証明の失敗に対応する。Skip は空の命令であり、何もしない。文法上、文が必要とされるが、プログラマが状態を変更したくない場合、プログラム内で使われる。

• Skip
• Abort

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

代入文は変数に値を代入する。

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

ここで

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

代入文はセミコロン(;)を間に書いて、並べて記述される。

Summarize Timeline Fact Check

選択（一般に、条件文とかif文と呼ばれる）はガード付きコマンドのリストであり、そのうちの1つの文が選択実行される。複数のガードが真である場合、実行する文はランダムまたは非決定的に選択される。どのガードも真でない場合、結果は未定義である。少なくとも1つのガードが真でなければならないので、空文の Skip を使うことが多い。

${\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}$）を実行

以下のような擬似コードを考える:

if a < b then c := True

else c := False

GCL ではこれが以下のようになる:

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

${\displaystyle a<b\rightarrow c:=True}$

${\displaystyle []\ a\geq b\rightarrow c:=False}$

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

擬似コード:

if error = True then x := 0

GCLの場合:

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

${\displaystyle error={\mbox{True}}\rightarrow x:=0}$

${\displaystyle []\ error={\mbox{False}}\rightarrow {\mbox{skip}}}$

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

2つ目のガードを省いた場合、error = False なら、結果は Abort となる。

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

${\displaystyle a\geq b\rightarrow max:=a}$

${\displaystyle []\ a\leq b\rightarrow max:=b}$

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

a = b の場合、max の新たな値として a または b が選ばれるが、結果は同じである。しかし、実装によっては、一方がもう一方より性能的に有利だったり容易だったりする場合もある。プログラマから見れば違いはないので、いかようにも実装してよい。