述語変換子の意味論

述語変換子意味論は、エドガー・ダイクストラが彼の画期的な論文「ガード付きコマンド、非決定性、そしてプログラムの形式的導出」で導入しました。この意味論は、命令型プログラミングパラダイムの意味論を定義するもので、この言語の各文に対応する述語変換子（文の状態空間における2つの述語間の全関数）を割り当てます。この意味で、述語変換子意味論は一種の表示的意味論です。実際、ガード付きコマンドにおいて、ダイクストラは1種類の述語変換子、すなわちよく知られている最弱前提条件（下記参照）のみを使用しています。

さらに、述語変換意味論はフロイド・ホーア論理を再定式化したものである。ホーア論理は演繹体系として提示されるのに対し、述語変換意味論（最弱前提条件または最強事後条件のいずれかによる。下記参照）は、ホーア論理の有効な演繹を構築するための完全な戦略である。言い換えれば、ホーア三項の検証問題を一階述語論理式を証明する問題に縮減する効果的なアルゴリズムを提供する。技術的には、述語変換意味論は、文を述語に変換する一種の記号実行を実行する。つまり、最弱前提条件の場合は逆方向に実行し、最強事後条件の場合は順方向に実行することとなる。

最も弱い前提条件

意味

文Sと事後条件 Rについて、最も弱い前提条件とは、任意の前提条件 $P$ に対して、が成り立つ場合のみとなる述語Qです。言い換えれば、これはSの後にR が成り立つことを保証するために必要な、最も「緩い」、つまり最も制限の少ない要件です。一意性は定義から容易に得られます。QとQ ' の両方が最も弱い前提条件である場合、定義により、となり、したがってとなります。事後条件Rに関して文Sの最も弱い前提条件を表すために、しばしばを使用します。 $\{P\}S\{R\}$ $P\Rightarrow Q$ $\{Q'\}S\{R\}$ $Q'\Rightarrow Q$ $\{Q\}S\{R\}$ $Q\Rightarrow Q'$ $Q=Q'$ $wp(S,R)$

コンベンション

Tはどこでも真となる述語、F はどこでも偽となる述語を表します。言語構文で定義されたブール式と概念的に混同しないようにする必要があります。ブール式には、ブールスカラーとして true と false が含まれる可能性があります。このようなスカラーに対しては、T = predicate(true)、F = predicate(false) という型変換を行う必要があります。このような型変換はしばしば何気なく行われるため、T を真、F を偽と解釈してしまう傾向があります。

スキップ

wp({\texttt {skip}},R)\ =\ R

アボート

wp({\texttt {abort}},R)\ =\ {\texttt {F}}

割り当て

以下に、代入文に対する2つの同等な最弱前提条件を示します。これらの式では、はRのコピーであり、xの自由出現がEに置き換えられています。したがって、ここで式Eは暗黙的に基礎ロジックの有効な項に変換されます。つまり、 E は純粋な式であり、完全に定義され、終了し、副作用がありません。 $R[x\leftarrow E]$

バージョン1:

wp(x:=E,R)\ =\ (\forall y.y=E\Rightarrow R[x\leftarrow y])

ここで、yは新しい変数であり、EとRでは自由ではない（変数xの最終値を表す）

バージョン2:

Eが明確に定義されていると仮定すると、バージョン1にいわゆる一点ルールを適用するだけです。すると

wp(x:=E,R)\ =\ R[x\leftarrow E]

最初のバージョンはRにおけるxの重複を回避しますが、2番目のバージョンはRにおけるxの出現回数が最大でも1回である場合に単純化されます。また、最初のバージョンは、最も弱い前提条件と最も強い事後条件の間に深い二重性があることを明らかにしています（下記参照）。

整数値の変数xへの割り当てに対するwp (バージョン 2 を使用)の有効な計算の例は次のとおりです。

{\begin{array}{rcl}wp(x:=x-5,x>10)&=&x-5>10\\&\Leftrightarrow &x>15\end{array}}

これは、代入後に事後条件x > 10 が真となるためには、代入前に前提条件x > 15 が真でなければならないことを意味します。これはまた、「最も弱い前提条件」でもあり、代入後にx > 10 を真とするxの値に対する「最も弱い」制約です。

