ガードコマンド言語

ガードコマンド言語（GCL）は、EWD472で述語変換器の意味論のためにエドガー・ダイクストラによって定義されたプログラミング言語です。 ^[1]これは、プログラミングの概念をコンパクトに組み合わせたものです。証明のアイデアが先導することで、プログラムとその証明を連携して開発することが容易になり、さらに、プログラムの一部を実際に計算することもできます。

GCLの重要な特性は非決定性です。たとえば、if 文では複数の選択肢が真になる可能性があり、どれを選択するかは実行時、つまり if 文が実行されるときに決定されます。これにより、プログラマーは不必要な選択を行う必要がなくなり、プログラムの正式な開発に役立ちます。

GCL には多重代入文が含まれています。たとえば、文の実行は、まず右側の値を評価し、次にそれを左側の変数に格納することによって行われます。したがって、この文はxとyx, y:= y, xの値を入れ替えます。

以下の書籍では、 GCL を使用したプログラムの開発について説明しています。

• ダイクストラ、エドガー W. (1976)。プログラミングの規律。プレンティス ホール。ISBN 978-0132158718。
• Gries, D. ( 1981 )。プログラミングの科学。コンピュータサイエンスのモノグラフ（英語、スペイン語、日本語、中国語、イタリア語、ロシア語）。ニューヨーク：Springer Verlag。doi :10.1007 / 978-1-4612-5983-1。ISBN 978-0-387-96480-5. S2CID  37034126。
• ダイクストラ、エドガー・W. ;フェイジェン、ウィム HJ (1988)。プログラミングの方法。マサチューセッツ州ボストン: Addison-Wesley Longman Publishing Co., Inc. p. 200.ISBN​ 978-0-201-17536-3。
• カルデワイジ、アン（1990）。プログラミング：アルゴリズムの導出。Prentice-Hall、Inc。ISBN 0132041081。
• コーエン、エドワード(1990)。デイビッド・グリース(編)。1990 年代のプログラミング: プログラム計算入門。コンピュータサイエンスのテキストとモノグラフ。Springer Verlag。doi :10.1007/ 978-1-4613-9706-9。ISBN 978-1-4613-9706-9. S2CID  1509875。

ガード付きコマンドは、ブール条件またはガードと、それによって「ガード」されるステートメントで構成されます。ステートメントはガードが true の場合にのみ実行されるため、ステートメントについて推論する際には、条件が true であると想定できます。これにより、プログラムが仕様を満たしていることを証明しやすくなります。

ガードコマンドとは、G → Sの形式の 文であり、

• Gはガードと呼ばれる命題である
• Sは文である

• G が true と評価された場合、S は実行対象となります。ほとんどの GCL 構造では、複数のガード付きコマンドに true のガードがある場合があり、そのうちの 1 つが任意に選択されて実行されます。
• G が偽の場合、S は実行されません。

skipとabort は、ガード付きコマンド言語の重要なステートメントです。abortは未定義の命令で、何でも実行します。終了する必要すらありません。証明を作成するときにプログラムを記述するために使用されますが、その場合、証明は通常失敗します。skipは空の命令で、何も実行しません。構文でステートメントが必要であるが状態は変更すべきでない場合によく使用されます。

スキップ

アボート

• スキップ: 何もしない
• 中止: 何もしない

変数に値を割り当てます。

v := E

または

v 0 , v 1 , ..., v n  := E 0 , E 1 , ..., E n

どこ

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

文はセミコロン (;) で区切られます。

選択 (多くの場合、「条件文」または「if 文」と呼ばれます) は、ガードされたコマンドのリストであり、そのうちの 1 つが実行対象として選択されます。複数のガードが true の場合、ガードが true である 1 つの文が任意に選択されて実行されます。ガードが true でない場合、結果は未定義、つまりabortと同等になります。ガードのうち少なくとも 1 つは true でなければならないため、空の文skipが必要になることがよくあります。文if fiにはガードされたコマンドがないため、真のガードは存在しません。したがって、if fi はabortと同等です。

G0 → S0の場合
 □ G1 → S1
...
 □ グン → スン
フィ

選択の実行時に、ガードが評価されます。ガードがいずれもtrueでない場合、選択は中止されます。そうでない場合は、ガードがtrueである節の 1 つが任意に選択され、そのステートメントが実行されます。

GCL は実装を指定しません。ガードは副作用を持つことができず、節の選択は任意であるため、実装では任意の順序でガードを評価し、たとえば 最初のtrue節を選択できます。

