情報科学 › ソフトウェア設計とテスト › 契約による設計

Hoare 論理の推論規則

定義 3.7（「契約による設計」§3）

契約表 C\mathcal{C} とは、操作名 m∈Opm \in \mathrm{Op} と表明 P,QP, Q の三つ組 (m,P,Q)(m, P, Q) の集合をいう。解釈 M\mathcal{M} が契約表 C\mathcal{C} を満たすとは、すべての (m,P,Q)∈C(m, P, Q) \in \mathcal{C} について ⊨M{P} call m {Q}\models_{\mathcal{M}} \{P\}\ \mathtt{call}\ m\ \{Q\} が成り立つことをいう。

契約表 C\mathcal{C} のもとでの導出可能性 ⊢C{P} c {Q}\vdash_{\mathcal{C}} \{P\}\ c\ \{Q\} を、次の規則で生成される最小の関係とする。

(H-Skip){P} skip {P}(H-Assign){Q[a/x]} x:=a {Q}(H-Seq){P} c1 {R}{R} c2 {Q}{P} c1;c2 {Q}(H-Call)(m,P,Q)∈C{P} call m {Q}(H-If){P∧b} c1 {Q}{P∧¬b} c2 {Q}{P} if b then c1 else c2 {Q}(H-While){I∧b} c {I}{I} while b do c {I∧¬b}(H-Conseq)P⇒P′{P′} c {Q′}Q′⇒Q{P} c {Q}\begin{aligned} &\text{(H-Skip)} && \{P\}\ \mathtt{skip}\ \{P\} \qquad\qquad \text{(H-Assign)} \quad \{Q[a/x]\}\ x := a\ \{Q\} \\[4pt] &\text{(H-Seq)} && \frac{\{P\}\ c_1\ \{R\} \qquad \{R\}\ c_2\ \{Q\}}{\{P\}\ c_1 ; c_2\ \{Q\}} \qquad\qquad \text{(H-Call)} \quad \frac{(m, P, Q) \in \mathcal{C}}{\{P\}\ \mathtt{call}\ m\ \{Q\}} \\[4pt] &\text{(H-If)} && \frac{\{P \wedge b\}\ c_1\ \{Q\} \qquad \{P \wedge \lnot b\}\ c_2\ \{Q\}}{\{P\}\ \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2\ \{Q\}} \\[4pt] &\text{(H-While)} && \frac{\{I \wedge b\}\ c\ \{I\}}{\{I\}\ \mathtt{while}\ b\ \mathtt{do}\ c\ \{I \wedge \lnot b\}} \\[4pt] &\text{(H-Conseq)} && \frac{P \Rightarrow P' \qquad \{P'\}\ c\ \{Q'\} \qquad Q' \Rightarrow Q}{\{P\}\ c\ \{Q\}} \end{aligned}

(H-While) の表明 II をループ不変条件、(H-Conseq) を帰結の規則という。

本文で読む（前後の説明と例）→

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。

これを使っている定理

証明で明示的に参照している定理は、まだありません。

関連するノック 1 問