順序

wp(S_{1};S_{2},R)\ =\ wp(S_{1},wp(S_{2},R))

例えば、

{\begin{array}{rcl}wp(x:=x-5;x:=x*2\ ,\ x>20)&=&wp(x:=x-5,wp(x:=x*2,x>20))\\&=&wp(x:=x-5,x*2>20)\\&=&(x-5)*2>20\\&=&x>15\end{array}}

条件付き

wp({\texttt {if}}\ E\ {\texttt {then}}\ S_{1}\ {\texttt {else}}\ S_{2}\ {\texttt {end}},R)\ =\ (E\Rightarrow wp(S_{1},R))\wedge (\neg E\Rightarrow wp(S_{2},R))

例:

{\begin{array}{rcl}wp({\texttt {if}}\ x<y\ {\texttt {then}}\ x:=y\ {\texttt {else}}\;\;{\texttt {skip}}\;\;{\texttt {end}},\ x\geq y)&=&(x<y\Rightarrow wp(x:=y,x\geq y))\ \wedge \ (\neg (x<y)\Rightarrow wp({\texttt {skip}},x\geq y))\\&=&(x<y\Rightarrow y\geq y)\ \wedge \ (\neg (x<y)\Rightarrow x\geq y)\\&\Leftrightarrow &{\texttt {true}}\end{array}}

whileループ

部分的な正しさ

一旦終了を無視すると、通常はプログラマーが提供するループ INVアリアントと呼ばれる述語INVを使用して、 wlpで表される最も弱いリベラル前提条件のルールを定義できます。

wlp({\texttt {while}}\ E\ {\texttt {do}}\ S\ {\texttt {done}},R)\Leftarrow \ {\textit {INV}}\ \ {\text{if}}\ \ {\begin{array}{l}\\(E\wedge {\textit {INV}}\Rightarrow wlp(S,{\textit {INV}}))\\\wedge \ (\neg E\wedge {\textit {INV}}\Rightarrow R)\end{array}}

完全な正確さ

完全な正しさを示すためには、ループが終了することも示さなければなりません。そのために、状態空間上に ( $wfs , <) と表記される$ well-founded な関係を定義し、次式となるような変種関数 $vfを定義します。$

wp({\texttt {while}}\ E\ {\texttt {do}}\ S\ {\texttt {done}},R)\ \Leftarrow \ {\textit {INV}}\ \ {\text{if}}\ \ \ \ {\begin{array}{l}\\(E\wedge {\textit {INV}}\Rightarrow {\textit {vf}}\in {\textit {wfs}})\\\wedge \ (E\wedge {\textit {INV}}\wedge v={\textit {vf}}\Rightarrow wp(S,{\textit {INV}}\wedge v<{\textit {vf}}))\\\wedge \ (\neg E\wedge {\textit {INV}}\Rightarrow R)\end{array}}

ここで $v$ は変数の新しいタプルである

非公式には、上記の 3 つの式を結合すると次のようになります。

最初のものは、ループに入る前にバリアントが well-founded 関係の一部でなければならないことを意味します。
2 番目は、ループ本体 (つまりステートメント $S$ ) が不変式を保持し、変数を削減する必要があることを意味します。
最後のは、ループが終了したときにループ事後条件 $R$ が確立される必要があることを意味します。

しかし、これら3つの条件が揃うことは必ずしも必要条件ではありません。

wp({\texttt {while}}\ E\ {\texttt {do}}\ S\ {\texttt {done}},R)\ \ =\ \ {\text{the strongest solution of the recursive equation}}\ {\begin{array}{l}Z:[Z\equiv (E\wedge wp(S,Z))\vee (\neg E\wedge R)]\end{array}}

非決定論的なガードコマンド

実際、ダイクストラのガード付きコマンド言語（GCL）は、これまで示してきた単純な命令型言語を非決定的な文で拡張したものです。GCLはアルゴリズムを定義するための形式的な記法となることを目指しています。非決定的な文は、（効果的なプログラミング言語において）実際の実装に委ねられた選択肢を表します。つまり、非決定的な文で証明される特性は、あらゆる実装の選択肢に対して保証されます。言い換えれば、非決定的な文の最弱前提条件は、