疑似コードでは:

a < b の場合は c を True に設定する
それ以外の場合はcをFalseに設定する

ガード付きコマンド言語の場合:

a < b → c の場合:= true
 □ a ≥ b → c := 偽
フィ

疑似コードでは:

エラーがTrueの場合、xを0に設定する

ガード付きコマンド言語の場合:

エラーの場合→ x := 0
 □エラー→スキップ${\displaystyle \neg}$

2 番目のガードが省略され、エラーが False の場合、結果は中止になります。

a ≥ b → 最大値 := a の場合
 □ b ≥ a → 最大値 := b
フィ

a = b の場合、最大値の新しい値として a または b のいずれかが選択され、結果は同じになります。ただし、実装によって、どちらか一方が他方よりも簡単または高速になる場合があります。プログラマーにとって違いはないため、どの実装でもかまいません。

この繰り返し、つまりループの実行を以下に示します。

G0 → S0を実行する
 □ G1 → S1
...
 □ グン → スン
od

繰り返しの実行は、0 回以上の反復の実行で構成されます。反復は、ガードGiが true であるガード付きコマンドGi → Si を任意に選択し、コマンドSi を実行することで構成されます。したがって、すべてのガードが最初は false の場合、繰り返しは反復を実行せずに直ちに終了します。ガード付きコマンドを持たない繰り返しdo odの実行は 0 回の反復を実行するため、 do od はskipと同等です。

a, b := A, B;
 a < b → b := b - aを実行します。
 □ b < a → a := a - b
od

この繰り返しは a = b のときに終了し、その場合、a と b はA と B の 最大公約数を保持します。

ダイクストラはこのアルゴリズムの中に、と が真のままとなるa := a - bようb := b - aな2 つの無限サイクルを同期させる方法を見出しました。 a≥0b≥0

a, b, x, y, u, v := A, B, 1, 0, 0, 1;
 b ≠ 0とします→
   q, r := a div b, a mod b;
   a、b、x、y、u、v := b、r、u、v、x - q*u、y - q*v
od

この繰り返しは b = 0 のときに終了し、その場合、変数はベズーの恒等式の解xA + yB = gcd(A,B) を保持します。

a>b → a, b := b, aを実行します。
 □ b>c → b, c := c, b
 □ c>d → c, d := d, c
od

プログラムは、要素の 1 つが次の要素よりも大きい間は、要素の順序を変え続けます。この非決定論的バブル ソートは、決定論的バージョンよりも効率的ではありませんが、証明は簡単です。要素がソートされていない間は停止せず、各ステップで少なくとも 2 つの要素をソートします。

x, y = 1, 1;
 x≠n
   とする→ f(x) ≤ f(y)の場合→ x := x+1
    □ f(x) ≥ f(y) → y := x; x := x+1
   フィオド
​

このアルゴリズムは、与えられた整数関数fが最大となる値 1 ≤ y ≤ n を見つけます。計算だけでなく最終状態も必ずしも一意に決まるわけではありません。

ガードコマンドの観測的合同性を格子に一般化することで、改良計算が生まれました。^[2]これは、B法などの形式手法で機械化されており、仕様からプログラムを形式的に導出することができます。

ガードされたコマンドは、繰り返しによって異なるコマンドの選択に任意の相対遅延が許容されるため、準遅延不感の回路設計に適しています。このアプリケーションでは、回路内のノードy を駆動するロジック ゲートは、次の 2 つのガードされたコマンドで構成されます。

プルダウンガード → y := 0
プルアップガード → y := 1

ここでのPullDownGuardとPullUpGuard は、論理ゲートの入力の関数であり、ゲートが出力をそれぞれプルダウンまたはプルアップするタイミングを表します。従来の回路評価モデルとは異なり、ガードされたコマンドのセット (非同期回路に対応) の繰り返しにより、その回路のあらゆる動的動作を正確に記述できます。電気回路要素にどのようなモデルを採用するかによって、ガードされたコマンドの記述を完全に満足のいくものにするために、ガードされたコマンドに対する追加の制限が必要になる場合があります。一般的な制限には、安定性、非干渉性、自己無効化コマンドの不在などがあります。^[3]

ガードされたコマンドは、 SPIN モデル チェッカーで使用されるPromelaプログラミング言語内で使用されます。SPIN は、同時実行ソフトウェア アプリケーションの正しい動作を検証します。

Perl モジュール Commands::Guarded は、Dijkstra のガードされたコマンドの決定論的かつ修正的なバリアントを実装します。