Guarded Command Language
以下のような擬似コードを考える:
if a < b then c := True
else c := False
GCL ではこれが以下のようになる:
if {\displaystyle {\mbox{if}}} a < b → c := T r u e {\displaystyle a<b\rightarrow c:=True} [ ] a ≥ b → c := F a l s e {\displaystyle []\ a\geq b\rightarrow c:=False}
fi {\displaystyle {\mbox{fi}}}
Guarded Command Language(GCL)とは、エドガー・ダイクストラが述語変換意味論向けに定義した言語である
繰り返しは、全てのガードが真でなくなるまでガード付きコマンド群を繰り返し実行する。通常、ガードはひとつだけである。
do {\displaystyle {\mbox{do}}} G 0 → S 0 {\displaystyle G_{0}\rightarrow S_{0}} [ ] G 1 → S 1 {\displaystyle []\ G_{1}\rightarrow S_{1}} . . . {\displaystyle ...} [ ] G n → S n {\displaystyle []\ G_{n}\rightarrow S_{n}}
od {\displaystyle {\mbox{od}}}