終了する実行が存在すること（例えば実装が存在すること）
そして、すべての終了実行の最終状態が事後条件を満たすこと。

上記の最も弱い前提条件の定義 (特にwhile ループの場合) では、このプロパティが保持されることに注意してください。

選択

選択はifステートメントの一般化です。

wp({\texttt {if}}\ E_{1}\rightarrow S_{1}\ [\!]\ \ldots \ [\!]\ E_{n}\rightarrow S_{n}\ {\texttt {fi}},R)\ ={\begin{array}{l}(E_{1}\vee \ldots \vee E_{n})\\\wedge \ (E_{1}\Rightarrow wp(S_{1},R))\\\ldots \\\wedge \ (E_{n}\Rightarrow wp(S_{n},R))\\\end{array}}

^[要引用]

ここで、2 つのガードとが同時に真である場合、この文を実行すると、関連付けられている文またはのいずれかが実行されます。 $E_{i}$ $E_{j}$ $S_{i}$ $S_{j}$

繰り返し

繰り返しは、同様の方法でwhileステートメントを一般化したものです。

仕様書

精緻化計算はGCLを仕様記述の概念で拡張する。構文的には、仕様記述は次のように記述する。

  $x:l[pre,post]$

これは、 preを満たす状態から始まり、 xのみを変更することでpostを満たす状態に終了することが保証されている計算を指定します。指定を補助するために用いられる論理定数を、ここでは論理定数と呼びます。例えば、xを1ずつ増やす計算は次のように指定できます。 $l$

  $x:l[x=l,x=l+1]$

もう 1 つの例は、整数の平方根の計算です。

  $x:l[x=l^{2},x=l]$

仕様記述文は、他の文を含まないという意味でプリミティブな文のように見えます。しかし、preとpostが任意の述語であるため、非常に表現力に優れています。最も弱い前提条件は次のとおりです。

wp(x:l[pre,post],R)=(\exists l::pre)\wedge (\forall s:(\forall l:pre:post(x\leftarrow s)):R(x\leftarrow s))

ここで、sは新鮮です。

これは、Morganの構文的アイデアと、Bijlsma、Matthews、Wiltinkによる鋭さの考え方を組み合わせたものです。^[1] この利点は、goto Lやその他のジャンプ文のwpを定義できることです。^[2]

Goto文

goto Lのようなジャンプ文の形式化は、非常に長く困難なプロセスを経る。一般的には、goto文は操作的にしか論じられないと考えられているようだ。これはおそらく、goto Lが実際には奇跡的（つまり非正格）であり、ダイクストラの考案した奇跡排除の法則に従わないことを認識していないためだろう。しかし、最弱の前提条件の観点からは、非常に単純な操作的視点から見ることができる。これは予想外だった。我々は次のように定義する。

wp({\texttt {goto}}\ L,R)=wpL

ここで、wpLはラベルLにおける最も弱い前提条件です。

goto Lの場合、実行は最も弱い前提条件が満たされるラベルLに制御を移します。 wpLが規則で参照される方法は、それほど驚くべきことではありません。それは、その時点までに計算された何らかのQに対して⁠ ⁠であるだけです。これは、 goto L がプリミティブに見えても、構成ステートメントを使用して wp 定義を与える他の wp 規則と同様です。この規則は、プログラム内でwpLが保持される場所の一意性を要求しないため、理論的には、各場所の最も弱い前提条件が同じ wpL である限り、同じラベルが複数の場所に出現することを許可します。 goto ステートメントは、そのような場所のいずれかにジャンプできます。これは実際に、⁠ ⁠のように、同じラベルを同じ場所に複数回配置できることを正当化します。これは⁠ ⁠と同じです。また、これはスコープ規則を意味しないため、たとえばループ本体へのジャンプが可能です。ループ本体へのジャンプがある次のプログラム S の wp を計算してみましょう。 $wp(L:S,Q)$ $S(L:L:S1)$ $S(L:S1)$

 wp(do x > 0 → L: x := x-1 od; if x < 0 → x := -x; goto L ⫿ x ≥ 0 → skip fi, post) = { 順次合成と交替の規則 } wp(do x > 0 → L: x := x-1 od, (x<0 ∧ wp(x := -x; L, post へ移動)) ∨ (x ≥ 0 ∧ post) = { 順次合成、goto、代入規則 } wp(do x > 0 → L: x := x-1 od, x<0 ∧ wpL(x ← -x) ∨ x≥0 ∧ post) = {繰り返しルール} 最強の解決策 Z: [ Z ≡ x > 0 ∧ wp(L: x := x-1, Z) ∨ x < 0 ∧ wpL(x ← -x) ∨ x=0 ∧ post ]  = { 割り当て規則、wpL = Z(x ← x-1) が見つかりました } 最強の解決策 Z: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x=0 ∧ ポスト] = { 置換 } 最強の解決策 Z:[ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x=0 ∧ ポスト ] = { 近似的に方程式を解く } 投稿(x ← 0)

したがって、

wp(S, post) = post(x ← 0) です。

その他の述語変換子

最も弱いリベラルな前提条件

最弱前提条件の重要な変種として、最弱リベラル前提条件がある。これは、 S が停止しないかRを確立する最も弱い条件となる。したがって、停止を保証しない点でwpと異なる。したがって、部分的な正しさにおいてホーア論理に対応する。上記の文言語において、wlp はwhile ループにおいてのみwpと異なり、変種を必要としない（上記参照）。 $wlp(S,R)$

最も強い事後条件

Sが文でR が前提条件(初期状態に対する述語)である場合、はそれらの最も強い事後条件です。つまり、R を満たす任意の初期状態に対して、S の任意の実行の最終状態によって満たされる任意の事後条件を意味します。言い換えると、Hoare トリプルは、以下の述語が成り立つ場合のみ、Hoare 論理で証明可能です。 $sp(S,R)$ $\{P\}S\{Q\}$

\forall x,sp(S,P)\Rightarrow Q

通常、最も強い事後条件は部分的な正しさのために使用されます。したがって、最も弱いリベラルな事前条件と最も強い事後条件の間には、次のような関係があります。

(\forall x,P\Rightarrow wlp(S,Q))\ \Leftrightarrow \ (\forall x,sp(S,P)\Rightarrow Q)

たとえば、課題には次のようなものがあります。

sp(x:=E,R)\ =\ \exists y,x=E[x\leftarrow y]\wedge R[x\leftarrow y]

ここでyは新鮮度

上記では、論理変数yは変数xの初期値を表しています。したがって、

sp(x:=x-5,x>15)\ =\ \exists y,x=y-5\wedge y>15\ \Leftrightarrow \ x>10

シーケンス上、 sp は前方に実行されるように見えます(一方、wp は後方に実行されます)。

sp(S_{1};S_{2}\ ,\ R)\ =\ sp(S_{2},sp(S_{1},R))

勝利と罪の述語変換子

レスリー・ランポートは並行プログラミングのための述語変換器としてwinとsinを提案した。^[3]

述語変換子のプロパティ

この節では、述語変換子の特徴的な性質をいくつか示す。^[4]以下、S は述語変換子（状態空間上の2つの述語間の関数）を表し、P は述語を表す。例えば、S(P)はwp(S,P)またはsp(S,P)を表す。xは状態空間の変数とする。

単調

対象となる述語変換器（wp、wlp、およびsp）は単調です。述語変換器Sが単調となるのは、以下の場合のみです。

(\forall x:P:Q)\Rightarrow (\forall x:S(P):S(Q))

この特性は、ホーア論理の結果規則に関連しています。

厳しい

述語変換器Sが正格である場合、次の条件を満たす:

S({\texttt {F}})\ \Leftrightarrow \ {\texttt {F}}

例えば、wpは人為的に正格にされているが、wlpは一般的には正格ではない。特に、文Sが終了しない場合は、文Sは充足可能である。 $wlp(S,{\texttt {F}})$

wlp({\texttt {while}}\ {\texttt {true}}\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}},{\texttt {F}})\ \Leftrightarrow {\texttt {T}}

実際、Tはそのループの有効な不変量です。

非厳密だが単調または連言的な述語変換子は奇跡的（miraculous）と呼ばれ、プログラミング構造のクラス、特にダイクストラがあまり重視しなかったジャンプ文を定義するためにも使用できます。これらのジャンプ文には、直接的なgoto L、ループ内のbreakとcontinue、手続き本体内のreturn文、例外処理などが含まれます。すべてのジャンプ文は実行可能な奇跡的（miraculous）^[5]、つまり実装は可能だが厳密ではないことが判明しています。

終了中

述語変換器Sは次の場合に終了します。

S({\texttt {T}})\ \Leftrightarrow \ {\texttt {T}}

実際、この用語は厳密な述語変換器に対してのみ意味を持ちます。つまり、はSの終了を保証する最も弱い前提条件です。 $wp(S,{\texttt {T}})$

このプロパティを「非中止」と名付ける方が適切と思われます。完全な正しさでは、非終了は中止ですが、部分的な正しさでは中止ではありません。

接続詞

述語変換子Sが連言的である場合、その条件は次の通りです。

S(P\wedge Q)\ \Leftrightarrow \ S(P)\wedge S(Q)

これは、文S が選択文または仕様文として非決定的であっても当てはまります。 $wp(S,.)$

分離的

述語変換子Sが選言的である場合、その条件は次の通りです。

S(P\vee Q)\ \Leftrightarrow \ S(P)\vee S(Q)

Sが非決定性である場合、これは一般的には当てはまりません。実際、任意のブール値を選択する非決定性文Sを考えてみましょう。この文は、ここでは以下の選択文として与えられます。 $wp(S,.)$

S\ =\ {\texttt {if}}\ {\texttt {true}}\rightarrow x:=0\ [\!]\ {\texttt {true}}\rightarrow x:=1\ {\texttt {fi}}

すると、は式に簡約されます。 $wp(S,R)$ $R[x\leftarrow 0]\wedge R[x\leftarrow 1]$

したがって、トートロジーとなる。 $wp(S,\ x=0\vee x=1)$ $(0=0\vee 0=1)\wedge (1=0\vee 1=1)$

一方、式は間違った命題に帰着します。 $wp(S,x=0)\vee wp(S,x=1)$ $(0=0\wedge 1=0)\vee (1=0\wedge 1=1)$

アプリケーション

最も弱い前提条件の計算は、主に定理証明器 ( SMT ソルバーや証明アシスタントなど)を使用してプログラム内のアサーションを静的にチェックするために使用されます。Frama -CまたはESC/Java2を参照してください。
他の多くの意味論的形式論とは異なり、述語変換意味論は計算の基礎を探求するために設計されたものではありません。むしろ、プログラマーに「計算スタイル」で「構築によって正しい」プログラムを開発するための方法論を提供することを目的としていました。この「トップダウン」スタイルは、ダイクストラ^[6]とN.ヴィルト^[7]によって提唱されました。これは、R.-J.バックらによってリファインメント計算においてさらに形式化されました。現在では、 Bメソッドなどのツールが、この方法論を促進するために自動推論を提供しています。
ホーア論理のメタ理論では、最弱前提条件は相対完全性の証明における重要な概念として現れる。^[8]

述語変換子を超えて

命令形の最も弱い前提条件と最も強い事後条件

述語変換子のセマンティクスでは、式は論理の項に制限されます（上記参照）。しかし、この制限は、式が副作用（副作用を持つ関数の呼び出しなど）を持つ場合や、終了または中止しない場合（ゼロ除算など）がある既存のプログラミング言語の多くにとって強すぎるように思われます。命令型式言語、特にモナド向けに、最弱事前条件または最強事後条件を拡張する提案は数多くあります。

その中で、Hoare型理論はHaskellのような言語のHoare論理、分離論理、型理論を組み合わせたものである。^[9]このシステムは現在、Ynotと呼ばれるRocqライブラリとして実装されている。^[10]この言語では、式の評価は最も強い事後条件の計算に対応する。

確率的述語変換

確率的述語変換器は、確率プログラムのための述語変換器の拡張です。実際、このようなプログラムは、暗号（ランダムノイズを用いた情報の隠蔽）や分散システム（対称性の破れ）など、多くの応用があります。 ^[11]

参照

公理的意味論- 述語変換子意味論を含む
動的論理- 述語変換子が様相として現れる
プログラミング言語の形式意味論— 概要

注記

^ Chen, Wei および Udding, Jan Tijmen, 「The Specific Statement Refined」WUCS-89-37 (1989). https://openscholarship.wustl.edu/cse_research/749
^ Chen, Wei、「ジャンプステートメントのwp特性評価」、2021年国際ソフトウェアエンジニアリング理論的側面シンポジウム（TASE）、2021年、pp. 15-22。doi：10.1109/TASE52547.2021.00019。
^ ランポート、レスリー（1990年7月）「win and sin：並行処理のための述語変換」ACM Trans. Program. Lang. Syst. 12 (3): 396– 428. CiteSeerX 10.1.1.33.90 . doi :10.1145/78969.78970. S2CID 209901.
^ バック、ラルフ・ヨハン、ライト、ヨアキム (2012) [1978]. 精密計算：体系的入門. コンピュータサイエンステキスト. シュプリンガー. ISBN 978-1-4612-1674-2。
^ 陳偉、「出口ステートメントは実行可能な奇跡である」WUCS-91-53 (1991). https://openscholarship.wustl.edu/cse_research/671
^ ダイクストラ, エドガー・W. (1968). 「プログラムの正しさの問題に対する構成的アプローチ」. BIT数値数学. 8 (3): 174– 186. doi :10.1007/bf01933419. S2CID 62224342.
^ Wirth, N. (1971年4月). 「段階的改良によるプログラム開発」(PDF) . Comm. ACM . 14 (4): 221–7 . doi :10.1145/362575.362577. hdl : 20.500.11850/80846 . S2CID 13214445.
^ Hoare 論理に関するチュートリアル: Coqライブラリ。Hoare 論理が操作的意味論に関して健全かつ完全であることをシンプルかつ正式に証明します。
^ Nanevski, Aleksandar; Morrisett, Greg; Birkedal, Lars (2008年9月). 「Hoare型理論、多態性、そして分離」(PDF) . Journal of Functional Programming . 18 ( 5–6 ): 865–911 . doi :10.1017/S0956796808006953. S2CID 6956622.
^ Hoare 型理論を実装したCoqライブラリではありません。
^ Morgan, Carroll; McIver, Annabelle ; Seidel, Karen (1996年5月). 「確率的述語変換」(PDF) . ACM Trans. Program. Lang. Syst . 18 (3): 325– 353. CiteSeerX 10.1.1.41.9219 . doi :10.1145/229542.229547. S2CID 5812195.

参考文献

de Bakker, JW (1980).プログラム正しさの数学的理論. Prentice-Hall. ISBN 978-0-13-562132-5。
Bonsangue, Marcello M.; Kok, Joost N. (1994年11月). 「最弱前提条件計算：再帰と双対性」. Formal Aspects of Computing . 6 (6): 788– 800. CiteSeerX 10.1.1.27.8491 . doi :10.1007/BF01213603. S2CID 40323488.
ダイクストラ, エドガー W. (1975年8月). 「ガード付きコマンド、非決定性、そしてプログラムの形式的導出」. Comm. ACM . 18 (8): 453–7 . doi : 10.1145/360933.360975 . S2CID 1679242.
ダイクストラ、エドガー・W. (1976). 『プログラミングの規律』プレンティス・ホール. ISBN 978-0-613-92411-5。— 多くの実例を交えたガードコマンド言語のバージョンの体系的な紹介
ダイクストラ、エドガー・W.ショルテン、カレル S. (1990)。述語計算とプログラムのセマンティクス。コンピューターサイエンスのテキストとモノグラフ。スプリンガー・フェルラーク。ISBN 978-0-387-96957-2。— より抽象的、形式的、そして決定的な扱い
デヴィッド・グリーズ（1981年）。プログラミングの科学。スプリンガー・フェルラーク。ISBN 978-0-387-96480-5。

[1] Chen, Wei および Udding, Jan Tijmen, 「The Specific Statement Refined」WUCS-89-37 (1989). https://openscholarship.wustl.edu/cse_research/749

[2] Chen, Wei、「ジャンプステートメントのwp特性評価」、2021年国際ソフトウェアエンジニアリング理論的側面シンポジウム（TASE）、2021年、pp. 15-22。doi：10.1109/TASE52547.2021.00019。

[3] ランポート、レスリー（1990年7月）「win and sin：並行処理のための述語変換」ACM Trans. Program. Lang. Syst. 12 (3): 396– 428. CiteSeerX 10.1.1.33.90 . doi :10.1145/78969.78970. S2CID 209901.

[4] バック、ラルフ・ヨハン、ライト、ヨアキム (2012) [1978]. 精密計算：体系的入門. コンピュータサイエンステキスト. シュプリンガー. ISBN 978-1-4612-1674-2。

[5] 陳偉、「出口ステートメントは実行可能な奇跡である」WUCS-91-53 (1991). https://openscholarship.wustl.edu/cse_research/671

[6] ダイクストラ, エドガー・W. (1968). 「プログラムの正しさの問題に対する構成的アプローチ」. BIT数値数学. 8 (3): 174– 186. doi :10.1007/bf01933419. S2CID 62224342.

[7] Wirth, N. (1971年4月). 「段階的改良によるプログラム開発」(PDF) . Comm. ACM . 14 (4): 221–7 . doi :10.1145/362575.362577. hdl : 20.500.11850/80846 . S2CID 13214445.

[8] Hoare 論理に関するチュートリアル: Coqライブラリ。Hoare 論理が操作的意味論に関して健全かつ完全であることをシンプルかつ正式に証明します。

[9] Nanevski, Aleksandar; Morrisett, Greg; Birkedal, Lars (2008年9月). 「Hoare型理論、多態性、そして分離」(PDF) . Journal of Functional Programming . 18 ( 5–6 ): 865–911 . doi :10.1017/S0956796808006953. S2CID 6956622.

[10] Hoare 型理論を実装したCoqライブラリではありません。

[11] Morgan, Carroll; McIver, Annabelle ; Seidel, Karen (1996年5月). 「確率的述語変換」(PDF) . ACM Trans. Program. Lang. Syst . 18 (3): 325– 353. CiteSeerX 10.1.1.41.9219 . doi :10.1145/229542.229547. S2CID 5812195.

v t e エドガー・ダイクストラ
作品	ALGOL 60 プログラミング入門（書籍）構造化プログラミング（書籍）プログラミングの規律（書籍）プログラミングの方法（書籍）述語計算とプログラム意味論（書籍）コンピューティングに関する選集：個人的な視点（書籍）グラフに関する2つの問題について協調する連続プロセス並行プログラミング制御における問題の解決「THE」マルチプログラミングシステムの構造 Go Toステートメントは有害であると考えられる構造化プログラミングに関するメモ謙虚なプログラマープログラミングを人間の活動として考える傷つけるかもしれない真実をどうやって伝えるのか？科学的思考の役割について分散制御にもかかわらず自己安定するシステムコンピュータサイエンスを教えるということの残酷さについて選定された論文 EWD原稿
主な研究分野	理論計算科学ソフトウェアエンジニアリングシステム科学アルゴリズム設計（ダイクストラのアルゴリズム）同時実行コンピューティング分散コンピューティング形式手法プログラミング方法論プログラミング言語の研究プログラムの設計と開発ソフトウェアアーキテクチャコンピュータプログラミングとコンピューティング科学の哲学
関連人物	シュロミ・ドレフペル・ブリンチ・ハンセントニー・ホアオレ・ヨハン・ダールレスリー・ランポートデビッド・パルナスヤープ・A・ゾンネフェルトカレル・S・ショルテンアドリアーン・ファン・ヴィンガルデンニクラウス・ヴィルト
ウィキクォート