契約による設計：事前条件・事後条件・不変条件と Hoare 論理

0. この記事の要点

関数を作る人と使う人のあいだで「何を渡せば、何が返るのか」を前もって決めておくと、誤りがどちらの側にあるのかがはっきりします。この記事は、その取り決め（契約）を数学の言葉で書き、プログラムが約束を守ることを証明する方法を学びます。読み終えると、ループの途中で成り立っていてほしい条件を見つけ、それを使ってプログラムの正しさと停止を示せるようになります。

• モジュールの契約は、呼び出し側が守る事前条件 $P$ と、実装が守る事後条件 $Q$ の組です。「$P$ を満たす状態から実行して止まれば $Q$ が成り立つ」という主張を Hoare の三つ組 $\{P\}\ c\ \{Q\}$ と書きます。
• 代入・逐次・条件分岐・while・帰結の 5 つの規則（と操作の呼び出しの規則）で導出した三つ組は、実行の意味論に照らして正しい（健全性）。while の規則が要求するのは、反復で保たれるループ不変条件です。
• 不変条件は「止まれば正しい」ことしか保証しません。自然数に値をとり反復ごとに真に減る変量があれば、ループは止まります。根拠は自然数の整列性です。
• クラスの表現不変条件は、構築子が成立させ、すべての公開操作が保ち、表現が外に漏れなければ、到達できるすべての状態で成り立ちます。表現を別名で渡すと、この帰納法の仮定が破れます。
• 下位型の実装が、事前条件を弱め（$P \Rightarrow P'$）事後条件を強める（$Q' \Rightarrow Q$）なら、上位型の契約だけで証明した呼び出し側は差し替えても正しいままです（Liskov の置換原則）。逆向きの変更は呼び出し側を壊します。
• 表明の実行時検査は、与えた入力での違反しか検出しません。すべての入力について契約が成り立つかの判定は、一般に決定不能です。テストは契約の有限個の点での検査、証明はすべての点での検査です。

この記事で使う事前知識

• 二分探索: 昇順に並んだ列の真ん中を調べ、探索範囲を半分に絞っていく方法。→ 探索アルゴリズム
• 下限位置: 昇順の列で、$x$ 以上の値が最初に現れる位置のこと。→ 下限位置
• 配列: 同じ種類の値を番号（添字）つきで並べたもの。→ 配列
• プログラミング言語の意味: プログラムの実行を、規則に従った書き換えとして数学的に定める考え方。→ プログラミング言語論
• 数学的帰納法: 最初の場合と「ひとつ前が成り立てば次も成り立つ」ことから、すべての場合を示す証明法。
• 命題論理: 「かつ」「または」「ならば」で条件を組み合わせて真偽を考える枠組み。

1. 動機

二分探索は 20 行に満たないアルゴリズムですが、探索アルゴリズム で見たとおり、正しい実装が公刊されるまでに長い年月がかかり、広く使われた標準ライブラリの中でも壊れていました。壊れていたのは算法の着想ではなく、「この関数は何を受け取り、何を返すと約束しているのか」「ループの途中で何が成り立っているのか」という、コードに書かれていない部分です。

プログラムの誤りを論じるには、まず「正しい」を定めなければなりません。関数 lower_bound(a, x) が正しいかどうかは、a が昇順であるという前提を置くかどうかで変わります。昇順でない配列を渡して変な値が返ってきたとき、誤っているのは関数ではなく呼び出し側です。逆に、昇順の配列を渡して下限位置でない値が返ってきたら、誤っているのは関数です。責任の境界を決めるのが契約です。B. Meyer はこの考え方を「契約による設計」（Design by Contract）と名づけ、事前条件を呼び出し側の義務、事後条件を実装側の義務として、クラスのインターフェースに書き込むことを提案しました。

契約を書くだけなら注釈にすぎません。この記事の主題は、契約から何が証明できるかです。C. A. R. Hoare は 1969 年の論文で、プログラムの各構文に対応する推論規則を与え、契約をプログラムの構造に沿って機械的に導出できることを示しました。この体系（Hoare 論理）の規則が正しいこと、つまり導出した契約が実際の実行で必ず守られることを、この記事では実行の意味論から証明します。そのうえで、同じ考え方をクラスの不変条件と、下位クラスへの差し替えに広げます。

この章は、テーマ「ソフトウェア設計とテスト」の出発点です。次章以降のテストは、いつも「何かに対する」テストです。その「何か」がこの章の契約で、テストは契約を有限個の入力で検査し、証明はすべての入力で検査します。両者の違いは最後の節で命題の形にします。

2. 仕様・実装・契約

定義 2.1（仕様・実装・インターフェース）↗

入力の集合 $X$ と出力の集合 $Y$ を固定する。

• 仕様とは、関係 $S \subseteq X \times Y$ と部分集合 $D \subseteq X$（仕様が何かを約束する入力の範囲）の組 $(D, S)$ をいう。$(x, y) \in S$ は「入力 $x$ に対して出力 $y$ は許される」ことを表す。
• 実装とは、$X$ から $Y$ への部分関数 $f$（止まらない入力では値が定まらない）をいう。
• 実装 $f$ が仕様 $(D, S)$ を満たすとは、すべての $x \in D$ について $f(x)$ が定まり、$(x, f(x)) \in S$ であることをいう。

モジュール（関数・クラス・パッケージ）が外に見せる操作の名前と、その仕様の集まりをインターフェースという。インターフェースに現れない実装の詳細（データの持ち方、補助関数）を外から使えないようにすることを情報隠蔽という。

仕様が関係であって関数でないのは、許される出力が 1 つとは限らないからです。「配列の中の $x$ の位置を 1 つ返す」という仕様は、$x$ が複数あればどれを返してもよいとしています。$D$ の外の入力について、仕様は何も約束しません。実装は何を返しても、止まらなくても、仕様に違反しません。

情報隠蔽は、D. Parnas が 1972 年に、モジュール分割の基準として提案した考え方です。隠す理由は秘密にしたいからではなく、隠したものは後から変えられるからです。呼び出し側がインターフェースの仕様だけを使って書かれていれば、実装を別のもの（同じ仕様を満たすもの）に取り替えても呼び出し側は正しいままです。この「取り替えても正しい」を定理にしたものが、第 7 節の 定理 7.2 です。

定義 2.2（契約：事前条件と事後条件）↗

状態（変数の値の割り当て）の集合を $\Sigma$ とする。$\Sigma$ の部分集合を表明という。表明 $P$ と状態 $\sigma$ について、$\sigma \in P$ を $P(\sigma)$ とも書き、「$\sigma$ で $P$ が成り立つ」と読む。

操作 $m$ の契約とは、表明の組 $(P, Q)$ をいう。$P$ を事前条件、$Q$ を事後条件という。契約 $(P, Q)$ は次の約束を表す。

• 呼び出し側の義務: $P$ が成り立つ状態でだけ $m$ を呼ぶ。
• 実装側の義務: $P$ が成り立つ状態から実行を始めて止まったなら、止まった状態で $Q$ が成り立つ。

表明 $P, P'$ について、$P \subseteq P'$ のとき $P \Rightarrow P'$ と書き、$P$ は $P'$ より強い、$P'$ は $P$ より弱いという。$P \wedge P' = P \cap P'$、$P \vee P' = P \cup P'$、$\lnot P = \Sigma \setminus P$、$\mathrm{true} = \Sigma$、$\mathrm{false} = \emptyset$ と書く。

表明を論理式ではなく状態の集合として定めたのは、論理式の言語を固定する手間を省くためです。「$x \ge 0$」と書いたら、それは $\{\sigma \mid \sigma(x) \ge 0\}$ という集合のことです。強い・弱いの向きに注意してください。強い条件ほど、満たす状態が少ない。事前条件が弱いほど実装は多くの入力を引き受け、事後条件が強いほど実装は多くを約束します。$\mathrm{false}$ はもっとも強く、$\mathrm{true}$ はもっとも弱い表明です。

小さな例で確かめます。命令「$x$ に 1 を足す」を、$x \ge 0$ の状態から実行すると、終わった状態では $x \ge 1$ です。事前条件を $x \ge 0$、事後条件を $x \ge 1$ とする契約が、この命令について成り立ちます。また「$x \ge 5$」を満たす状態は必ず「$x \ge 0$」も満たすので、$x \ge 5$ は $x \ge 0$ より強い条件です。

強い条件ほど、満たす状態の集合は小さい。P は P' より強く、P ならば P' が成り立つ。

事後条件が「実行前の値」に触れたいことがあります（「幅を変えても高さは変わらない」）。この記事では、実行前の値を表す定数 $h_0$ ごとに契約 $(P \wedge h = h_0,\ Q \wedge h = h_0)$ を 1 つずつ用意し、契約の族として表します。定義 3.7 の契約表が三つ組の集合になっているのは、そのためです。

3. 言語 W と Hoare 論理

3.1. 構文と大ステップ意味論

契約が「守られる」とはどういうことかを定めるには、プログラムの実行を数学的に定めなければなりません。プログラミング言語論 の言語 L（定義 4.1［プログラミング言語論］）は、式を 1 ステップずつ書き換える簡約関係で意味を定めました。ここでは変数への代入とループをもつ命令型の言語 W を用意し、「命令 $c$ を状態 $\sigma$ から実行すると状態 $\sigma'$ で止まる」という関係を直接定めます（大ステップ意味論）。

次の定義は長く見えますが、やっていることは「Python のような小さな言語の、各構文が何をするか」を一覧にするだけです。横線の書き方は「線の上が成り立てば、線の下も成り立つ」と読みます。たとえば「$x := x + 1$ を、$x = 3$ の状態から実行すると、$x = 4$ の状態で終わる」ことが、この関係の最も簡単な例です。まず規則の表は流し読みし、第 3.2 節以降で必要になったときに戻ってください。

定義 3.1（言語 W）↗

$\mathrm{Var}$ を変数の集合、$\mathrm{Op}$ を操作名の有限集合とする。状態とは写像 $\sigma : \mathrm{Var} \to \mathbb{Z}$ をいい、状態の全体を $\Sigma$ と書く。$\sigma[x \mapsto n]$ は、$x$ の値を $n$ に変え、ほかの変数の値を $\sigma$ と同じにした状態を表す。

算術式 $a$、ブール式 $b$、命令 $c$ を次の文法で定める（$n \in \mathbb{Z}$、$x \in \mathrm{Var}$、$k$ は正の整数、$m \in \mathrm{Op}$）。

$$\begin{aligned} a &::= n \mid x \mid a_1 + a_2 \mid a_1 - a_2 \mid a_1 \times a_2 \mid a_1 \div k \\ b &::= \mathtt{true} \mid a_1 = a_2 \mid a_1 \le a_2 \mid \lnot b \mid b_1 \wedge b_2 \\ c &::= \mathtt{skip} \mid x := a \mid c_1 ; c_2 \mid \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2 \mid \mathtt{while}\ b\ \mathtt{do}\ c \mid \mathtt{call}\ m \end{aligned}$$

式の値 $\llbracket a \rrbracket\sigma \in \mathbb{Z}$、$\llbracket b \rrbracket\sigma \in \{\mathrm{tt}, \mathrm{ff}\}$ を、式の構造についての再帰で定める。$\llbracket n \rrbracket\sigma = n$、$\llbracket x \rrbracket\sigma = \sigma(x)$、$\llbracket a_1 + a_2 \rrbracket\sigma = \llbracket a_1 \rrbracket\sigma + \llbracket a_2 \rrbracket\sigma$（$-$、$\times$ も同様）、$\llbracket a_1 \div k \rrbracket\sigma = \lfloor \llbracket a_1 \rrbracket\sigma / k \rfloor$。$\llbracket \mathtt{true} \rrbracket\sigma = \mathrm{tt}$、$\llbracket a_1 = a_2 \rrbracket\sigma = \mathrm{tt}$ となるのは $\llbracket a_1 \rrbracket\sigma = \llbracket a_2 \rrbracket\sigma$ のとき（$\le$ も同様）、$\lnot$ と $\wedge$ は真理値の否定と連言。ブール式 $b$ を表明 $\{\sigma \mid \llbracket b \rrbracket\sigma = \mathrm{tt}\}$ と同一視する。$a_1 \lt a_2$ は $\lnot(a_2 \le a_1)$ の略記とする。

解釈 $\mathcal{M}$ とは、各操作名 $m \in \mathrm{Op}$ に関係 $\mathcal{M}(m) \subseteq \Sigma \times \Sigma$ を割り当てるものをいう。解釈 $\mathcal{M}$ のもとでの実行関係 $\langle c, \sigma \rangle \Downarrow \sigma'$ を、次の規則で生成される最小の関係とする。

$$\begin{aligned} &\text{(Skip)} && \langle \mathtt{skip}, \sigma \rangle \Downarrow \sigma \qquad\qquad \text{(Assign)} \quad \langle x := a, \sigma \rangle \Downarrow \sigma[x \mapsto \llbracket a \rrbracket\sigma] \\[4pt] &\text{(Seq)} && \frac{\langle c_1, \sigma \rangle \Downarrow \sigma_1 \qquad \langle c_2, \sigma_1 \rangle \Downarrow \sigma'}{\langle c_1 ; c_2, \sigma \rangle \Downarrow \sigma'} \qquad\qquad \text{(Call)} \quad \frac{(\sigma, \sigma') \in \mathcal{M}(m)}{\langle \mathtt{call}\ m, \sigma \rangle \Downarrow \sigma'} \\[4pt] &\text{(IfT)} && \frac{\llbracket b \rrbracket\sigma = \mathrm{tt} \qquad \langle c_1, \sigma \rangle \Downarrow \sigma'}{\langle \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, \sigma \rangle \Downarrow \sigma'} \qquad \text{(IfF)} \quad \frac{\llbracket b \rrbracket\sigma = \mathrm{ff} \qquad \langle c_2, \sigma \rangle \Downarrow \sigma'}{\langle \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, \sigma \rangle \Downarrow \sigma'} \\[4pt] &\text{(WhF)} && \frac{\llbracket b \rrbracket\sigma = \mathrm{ff}}{\langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma \rangle \Downarrow \sigma} \qquad\qquad \text{(WhT)} \quad \frac{\llbracket b \rrbracket\sigma = \mathrm{tt} \qquad \langle c, \sigma \rangle \Downarrow \sigma_1 \qquad \langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma_1 \rangle \Downarrow \sigma'}{\langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma \rangle \Downarrow \sigma'} \end{aligned}$$

$\langle c, \sigma \rangle \Downarrow \sigma'$ となる $\sigma'$ が存在するとき、$c$ は $\sigma$ から停止するという。

「規則で生成される最小の関係」とは、規則を有限回使って組み立てた導出（有限の木）があるものだけが関係に属する、ということです。導出の高さは自然数なので、「導出についての帰納法」は高さについての完全帰納法（定理 4.3［証明の技術］）として正当化されます。$\mathtt{while}\ \mathtt{true}\ \mathtt{do}\ \mathtt{skip}$ にはどの状態からも有限の導出がありません。(WhT) を使うたびに同じ命令の導出がもう 1 つ必要になるからです。止まらない実行は、この意味論では「$\Downarrow$ が成り立つ $\sigma'$ が無い」として表されます。

式の値は、状態の全域関数として定めました（ゼロ除算を避けるため、割り算は正の定数による切り捨て除算だけにしています）。以下の証明が式について使うのは、この「状態が決まれば値が決まる」ことだけです。$\mathtt{call}\ m$ は、中身を書かない操作の呼び出しです。中身の代わりに解釈 $\mathcal{M}$ が状態の変化を与えます。第 7 節で、$\mathcal{M}$ を取り替えることが「実装の差し替え」になります。

補題 3.2（実行の決定性）✓

解釈 $\mathcal{M}$ がすべての $m \in \mathrm{Op}$ について部分関数である（$(\sigma, \sigma_1), (\sigma, \sigma_2) \in \mathcal{M}(m)$ ならば $\sigma_1 = \sigma_2$）とする。このとき、$\langle c, \sigma \rangle \Downarrow \sigma'$ かつ $\langle c, \sigma \rangle \Downarrow \sigma''$ ならば $\sigma' = \sigma''$ である。

証明（補題 3.2）

言語 L の決定性（定理 4.4［プログラミング言語論］）と同じ方針で、$\langle c, \sigma \rangle \Downarrow \sigma'$ の導出の高さについての完全帰納法（定理 4.3［証明の技術］）で示します。導出の最後の規則で場合を分けます。

(Skip)。$c = \mathtt{skip}$ で、$\mathtt{skip}$ を結論にもつ規則は (Skip) だけなので、$\sigma' = \sigma = \sigma''$ です。

(Assign)。$c$ は $x := a$ で、この形を結論にもつ規則は (Assign) だけです。$\llbracket a \rrbracket\sigma$ は $\sigma$ から 1 つに決まるので、$\sigma' = \sigma[x \mapsto \llbracket a \rrbracket\sigma] = \sigma''$ です。

(Call)。$c = \mathtt{call}\ m$ で、適用できる規則は (Call) だけです。$(\sigma, \sigma'), (\sigma, \sigma'') \in \mathcal{M}(m)$ なので、$\mathcal{M}(m)$ が部分関数であるという仮定から $\sigma' = \sigma''$ です。

(Seq)。$c = c_1; c_2$ で、前提は $\langle c_1, \sigma \rangle \Downarrow \sigma_1$ と $\langle c_2, \sigma_1 \rangle \Downarrow \sigma'$ です。もう一方の導出も (Seq) で終わり、前提は $\langle c_1, \sigma \rangle \Downarrow \sigma_1'$ と $\langle c_2, \sigma_1' \rangle \Downarrow \sigma''$ です。$\langle c_1, \sigma \rangle \Downarrow \sigma_1$ の導出は元の導出より低いので、帰納法の仮定から $\sigma_1 = \sigma_1'$。すると $\langle c_2, \sigma_1 \rangle \Downarrow \sigma'$ と $\langle c_2, \sigma_1 \rangle \Downarrow \sigma''$ にもう一度帰納法の仮定を使えて、$\sigma' = \sigma''$ です。

(IfT)。$\llbracket b \rrbracket\sigma = \mathrm{tt}$ なので、もう一方の導出の最後の規則は (IfF) ではありえず（(IfF) は $\llbracket b \rrbracket\sigma = \mathrm{ff}$ を要求します）、(IfT) です。どちらの前提も $c_1$ を $\sigma$ から実行したもので、帰納法の仮定から $\sigma' = \sigma''$ です。(IfF) も同じです。

(WhF)。$\llbracket b \rrbracket\sigma = \mathrm{ff}$ なので、もう一方の導出も (WhF) で終わり、$\sigma' = \sigma = \sigma''$ です。

(WhT)。$\llbracket b \rrbracket\sigma = \mathrm{tt}$ なので、もう一方も (WhT) で終わります。前提は $\langle c, \sigma \rangle \Downarrow \sigma_1$、$\langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma_1 \rangle \Downarrow \sigma'$ と、$\langle c, \sigma \rangle \Downarrow \sigma_1'$、$\langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma_1' \rangle \Downarrow \sigma''$ です。帰納法の仮定を本体の実行に使って $\sigma_1 = \sigma_1'$、続いて残りのループの実行（これも元の導出より低い）に使って $\sigma' = \sigma''$ です。

∎

3.2. 三つ組と置換

定義 3.3（Hoare の三つ組：部分正当性と全正当性）↗

$P, Q$ を表明、$c$ を言語 W の命令、$\mathcal{M}$ を解釈とする。

• 三つ組 $\{P\}\ c\ \{Q\}$ が $\mathcal{M}$ のもとで部分正当であるとは、すべての状態 $\sigma, \sigma'$ について「$P(\sigma)$ かつ $\langle c, \sigma \rangle \Downarrow \sigma'$ ならば $Q(\sigma')$」が成り立つことをいう。このとき $\models_{\mathcal{M}} \{P\}\ c\ \{Q\}$ と書く。
• 三つ組 $[P]\ c\ [Q]$ が $\mathcal{M}$ のもとで全正当であるとは、すべての状態 $\sigma$ について「$P(\sigma)$ ならば、$\langle c, \sigma \rangle \Downarrow \sigma'$ かつ $Q(\sigma')$ を満たす $\sigma'$ が存在する」が成り立つことをいう。このとき $\models_{\mathcal{M}} [P]\ c\ [Q]$ と書く。

部分正当性は「止まれば正しい」、全正当性は「止まって、しかも正しい」です。止まらないプログラムは、どんな事後条件についても部分正当です。たとえば $\models \{\mathrm{true}\}\ \mathtt{while}\ \mathtt{true}\ \mathtt{do}\ \mathtt{skip}\ \{\mathrm{false}\}$ が成り立ちます。前提「$\langle c, \sigma \rangle \Downarrow \sigma'$」を満たす $\sigma'$ が無いからです。部分正当性だけでは弱すぎるように見えますが、正しさと停止性を分けて証明できることが利点で、停止性は第 5 節で別に扱います。

代入の規則を述べるには、表明の中の変数を式で置き換える操作が要ります。

定義 3.4（表明への代入）↗

表明 $Q$、変数 $x$、算術式 $a$ に対して、表明 $Q[a/x]$ を

$$Q[a/x] = \{\, \sigma \in \Sigma \mid Q(\sigma[x \mapsto \llbracket a \rrbracket\sigma]) \,\}$$

で定める。また、算術式 $a'$ とブール式 $b$ の中の変数 $x$ をすべて $a$ に書き換えた式を $a'[a/x]$、$b[a/x]$ と書く。

$Q[a/x]$ は「$x$ に $a$ の値を入れたあとで $Q$ が成り立つような、入れる前の状態」の集合です。$Q$ が式で書かれているとき、この集合は文字どおりの書き換えで得られます。それが次の補題です。この補題は、代入の規則（次の命題）を実際の式の書き換えで計算できるようにするための準備です。証明は、式の作りに沿って場合を分けるだけの確認作業です。

補題 3.5（置換補題）✓

算術式 $a, a'$、ブール式 $b$、変数 $x$、状態 $\sigma$ について

$$\llbracket a'[a/x] \rrbracket\sigma = \llbracket a' \rrbracket\bigl(\sigma[x \mapsto \llbracket a \rrbracket\sigma]\bigr), \qquad \llbracket b[a/x] \rrbracket\sigma = \llbracket b \rrbracket\bigl(\sigma[x \mapsto \llbracket a \rrbracket\sigma]\bigr)$$

が成り立つ。とくに、ブール式 $b$ を表明とみたとき、式の書き換え $b[a/x]$ が表す表明は 定義 3.4 の $b[a/x]$ と一致する。

証明（補題 3.5）

$\tau = \sigma[x \mapsto \llbracket a \rrbracket\sigma]$ とおきます。まず算術式 $a'$ の構造についての帰納法で第 1 式を示します。

$a' = n$（定数）のとき、$a'[a/x] = n$ で、両辺とも $n$ です。$a' = x$ のとき、$a'[a/x] = a$ なので左辺は $\llbracket a \rrbracket\sigma$、右辺は $\tau(x) = \llbracket a \rrbracket\sigma$ です。$a' = y$（$x$ と異なる変数）のとき、$a'[a/x] = y$ なので左辺は $\sigma(y)$、右辺は $\tau(y) = \sigma(y)$ です（$\tau$ は $x$ 以外で $\sigma$ と同じ）。$a' = a_1 + a_2$ のとき、書き換えは部分式ごとに行うので $a'[a/x] = a_1[a/x] + a_2[a/x]$ で、

$$\llbracket a'[a/x] \rrbracket\sigma = \llbracket a_1[a/x] \rrbracket\sigma + \llbracket a_2[a/x] \rrbracket\sigma = \llbracket a_1 \rrbracket\tau + \llbracket a_2 \rrbracket\tau = \llbracket a_1 + a_2 \rrbracket\tau$$

です（2 つ目の等号が帰納法の仮定）。$-$、$\times$、$\div k$ も、値の定義が部分式の値の関数なので同じです。

ブール式についても構造についての帰納法で示します。$b = \mathtt{true}$ は両辺 $\mathrm{tt}$。$b = (a_1 = a_2)$ のとき、$\llbracket b[a/x] \rrbracket\sigma = \mathrm{tt}$ は $\llbracket a_1[a/x] \rrbracket\sigma = \llbracket a_2[a/x] \rrbracket\sigma$ と同値で、いま示した第 1 式によりこれは $\llbracket a_1 \rrbracket\tau = \llbracket a_2 \rrbracket\tau$、すなわち $\llbracket b \rrbracket\tau = \mathrm{tt}$ と同値です。$\le$ も同じです。$\lnot b_1$ と $b_1 \wedge b_2$ は、値が部分式の値の関数なので帰納法の仮定から従います。

最後の主張は、$\{\sigma \mid \llbracket b[a/x] \rrbracket\sigma = \mathrm{tt}\} = \{\sigma \mid \llbracket b \rrbracket(\sigma[x \mapsto \llbracket a \rrbracket\sigma]) = \mathrm{tt}\}$ であり、右辺は 定義 3.4 の定義そのものです。

∎

命題 3.6（代入の規則は後ろ向きである）✓

$x$ を変数、$a$ を算術式、$P, Q$ を表明とする。解釈は任意でよい。

1. $\models \{Q[a/x]\}\ x := a\ \{Q\}$ が成り立つ。
2. $\models \{P\}\ x := a\ \{Q\}$ ならば $P \Rightarrow Q[a/x]$ である。すなわち $Q[a/x]$ は、事後条件 $Q$ を保証する事前条件のうちでもっとも弱い。
3. 「前向き」に書いた規則 $\{P\}\ x := a\ \{P \wedge x = a\}$ は正しくない。$P$ を $x = 0$、$a$ を $x + 1$ とすると、三つ組 $\{x = 0\}\ x := x + 1\ \{x = 0 \wedge x = x + 1\}$ は部分正当でない。

証明（命題 3.6）

(1) $Q[a/x](\sigma)$ かつ $\langle x := a, \sigma \rangle \Downarrow \sigma'$ とします。代入を結論にもつ規則は (Assign) だけなので $\sigma' = \sigma[x \mapsto \llbracket a \rrbracket\sigma]$ です。定義 3.4 より、$Q[a/x](\sigma)$ は $Q(\sigma[x \mapsto \llbracket a \rrbracket\sigma])$、つまり $Q(\sigma')$ のことです。

(2) $P(\sigma)$ とします。(Assign) により $\sigma' = \sigma[x \mapsto \llbracket a \rrbracket\sigma]$ について $\langle x := a, \sigma \rangle \Downarrow \sigma'$ が成り立つので、仮定 $\models \{P\}\ x := a\ \{Q\}$ から $Q(\sigma')$ です。これは $Q[a/x](\sigma)$ の定義です。

(3) $\sigma(x) = 0$ である状態 $\sigma$ をとります。$P(\sigma)$ は成り立ち、$\langle x := x + 1, \sigma \rangle \Downarrow \sigma'$、$\sigma' = \sigma[x \mapsto 1]$ です。事後条件 $x = 0 \wedge x = x + 1$ は、$\sigma'(x) = \sigma'(x) + 1$ を満たす状態が無いので空集合（$\mathrm{false}$）です。$\sigma'$ はこれに属しません。

∎

(3) の規則が壊れるのは、事後条件の中の $x$ が代入後の値を指すのに、$P$ と $a$ の中の $x$ は代入前の値を指しているからです。$x$ が $P$ にも $a$ にも現れなければ、前向きの規則は正しくなります。後ろ向きの規則は、(1) の証明が 1 行で済んだとおり、意味論の (Assign) をそのまま写しています。事後条件 $Q$ の中の $x$ を「これから入る値」$a$ に置き換えれば、それが代入前に成り立つべき条件です。たとえば $\{x + 1 \le 10\}\ x := x + 1\ \{x \le 10\}$ で、事前条件は $x \le 9$ です。

3.3. 推論規則と健全性

定義 3.7（Hoare 論理の推論規則）↗

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

契約表 $\mathcal{C}$ のもとでの導出可能性 $\vdash_{\mathcal{C}} \{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) の表明 $I$ をループ不変条件、(H-Conseq) を帰結の規則という。

規則は命令の構文 1 つにつき 1 つあり、(H-Conseq) だけが構文によらない規則です。(H-Conseq) は「事前条件は強めてよく、事後条件は弱めてよい」と読めます。この規則が帰結の規則と呼ばれるのは、すでに導いた三つ組から、条件を弱めたり強めたりした別の三つ組を結論できるからです。(H-While) は、ループ本体が「$I$ と条件 $b$ が成り立つ状態から、$I$ が成り立つ状態へ」移ることだけを要求し、反復の回数には触れません。ループを抜けたときに言えるのは、$I$ と、抜けた理由である $\lnot b$ です。

定理 3.8（Hoare 論理の健全性）✓

$\mathcal{C}$ を契約表、$\mathcal{M}$ を $\mathcal{C}$ を満たす解釈とする。$\vdash_{\mathcal{C}} \{P\}\ c\ \{Q\}$ ならば $\models_{\mathcal{M}} \{P\}\ c\ \{Q\}$ である。

証明の方針を先に述べます。規則の数だけ場合分けをし、ほとんどは意味論の規則をそのまま写すだけで済みます。手間がかかるのは while だけで、ここでは帰納法を二重に使います。論理の導出についての帰納法が本体の事実を 1 つ与え、実行の導出についての帰納法が、それを反復の回数だけ繰り返し使います。

証明（定理 3.8）

$\vdash_{\mathcal{C}} \{P\}\ c\ \{Q\}$ の導出の高さについての完全帰納法（定理 4.3［証明の技術］）で示します。導出の最後の規則で場合を分けます。以下、$\models$ は $\models_{\mathcal{M}}$ の意味です。

(H-Skip)。$P(\sigma)$ かつ $\langle \mathtt{skip}, \sigma \rangle \Downarrow \sigma'$ とします。適用できる規則は (Skip) だけなので $\sigma' = \sigma$、よって $P(\sigma')$ です。

(H-Assign)。命題 3.6 (1) です。

(H-Call)。$(m, P, Q) \in \mathcal{C}$ で、$\mathcal{M}$ は $\mathcal{C}$ を満たすので、定義から $\models \{P\}\ \mathtt{call}\ m\ \{Q\}$ です。

(H-Seq)。帰納法の仮定から $\models \{P\}\ c_1\ \{R\}$ と $\models \{R\}\ c_2\ \{Q\}$ です。$P(\sigma)$ かつ $\langle c_1; c_2, \sigma \rangle \Downarrow \sigma'$ とします。この実行の導出は (Seq) で終わるので、$\langle c_1, \sigma \rangle \Downarrow \sigma_1$ かつ $\langle c_2, \sigma_1 \rangle \Downarrow \sigma'$ となる $\sigma_1$ があります。1 つ目の仮定から $R(\sigma_1)$、2 つ目の仮定から $Q(\sigma')$ です。

(H-If)。帰納法の仮定から $\models \{P \wedge b\}\ c_1\ \{Q\}$ と $\models \{P \wedge \lnot b\}\ c_2\ \{Q\}$ です。$P(\sigma)$ かつ $\langle \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, \sigma \rangle \Downarrow \sigma'$ とします。実行の導出が (IfT) で終わるなら、$\llbracket b \rrbracket\sigma = \mathrm{tt}$ かつ $\langle c_1, \sigma \rangle \Downarrow \sigma'$ で、$(P \wedge b)(\sigma)$ なので 1 つ目の仮定から $Q(\sigma')$ です。(IfF) で終わるなら、$\llbracket b \rrbracket\sigma = \mathrm{ff}$ かつ $\langle c_2, \sigma \rangle \Downarrow \sigma'$ で、$(P \wedge \lnot b)(\sigma)$ なので 2 つ目の仮定から $Q(\sigma')$ です。

(H-Conseq)。帰納法の仮定から $\models \{P'\}\ c\ \{Q'\}$ です。$P(\sigma)$ かつ $\langle c, \sigma \rangle \Downarrow \sigma'$ とします。$P \Rightarrow P'$ より $P'(\sigma)$、仮定より $Q'(\sigma')$、$Q' \Rightarrow Q$ より $Q(\sigma')$ です。

(H-While)。$w = \mathtt{while}\ b\ \mathtt{do}\ c$ とおきます。外側の帰納法の仮定から $\models \{I \wedge b\}\ c\ \{I\}$ です。示すことは、すべての $\sigma, \sigma'$ について

$I(\sigma)$ かつ $\langle w, \sigma \rangle \Downarrow \sigma'$ ならば、$I(\sigma')$ かつ $\llbracket b \rrbracket\sigma' = \mathrm{ff}$

です。これを、実行 $\langle w, \sigma \rangle \Downarrow \sigma'$ の導出の高さについての完全帰納法（内側の帰納法）で示します。$w$ を結論にもつ規則は (WhF) と (WhT) だけです。

実行の導出が (WhF) で終わるとき、$\llbracket b \rrbracket\sigma = \mathrm{ff}$ かつ $\sigma' = \sigma$ です。$I(\sigma)$ は仮定なので、$I(\sigma')$ かつ $\llbracket b \rrbracket\sigma' = \mathrm{ff}$ です。

実行の導出が (WhT) で終わるとき、$\llbracket b \rrbracket\sigma = \mathrm{tt}$、$\langle c, \sigma \rangle \Downarrow \sigma_1$、$\langle w, \sigma_1 \rangle \Downarrow \sigma'$ となる $\sigma_1$ があります。$(I \wedge b)(\sigma)$ なので、$\models \{I \wedge b\}\ c\ \{I\}$ から $I(\sigma_1)$ です。$\langle w, \sigma_1 \rangle \Downarrow \sigma'$ の導出は元の実行の導出の部分木で、高さが真に小さいので、内側の帰納法の仮定を $\sigma_1$ に使えて、$I(\sigma')$ かつ $\llbracket b \rrbracket\sigma' = \mathrm{ff}$ です。

以上で $\models \{I\}\ w\ \{I \wedge \lnot b\}$ が示されました。

∎

while の場合に帰納法が二重になるのは、Hoare 論理の導出の中では while は 1 回しか現れないのに、実行の導出の中では反復の回数だけ (WhT) が現れるからです。外側の帰納法（論理の導出）は本体についての事実を 1 つ与え、内側の帰納法（実行の導出）がそれを反復の回数だけ繰り返し使います。ループ不変条件は、この内側の帰納法の「帰納法の仮定」を表明として書いたものです。幅優先探索の正しさを 3 つの不変式で示した証明（補題 3.1［グラフアルゴリズム］）も、同じ形をしています。

注意 3.9（逆向き：相対完全性）

健全性の逆、「部分正当な三つ組はすべて導出できるか」は、表明として何を許すかに依存します。この記事のように表明を状態の任意の集合とすれば、定理 4.2 の $\mathrm{wlp}$ を中間の表明に使って、$\mathtt{call}$ を含まない命令についてはすべての部分正当な三つ組が導出できます。表明を一階算術の論理式に限ると、$\mathrm{wlp}$ がその言語で書けること（表現可能性）を別に示す必要があり、また (H-Conseq) の $P \Rightarrow P'$ の真偽は算術の真理に委ねられます。この「算術の真な含意をすべて使ってよいなら完全」という結果を相対完全性といい、S. A. Cook が 1978 年に示しました。証明は表現可能性の議論が長いので、この記事では扱いません。Winskel の教科書の第 7 章に証明があります。

3.4. 例：二分探索を Hoare 論理で書き直す

例 3.10（二分探索の検証条件）

探索アルゴリズム の lower_bound を言語 W で書きます。配列は書き換えないので、状態には入れず、固定した関数 $A : \mathbb{Z} \to \mathbb{Z}$（添字 $0, \ldots, n - 1$ の外では $0$）として、式 $A[a]$ の値を $A(\llbracket a \rrbracket\sigma)$ と定めます。これは状態の全域関数なので、ここまでの証明はそのまま通ります。$n \ge 0$ と $x$ も定数とします。

$$\begin{aligned} &lo := 0;\ hi := n; \\ &\mathtt{while}\ lo \lt hi\ \mathtt{do}\ \bigl(\, mid := lo + (hi - lo) \div 2;\ \mathtt{if}\ A[mid] \lt x\ \mathtt{then}\ lo := mid + 1\ \mathtt{else}\ hi := mid \,\bigr) \end{aligned}$$

事前条件は「$A$ は $0, \ldots, n - 1$ で昇順」ですが、$A$ は定数なので、これは状態によらない仮定です。ループ不変条件 $I$ は、既存の証明（定理 3.2［探索アルゴリズム］）の 3 条件の連言です。

$$I:\quad 0 \le lo \le hi \le n \ \wedge\ \bigl(\forall i \lt lo,\ A[i] \lt x\bigr) \ \wedge\ \bigl(\forall i \ge hi,\ i \lt n \Rightarrow A[i] \ge x\bigr)$$

（$i$ は $0 \le i \lt n$ を動きます。）Hoare 論理の規則を後ろからたどると、示すべきことは次の 3 つの含意（検証条件）に帰着します。

(V1) 初期化。 $\{\mathrm{true}\}\ lo := 0;\ hi := n\ \{I\}$ を導くには、(H-Assign) を 2 回使って事前条件 $(I[n/hi])[0/lo]$ を得ます。これは $0 \le 0 \le n \le n$ と「$i \lt 0$ なら…」「$i \ge n$ かつ $i \lt n$ なら…」の連言で、$n \ge 0$ のもとで成り立ちます。(H-Conseq) で $\mathrm{true}$ から導けます。

(V2) 保存。 本体を $c$ とします。$\{I \wedge lo \lt hi\}\ c\ \{I\}$ を導くには、(H-If) と (H-Assign) から、$mid$ への代入のあとで

$$\bigl(A[mid] \lt x \Rightarrow I[mid + 1/lo]\bigr) \ \wedge\ \bigl(A[mid] \ge x \Rightarrow I[mid/hi]\bigr)$$

が成り立てば十分で、さらに $mid$ に $lo + (hi - lo) \div 2$ を代入したものが $I \wedge lo \lt hi$ から従えば十分です。中身は「$lo \le mid \lt hi$」「$A[mid] \lt x$ なら $i \le mid$ のすべてで $A[i] \lt x$」「$A[mid] \ge x$ なら $i \ge mid$ のすべてで $A[i] \ge x$」で、既存の証明の「中央位置の範囲」と「保存」の段がちょうどこれを示しています。

(V3) 終了時。 (H-While) の結論の事後条件は $I \wedge \lnot(lo \lt hi)$ です。$I$ の $lo \le hi$ と合わせて $lo = hi$ で、$I$ の残りから $lo$ は $A[i] \lt x$ となる $i$ の個数、すなわち下限位置 $\mathrm{lb}_A(x)$（定義 3.1［探索アルゴリズム］）に等しいことが従います。(H-Conseq) で事後条件 $lo = \mathrm{lb}_A(x)$ を得ます。

(V1)〜(V3) から 定理 3.8 により $\models \{\mathrm{true}\}\ \text{（上のプログラム）}\ \{lo = \mathrm{lb}_A(x)\}$ です。Hoare 論理は、既存の証明の「初期化・保存・終了時」という段取りを、規則の適用として固定したものだと分かります。人が考える必要があるのは、不変条件 $I$ を見つけることと、3 つの含意を示すことだけです。

4. 最弱事前条件

命題 3.6 (2) は、代入について「事後条件 $Q$ を保証するもっとも弱い事前条件」が $Q[a/x]$ であることを述べていました。E. W. Dijkstra は、これをすべての命令に広げ、プログラムの意味を「事後条件から事前条件への写像」として捉えました。

定義 4.1（最弱事前条件）↗

解釈 $\mathcal{M}$、命令 $c$、表明 $Q$ に対して

$$\begin{aligned} \mathrm{wlp}(c, Q) &= \{\, \sigma \mid \text{すべての } \sigma' \text{ について、} \langle c, \sigma \rangle \Downarrow \sigma' \text{ ならば } Q(\sigma') \,\}, \\ \mathrm{wp}(c, Q) &= \{\, \sigma \mid c \text{ は } \sigma \text{ から停止し、すべての } \sigma' \text{ について、} \langle c, \sigma \rangle \Downarrow \sigma' \text{ ならば } Q(\sigma') \,\} \end{aligned}$$

と定める。$\mathrm{wlp}(c, Q)$ を最弱自由事前条件（weakest liberal precondition）、$\mathrm{wp}(c, Q)$ を最弱事前条件（weakest precondition）という。

定理 4.2（最弱事前条件の性質）✓

$\mathcal{M}$ を解釈、$c, c_1, c_2$ を命令、$P, Q, Q_1, Q_2$ を表明とする。

1. （特徴づけ）$\models_{\mathcal{M}} \{P\}\ c\ \{Q\}$ は $P \Rightarrow \mathrm{wlp}(c, Q)$ と同値である。また $P \Rightarrow \mathrm{wp}(c, Q)$ ならば $\models_{\mathcal{M}} [P]\ c\ [Q]$ である。
2. （単調性）$Q_1 \Rightarrow Q_2$ ならば $\mathrm{wlp}(c, Q_1) \Rightarrow \mathrm{wlp}(c, Q_2)$ かつ $\mathrm{wp}(c, Q_1) \Rightarrow \mathrm{wp}(c, Q_2)$。
3. （連言）$\mathrm{wlp}(c, Q_1 \wedge Q_2) = \mathrm{wlp}(c, Q_1) \wedge \mathrm{wlp}(c, Q_2)$、$\mathrm{wp}(c, Q_1 \wedge Q_2) = \mathrm{wp}(c, Q_1) \wedge \mathrm{wp}(c, Q_2)$。
4. （選言）$\mathcal{M}$ がすべての操作名について部分関数ならば、$\mathrm{wp}(c, Q_1 \vee Q_2) = \mathrm{wp}(c, Q_1) \vee \mathrm{wp}(c, Q_2)$、$\mathrm{wlp}(c, Q_1 \vee Q_2) = \mathrm{wlp}(c, Q_1) \vee \mathrm{wlp}(c, Q_2)$。さらにこのとき、$\models_{\mathcal{M}} [P]\ c\ [Q]$ は $P \Rightarrow \mathrm{wp}(c, Q)$ と同値である。
5. （計算規則）$\mathrm{wlp}(\mathtt{skip}, Q) = Q$、$\mathrm{wlp}(x := a, Q) = Q[a/x]$、$\mathrm{wlp}(c_1; c_2, Q) = \mathrm{wlp}(c_1, \mathrm{wlp}(c_2, Q))$、 $\mathrm{wlp}(\mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, Q) = \bigl(b \wedge \mathrm{wlp}(c_1, Q)\bigr) \vee \bigl(\lnot b \wedge \mathrm{wlp}(c_2, Q)\bigr)$。

証明（定理 4.2）

(1) $\models \{P\}\ c\ \{Q\}$ は「すべての $\sigma$ について、$P(\sigma)$ ならば（すべての $\sigma'$ について、$\langle c, \sigma \rangle \Downarrow \sigma'$ ならば $Q(\sigma')$）」と書き直せます。括弧の中は $\sigma \in \mathrm{wlp}(c, Q)$ の定義なので、これは $P \subseteq \mathrm{wlp}(c, Q)$ です。後半。$P \Rightarrow \mathrm{wp}(c, Q)$ とし、$P(\sigma)$ とします。$\sigma \in \mathrm{wp}(c, Q)$ なので $c$ は $\sigma$ から停止し、$\langle c, \sigma \rangle \Downarrow \sigma'$ となる $\sigma'$ があり、定義の後半から $Q(\sigma')$ です。これは全正当性の定義です。

(2) $\sigma \in \mathrm{wlp}(c, Q_1)$ とし、$\langle c, \sigma \rangle \Downarrow \sigma'$ とします。$Q_1(\sigma')$ で、$Q_1 \Rightarrow Q_2$ より $Q_2(\sigma')$ です。よって $\sigma \in \mathrm{wlp}(c, Q_2)$。$\mathrm{wp}$ は、これに「$\sigma$ から停止する」という $Q$ によらない条件が付くだけなので同じです。

(3) $\sigma \in \mathrm{wlp}(c, Q_1 \wedge Q_2)$ は「すべての $\sigma'$ について、$\langle c, \sigma \rangle \Downarrow \sigma'$ ならば $Q_1(\sigma')$ かつ $Q_2(\sigma')$」です。「すべての $\sigma'$ について $A(\sigma')$ ならば（$B_1(\sigma')$ かつ $B_2(\sigma')$）」は「（すべての $\sigma'$ について $A \Rightarrow B_1$）かつ（すべての $\sigma'$ について $A \Rightarrow B_2$）」と同値なので、これは $\sigma \in \mathrm{wlp}(c, Q_1)$ かつ $\sigma \in \mathrm{wlp}(c, Q_2)$ です。$\mathrm{wp}$ では両辺に同じ条件「$\sigma$ から停止する」が付きます。

(4) $Q_i \Rightarrow Q_1 \vee Q_2$ なので、(2) より $\mathrm{wp}(c, Q_i) \Rightarrow \mathrm{wp}(c, Q_1 \vee Q_2)$（$i = 1, 2$）で、右辺 $\subseteq$ 左辺が分かります（この向きに決定性は要りません）。逆を示します。$\sigma \in \mathrm{wp}(c, Q_1 \vee Q_2)$ とします。$c$ は $\sigma$ から停止するので $\langle c, \sigma \rangle \Downarrow \sigma'$ となる $\sigma'$ があり、補題 3.2 によりそのような $\sigma'$ はただ 1 つです。$Q_1(\sigma')$ または $Q_2(\sigma')$ が成り立ちます。$Q_1(\sigma')$ なら、実行の結果は $\sigma'$ だけなので「すべての結果が $Q_1$ を満たす」ことになり $\sigma \in \mathrm{wp}(c, Q_1)$ です。$Q_2(\sigma')$ なら同様に $\sigma \in \mathrm{wp}(c, Q_2)$ です。$\mathrm{wlp}$ については、$c$ が $\sigma$ から停止しない場合に $\sigma$ が $\mathrm{wlp}(c, Q_1)$ に（条件が空虚に成り立って）属することを加えれば、同じ議論です。

同値の主張。$\Leftarrow$ は (1) で示しました。$\models [P]\ c\ [Q]$ とし、$P(\sigma)$ とします。$\langle c, \sigma \rangle \Downarrow \sigma'$ かつ $Q(\sigma')$ となる $\sigma'$ があります。$c$ は $\sigma$ から停止し、補題 3.2 により結果は $\sigma'$ だけなので、すべての結果が $Q$ を満たします。よって $\sigma \in \mathrm{wp}(c, Q)$ です。

(5) $\mathtt{skip}$。$\langle \mathtt{skip}, \sigma \rangle \Downarrow \sigma'$ は $\sigma' = \sigma$ と同値（規則は (Skip) だけ）なので、$\sigma \in \mathrm{wlp}(\mathtt{skip}, Q)$ は $Q(\sigma)$ と同値です。

代入。命題 3.6 の (1) と (1) の特徴づけから $Q[a/x] \Rightarrow \mathrm{wlp}(x := a, Q)$。逆に (1) より $\models \{\mathrm{wlp}(x := a, Q)\}\ x := a\ \{Q\}$ なので、命題 3.6 の (2) から $\mathrm{wlp}(x := a, Q) \Rightarrow Q[a/x]$ です。

逐次。$\langle c_1; c_2, \sigma \rangle \Downarrow \sigma''$ は、「$\langle c_1, \sigma \rangle \Downarrow \sigma_1$ かつ $\langle c_2, \sigma_1 \rangle \Downarrow \sigma''$ となる $\sigma_1$ がある」ことと同値です（$\Rightarrow$ は、この形を結論にもつ規則が (Seq) だけであること、$\Leftarrow$ は (Seq) そのもの）。したがって

$$\begin{aligned} \sigma \in \mathrm{wlp}(c_1; c_2, Q) &\iff \forall \sigma_1\ \forall \sigma''\ \bigl(\langle c_1, \sigma \rangle \Downarrow \sigma_1 \text{ かつ } \langle c_2, \sigma_1 \rangle \Downarrow \sigma'' \Rightarrow Q(\sigma'')\bigr) \\ &\iff \forall \sigma_1\ \bigl(\langle c_1, \sigma \rangle \Downarrow \sigma_1 \Rightarrow \sigma_1 \in \mathrm{wlp}(c_2, Q)\bigr) \\ &\iff \sigma \in \mathrm{wlp}(c_1, \mathrm{wlp}(c_2, Q)) \end{aligned}$$

です。

条件分岐。$\llbracket b \rrbracket\sigma = \mathrm{tt}$ のとき、条件分岐の実行の導出は (IfT) でしか終われないので、$\langle \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, \sigma \rangle \Downarrow \sigma'$ は $\langle c_1, \sigma \rangle \Downarrow \sigma'$ と同値です。よってこのような $\sigma$ については、左辺に属することと $\sigma \in \mathrm{wlp}(c_1, Q)$ が同値で、右辺に属すること（$\lnot b$ の側は成り立たないので $\sigma \in \mathrm{wlp}(c_1, Q)$）とも同値です。$\llbracket b \rrbracket\sigma = \mathrm{ff}$ のときは $c_2$ について同じです。

∎

定理の五つの性質のうち、実際に計算で使うのは (1) と (5) です。(2)〜(4) は、条件を足したり弱めたりしても振る舞いが素直に変わることの確認です。先に次の具体例を見てから読むと分かりやすくなります。

(1) が名前の由来です。$\mathrm{wlp}(c, Q)$ は $\{P\}\ c\ \{Q\}$ を部分正当にする $P$ のうちでもっとも弱いものです。(5) の計算規則を後ろから順に使うと、ループを含まない命令の $\mathrm{wlp}$ は機械的に計算できます。例 3.10 の検証条件は、この計算の結果です。検証ツールが「ループ不変条件だけ人が書けば、あとは自動」と言えるのは、この計算規則と (1) によります。

例 4.3（絶対値の計算の最弱事前条件）

$c$ を $\mathtt{if}\ x \lt 0\ \mathtt{then}\ y := 0 - x\ \mathtt{else}\ y := x$ とし、事後条件 $Q$ を $y \ge 0$ とします。定理 4.2 (5) より

$$\mathrm{wlp}(c, Q) = \bigl(x \lt 0 \wedge Q[0 - x/y]\bigr) \vee \bigl(\lnot(x \lt 0) \wedge Q[x/y]\bigr) = (x \lt 0 \wedge 0 - x \ge 0) \vee (x \ge 0 \wedge x \ge 0).$$

$x \lt 0$ なら $-x \ge 0$ なので 1 つ目は $x \lt 0$、2 つ目は $x \ge 0$ で、選言は $\mathrm{true}$ です。事前条件なしで $y \ge 0$ が保証されます。

誤って $\mathtt{else}$ の枝も $y := 0 - x$ と書いた命令 $c'$ では、2 つ目が $x \ge 0 \wedge 0 - x \ge 0$、すなわち $x = 0$ になり、$\mathrm{wlp}(c', Q) = (x \le 0)$ です。誤った実装が契約を満たす入力の範囲が、式として得られました。$x \le 0$ の入力だけでテストすると、この誤りは見つかりません。

例 4.4（非決定的な操作では選言と可換でない）

定理 4.2 (4) の仮定は落とせません。操作 $m$ の解釈を $\mathcal{M}(m) = \{(\sigma, \sigma[x \mapsto 0]) \mid \sigma \in \Sigma\} \cup \{(\sigma, \sigma[x \mapsto 1]) \mid \sigma \in \Sigma\}$（$x$ に $0$ か $1$ のどちらかを入れる）とします。$\mathtt{call}\ m$ はどの状態からも停止し、結果は必ず $x = 0 \vee x = 1$ を満たすので、$\mathrm{wp}(\mathtt{call}\ m, x = 0 \vee x = 1) = \mathrm{true}$ です。一方、どの状態からも $x = 1$ となる実行があるので $\mathrm{wp}(\mathtt{call}\ m, x = 0) = \mathrm{false}$、同様に $\mathrm{wp}(\mathtt{call}\ m, x = 1) = \mathrm{false}$ で、選言は $\mathrm{false}$ です。並行プログラムや、仕様が複数の結果を許す操作では、この違いが現れます。

5. 停止性と全正当性

(H-While) は、ループが止まることを何も保証しません。停止性を示すには、反復のたびに「減っていく量」を見つけます。

定義 5.1（ループ変量）↗

ループ $\mathtt{while}\ b\ \mathtt{do}\ c$ と表明 $I$ に対し、写像 $v : \Sigma \to \mathbb{Z}$ が次の 2 条件を満たすとき、$v$ を（不変条件 $I$ のもとでの）ループ変量という。

• （下に有界）$I(\sigma)$ かつ $\llbracket b \rrbracket\sigma = \mathrm{tt}$ ならば $v(\sigma) \ge 0$。
• （真に減る）すべての $k \in \mathbb{Z}$ について $\models [I \wedge b \wedge v = k]\ c\ [I \wedge v \lt k]$。ここで $v = k$ は表明 $\{\sigma \mid v(\sigma) = k\}$、$v \lt k$ は $\{\sigma \mid v(\sigma) \lt k\}$ を表す。

2 つ目の条件は、本体 $c$ が停止すること、不変条件 $I$ を保つこと、変量を真に減らすことを 1 つの全正当な三つ組にまとめたものです。

次の定理の証明の方針は、背理法です。「止まらない状態」があるとして、その中で変量が最小のものを取り出し、本体を 1 回実行すると、変量がもっと小さい状態に移ることを使って矛盾を導きます。自然数には最小元があるので、このように「最小の悪い例」を取れます。

定理 5.2（変量による停止性：全正当性の規則の健全性）✓

$\mathcal{M}$ を解釈とする。

1. ループ $\mathtt{while}\ b\ \mathtt{do}\ c$ が、表明 $I$ のもとでループ変量 $v$ をもつならば、$\models_{\mathcal{M}} [I]\ \mathtt{while}\ b\ \mathtt{do}\ c\ [I \wedge \lnot b]$ である。
2. $\mathtt{call}$ を含まない命令について、定義 3.7 の (H-Skip)・(H-Assign)・(H-Seq)・(H-If)・(H-Conseq) は、三つ組を全正当性 $[P]\ c\ [Q]$ に読み替えても正しい。すなわち、各規則の前提の三つ組がすべて全正当ならば、結論の三つ組も全正当である。

証明（定理 5.2）

(1) $w = \mathtt{while}\ b\ \mathtt{do}\ c$ とおき、状態 $\sigma$ が良いとは「$\langle w, \sigma \rangle \Downarrow \sigma''$、$I(\sigma'')$、$\llbracket b \rrbracket\sigma'' = \mathrm{ff}$ を満たす $\sigma''$ が存在する」ことと定めます。$I$ を満たす状態がすべて良いことを示せば、それが結論です。

まず、$I(\sigma)$ かつ $\llbracket b \rrbracket\sigma = \mathrm{ff}$ である $\sigma$ は良い状態です。(WhF) より $\langle w, \sigma \rangle \Downarrow \sigma$ で、$\sigma'' = \sigma$ が条件を満たすからです。

背理法で、$I$ を満たすのに良くない状態があると仮定します。そのような状態の全体を $B$ とします。いま見たことから、$B$ の元 $\sigma$ では $\llbracket b \rrbracket\sigma = \mathrm{tt}$ で、変量の 1 つ目の条件から $v(\sigma) \ge 0$ です。したがって

$$S = \{\, v(\sigma) + 1 \mid \sigma \in B \,\}$$

は $\mathbb{N} = \{1, 2, \ldots\}$ の空でない部分集合です。整列性（公理 3.1［証明の技術］）により $S$ は最小元をもつので、$v(\sigma) + 1$ がその最小元になる $\sigma \in B$ をとります。

$k = v(\sigma)$ とおくと $(I \wedge b \wedge v = k)(\sigma)$ なので、変量の 2 つ目の条件から、$\langle c, \sigma \rangle \Downarrow \sigma_1$、$I(\sigma_1)$、$v(\sigma_1) \lt k$ を満たす $\sigma_1$ があります。$\sigma_1$ は良い状態です。実際、$\llbracket b \rrbracket\sigma_1 = \mathrm{ff}$ なら先に見たとおり良く、$\llbracket b \rrbracket\sigma_1 = \mathrm{tt}$ のとき、もし $\sigma_1 \in B$ なら $v(\sigma_1) + 1 \in S$ かつ $v(\sigma_1) + 1 \lt v(\sigma) + 1$ となって最小性に反するからです。

$\sigma_1$ が良いので、$\langle w, \sigma_1 \rangle \Downarrow \sigma''$、$I(\sigma'')$、$\llbracket b \rrbracket\sigma'' = \mathrm{ff}$ となる $\sigma''$ があります。$\llbracket b \rrbracket\sigma = \mathrm{tt}$、$\langle c, \sigma \rangle \Downarrow \sigma_1$、$\langle w, \sigma_1 \rangle \Downarrow \sigma''$ に (WhT) を使うと $\langle w, \sigma \rangle \Downarrow \sigma''$ です。これは $\sigma$ が良いことを意味し、$\sigma \in B$ に反します。よって $B$ は空です。

(2) 各規則を順に確かめます。

(H-Skip)。$P(\sigma)$ とします。(Skip) より $\langle \mathtt{skip}, \sigma \rangle \Downarrow \sigma$ で、$P(\sigma)$ です。

(H-Assign)。$Q[a/x](\sigma)$ とします。$\sigma' = \sigma[x \mapsto \llbracket a \rrbracket\sigma]$ とおくと (Assign) より $\langle x := a, \sigma \rangle \Downarrow \sigma'$ で、定義 3.4 より $Q(\sigma')$ です。

(H-Seq)。$\models [P]\ c_1\ [R]$、$\models [R]\ c_2\ [Q]$ とし、$P(\sigma)$ とします。1 つ目から $\langle c_1, \sigma \rangle \Downarrow \sigma_1$ かつ $R(\sigma_1)$ となる $\sigma_1$ があり、2 つ目から $\langle c_2, \sigma_1 \rangle \Downarrow \sigma'$ かつ $Q(\sigma')$ となる $\sigma'$ があります。(Seq) より $\langle c_1; c_2, \sigma \rangle \Downarrow \sigma'$ です。

(H-If)。$\models [P \wedge b]\ c_1\ [Q]$、$\models [P \wedge \lnot b]\ c_2\ [Q]$ とし、$P(\sigma)$ とします。$\llbracket b \rrbracket\sigma = \mathrm{tt}$ なら 1 つ目から $\langle c_1, \sigma \rangle \Downarrow \sigma'$ かつ $Q(\sigma')$ となる $\sigma'$ があり、(IfT) より条件分岐も $\sigma$ から $\sigma'$ に至ります。$\mathrm{ff}$ なら 2 つ目と (IfF) で同じです。

(H-Conseq)。$P \Rightarrow P'$、$\models [P']\ c\ [Q']$、$Q' \Rightarrow Q$ とし、$P(\sigma)$ とします。$P'(\sigma)$ なので $\langle c, \sigma \rangle \Downarrow \sigma'$ かつ $Q'(\sigma')$ となる $\sigma'$ があり、$Q(\sigma')$ です。

∎

証明の核は、「良くない状態があれば、変量が最小のものをとれる」という 1 点です。変量の値が整礎な集合（無限に下がり続ける列が無い集合）に入っていることが効いています。値が有理数だと、この議論は使えません。有理数の変数 $x$ について「$x \gt 0$ のあいだ $x$ を半分にする」ループは、$x$ が毎回真に減り $0$ 以上にとどまりますが、止まりません。$1, 1/2, 1/4, \ldots$ は、下に有界でも最小元に到達しないからです。

例 5.3（二分探索の変量）

例 3.10 のループに、変量 $v = hi - lo$ をとります。$I \wedge lo \lt hi$ のもとで $v \ge 1 \ge 0$ です。本体は代入と条件分岐だけなので必ず停止し、$I$ を保つことは検証条件 (V2) で見ました。$lo \le mid \lt hi$ なので、$lo := mid + 1$ のあとの $v$ は $hi - mid - 1 \lt hi - lo$、$hi := mid$ のあとの $v$ は $mid - lo \lt hi - lo$ で、どちらも真に減ります。定理 5.2 (1) と、初期化の部分への (2) の適用から、プログラム全体が全正当です。これは 定理 3.2［探索アルゴリズム］ の「必ず停止し、下限位置を返す」と同じ主張です。変量は「あと何回まわりうるか」の上界でもあり、毎回 $1$ 以上減る非負整数なので、反復は高々 $n$ 回です。実際には半分以下に減ることを使うと $\lfloor \log_2 n \rfloor + 1$ 回という評価が得られます（定理 3.3［探索アルゴリズム］）。

例 5.4（中点の計算と値の範囲）

言語 W の変数は任意の整数をとりますが、多くの言語の整数型は範囲が有限です。32 ビットの符号つき整数は $-2^{31}$ から $2^{31} - 1 = 2147483647$ までで、範囲を超えた加算の結果は $2^{32}$ を法として折り返します（言語によっては未定義の動作です）。中点を $(lo + hi) \div 2$ と書いた二分探索で、$lo = 2^{30} = 1073741824$、$hi = 2^{30} + 2 = 1073741826$ になったとします。数学的な和は $2147483650$ で、$2^{31} - 1$ を $3$ 超えます。折り返した値は $2147483650 - 2^{32} = -2147483646$、その半分は $-1073741823$ で、添字として範囲外です。

W の上での証明は、この実装の正しさを保証しません。証明した対象（整数が無限にある言語のプログラム）と、動かす対象（32 ビットで折り返す機械の上のプログラム）が違うからです。契約に値の範囲を入れると食い違いが見えます。「すべての中間結果が $2^{31} - 1$ 以下」を不変条件に足そうとすると、$lo + hi \le 2n - 1$ までしか言えないので、事前条件に $n \le 2^{30}$ が必要になります。一方 $lo + (hi - lo) \div 2$ なら、中間結果は $hi - lo \le n$ と $mid \lt hi \le n$ で、事前条件は $n \le 2^{31} - 1$ で足ります。契約は、どのモデルの上の主張なのかまで含めて書いて、はじめて実装を縛ります。

6. 表現不変条件と抽象化関数

ここまでは 1 つの手続きの契約でした。クラス（抽象データ型）は、内部の状態を複数の操作が共有します。操作ごとの事前・事後条件に加えて、「操作と操作のあいだで、内部の状態がいつも満たしている条件」が要ります。

定義 6.1（データ型の実装・表現不変条件・抽象化関数）↗

データ型の実装とは、次の組 $(\mathrm{Rep}, \mathrm{Init}, (\mathrm{op}_m)_{m \in \mathrm{Op}})$ をいう。

• $\mathrm{Rep}$ は表現（内部の状態）の集合、$\mathrm{Init} \subseteq \mathrm{Rep}$ は構築子が作りうる表現の集合。
• 各公開操作 $m \in \mathrm{Op}$ は、引数の集合 $X_m$、結果の集合 $Y_m$、事前条件 $\mathrm{pre}_m \subseteq \mathrm{Rep} \times X_m$ と、写像 $\mathrm{op}_m : \mathrm{Rep} \times X_m \to \mathrm{Rep} \times Y_m$（新しい表現と結果を返す）をもつ。

表現不変条件とは、部分集合 $\mathrm{Inv} \subseteq \mathrm{Rep}$ をいう。集合 $A$（抽象値の集合）への写像 $\alpha : \mathrm{Inv} \to A$ を抽象化関数という。

このデータ型を使うプログラムの実行とは、表現と呼び出し側の状態の組の列 $(r_0, e_0), (r_1, e_1), \ldots, (r_N, e_N)$ をいう。実行が表現を漏らさないとは、$r_0 \in \mathrm{Init}$ であり、各 $i \lt N$ について次のどちらかが成り立つことをいう。

• （公開操作の呼び出し）ある $m \in \mathrm{Op}$ と $x \in X_m$ があって、$(r_i, x) \in \mathrm{pre}_m$ かつ $\mathrm{op}_m(r_i, x) = (r_{i+1}, y)$（$y$ は結果）。
• （呼び出し側の動作）$r_{i+1} = r_i$。

「表現を漏らさない」は、表現が変わるのは公開操作を通したときだけ、という条件です。呼び出し側が自分の状態 $e$ をどう変えようと、表現 $r$ には触れられません。プログラミング言語では、フィールドを非公開にし、内部の可変なオブジェクトへの参照（別名）を外に渡さないことで、この条件を成り立たせます。

定理 6.2（表現不変条件の帰納法）✓

データ型の実装と表現不変条件 $\mathrm{Inv}$ が次の 2 条件を満たすとする。

• （成立）$\mathrm{Init} \subseteq \mathrm{Inv}$。
• （保存）すべての $m \in \mathrm{Op}$、$r \in \mathrm{Inv}$、$x \in X_m$ について、$(r, x) \in \mathrm{pre}_m$ かつ $\mathrm{op}_m(r, x) = (r', y)$ ならば $r' \in \mathrm{Inv}$。

このとき、表現を漏らさない任意の実行 $(r_0, e_0), \ldots, (r_N, e_N)$ について、すべての $i$ で $r_i \in \mathrm{Inv}$ である。

証明（定理 6.2）

$i$ についての帰納法（定理 3.2［証明の技術］。$i = 0$ から始めます）で示します。

$i = 0$。表現を漏らさない実行の定義から $r_0 \in \mathrm{Init}$ で、（成立）より $r_0 \in \mathrm{Inv}$ です。

$i \lt N$ とし、$r_i \in \mathrm{Inv}$ と仮定します。定義から、$i$ 番目の段は 2 種類のどちらかです。公開操作の呼び出しなら、$(r_i, x) \in \mathrm{pre}_m$ かつ $\mathrm{op}_m(r_i, x) = (r_{i+1}, y)$ で、$r_i \in \mathrm{Inv}$ なので（保存）より $r_{i+1} \in \mathrm{Inv}$ です。呼び出し側の動作なら $r_{i+1} = r_i \in \mathrm{Inv}$ です。

∎

証明は短いですが、使い道は大きい定理です。（保存）を確かめるとき、各操作は入口で不変条件を仮定してよい。$\mathrm{Inv}$ は、操作から見れば「いつでも使ってよい事前条件」であり、同時に「必ず守るべき事後条件」です。これは (H-While) と同じ形をしています。オブジェクトの一生を「公開操作を任意の順で繰り返すループ」とみれば、表現不変条件はそのループ不変条件です。

定理の 3 つの仮定（成立・保存・漏らさない）は、どれも落とせません。3 つ目が破れる例を実行して確かめます。

例 6.3（表現が漏れると不変条件が破れる）

整列済みのリストで集合を表すクラスです。表現不変条件は「_xs は狭義昇順」で、add と in はこれを前提に二分探索を使います。

# Python 3.12.14（標準ライブラリのみ）
import bisect

class SortedSet:
    """表現: リスト _xs。表現不変条件: _xs は狭義昇順（整列済みで重複がない）。"""
    def __init__(self):
        self._xs = []
    def _inv(self):
        return all(self._xs[i] < self._xs[i + 1] for i in range(len(self._xs) - 1))
    def add(self, x):
        i = bisect.bisect_left(self._xs, x)          # 不変条件を使う（二分探索）
        if i == len(self._xs) or self._xs[i] != x:
            self._xs.insert(i, x)
    def __contains__(self, x):
        i = bisect.bisect_left(self._xs, x)          # 不変条件を使う
        return i < len(self._xs) and self._xs[i] == x
    def items_leaky(self):
        return self._xs                              # 表現そのもの（別名）を返す
    def items(self):
        return list(self._xs)                        # コピーを返す

for getter in ("items_leaky", "items"):
    s = SortedSet()
    for x in (5, 1, 3):
        s.add(x)
    view = getattr(s, getter)()
    view.append(0)                                   # 呼び出し側が受け取ったリストを書き換える
    s.add(2)
    print(f"{getter:12s} 表現 = {s._xs}  不変条件 = {s._inv()}  0 in s = {0 in s}  5 in s = {5 in s}")

items_leaky  表現 = [1, 2, 3, 5, 0]  不変条件 = False  0 in s = False  5 in s = False
items        表現 = [1, 2, 3, 5]  不変条件 = True  0 in s = False  5 in s = True

items_leaky は内部のリストそのものを返すので、呼び出し側の view.append(0) が表現を直接書き換えます。これは 定義 6.1 の 2 種類の段のどちらでもありません（公開操作でないのに $r$ が変わっています）。不変条件が破れた結果、add で入れたはずの 5 が「入っていない」と答えています。二分探索が、整列を前提に 5 の位置を通り過ぎるからです。壊れたのは items_leaky を呼んだ時点ではなく、あとで別の操作を呼んだときで、原因と症状が離れます。items はコピーを返すので、呼び出し側が何をしても表現は変わらず、定理 6.2 の仮定が保たれます。

不変条件は「表現が壊れていない」ことを言うだけで、操作が仕様どおりの答えを返すことまでは言いません。それを言うのが抽象化関数です。

抽象化関数 α と操作の可換性。実装の側で操作してから抽象化しても、抽象化してから仕様の側で操作しても、同じ抽象値と同じ結果 y になる。

命題 6.4（抽象化関数が操作と可換なら実装は仕様を満たす）✓

抽象仕様として、抽象値の集合 $A$、初期値 $a_0 \in A$、各 $m \in \mathrm{Op}$ の事前条件 $\mathrm{pre}^A_m \subseteq A \times X_m$ と写像 $\mathrm{op}^A_m : A \times X_m \to A \times Y_m$ が与えられているとする。データ型の実装 $(\mathrm{Rep}, \mathrm{Init}, (\mathrm{op}_m))$、表現不変条件 $\mathrm{Inv}$、抽象化関数 $\alpha : \mathrm{Inv} \to A$ が次を満たすとする。

• （初期値）$\mathrm{Init} \subseteq \mathrm{Inv}$ で、すべての $r \in \mathrm{Init}$ について $\alpha(r) = a_0$。
• （可換性）すべての $m$、$r \in \mathrm{Inv}$、$x \in X_m$ について、$(\alpha(r), x) \in \mathrm{pre}^A_m$ かつ $\mathrm{op}_m(r, x) = (r', y)$ ならば、$r' \in \mathrm{Inv}$ かつ $\mathrm{op}^A_m(\alpha(r), x) = (\alpha(r'), y)$。

操作の列 $(m_1, x_1), \ldots, (m_N, x_N)$ を、抽象仕様の側で $a_0$ から順に実行した抽象値と結果を $a_i$、$y^A_i$（$\mathrm{op}^A_{m_i}(a_{i-1}, x_i) = (a_i, y^A_i)$）とし、各段で事前条件 $(a_{i-1}, x_i) \in \mathrm{pre}^A_{m_i}$ が成り立つとする。同じ列を実装の側で $r_0 \in \mathrm{Init}$ から順に実行した表現と結果を $r_i$、$y_i$（$\mathrm{op}_{m_i}(r_{i-1}, x_i) = (r_i, y_i)$）とする。このとき、すべての $i$ について

$$r_i \in \mathrm{Inv}, \qquad \alpha(r_i) = a_i, \qquad y_i = y^A_i \quad (i \ge 1)$$

が成り立つ。すなわち、呼び出し側が観測する結果の列は、抽象仕様のものと一致する。

証明（命題 6.4）

$i$ についての帰納法（定理 3.2［証明の技術］）で、「$r_i \in \mathrm{Inv}$ かつ $\alpha(r_i) = a_i$（$i \ge 1$ ならさらに $y_i = y^A_i$）」を示します。

$i = 0$。（初期値）より $r_0 \in \mathrm{Inv}$ かつ $\alpha(r_0) = a_0$ です。

$i - 1$ で成り立つとします。$r_{i-1} \in \mathrm{Inv}$、$\alpha(r_{i-1}) = a_{i-1}$ です。仮定から $(a_{i-1}, x_i) \in \mathrm{pre}^A_{m_i}$、すなわち $(\alpha(r_{i-1}), x_i) \in \mathrm{pre}^A_{m_i}$ です。$\mathrm{op}_{m_i}(r_{i-1}, x_i) = (r_i, y_i)$ に（可換性）を使うと、$r_i \in \mathrm{Inv}$ かつ

$$\mathrm{op}^A_{m_i}(a_{i-1}, x_i) = \mathrm{op}^A_{m_i}(\alpha(r_{i-1}), x_i) = (\alpha(r_i), y_i)$$

です。左辺は定義により $(a_i, y^A_i)$ なので、$\alpha(r_i) = a_i$ かつ $y_i = y^A_i$ です。

∎

呼び出し側は表現 $r_i$ を見られず、結果 $y_i$ だけを見ます。その $y_i$ が仕様のものと一致するので、呼び出し側からは実装と仕様を区別できません。これは C. A. R. Hoare が 1972 年に示した、データ表現の正しさの証明法のもっとも簡単な形です。次々章のモデルベーステストは、この命題の対偶（結果の列が食い違えば、可換性がどこかで破れている）を使います。

例 6.5（整列済みリストによる集合）

例 6.3 の SortedSet で、抽象値を整数の有限集合、$\alpha(xs) = \{xs[0], \ldots, xs[\ell - 1]\}$（リストの要素の集合）とします。抽象仕様は $\mathrm{add}^A(S, x) = (S \cup \{x\}, \text{なし})$、$\mathrm{contains}^A(S, x) = (S, [x \in S])$ です。可換性を確かめます。xs が狭義昇順のとき、bisect_left(xs, x) は下限位置 $i$ を返します（定理 3.2［探索アルゴリズム］）。$x \in \alpha(xs)$ なら $xs[i] = x$ で、add は何もせず、$\alpha$ は $S = S \cup \{x\}$ のままです。$x \notin \alpha(xs)$ なら $i$ の左はすべて $x$ より小さく、$i$ 以降はすべて $x$ より大きいので、位置 $i$ への挿入は狭義昇順を保ち、要素の集合は $S \cup \{x\}$ になります。in は $i \lt \ell$ かつ $xs[i] = x$ を返し、これは $x \in S$ と同値です。命題 6.4 により、SortedSet は表現を漏らさないかぎり集合として振る舞います。

可換性の検証で、不変条件（狭義昇順）を 2 度使いました。二分探索が正しい位置を返すためと、挿入後も昇順であることを言うためです。不変条件のない表現（整列していないリスト）でも集合は実装できますが、そのときは $\alpha$ は同じでも操作の実装が線形探索になります。不変条件を強くするほど、操作の実装は多くを仮定でき、速くできる代わりに、保存の義務が重くなります。

例 6.6（有理数クラスの不変条件）

有理数を整数の組 $(p, q)$ で表し、$\mathrm{Inv}$ を「$q \gt 0$ かつ $\gcd(p, q) = 1$」、$\alpha(p, q) = p/q \in \mathbb{Q}$ とします。この不変条件のもとで $\alpha$ は単射です。$p/q = p'/q'$ なら $pq' = p'q$ で、$\gcd(p, q) = 1$ より $q \mid q'$、対称に $q' \mid q$、分母は正なので $q = q'$、よって $p = p'$ です。したがって有理数として等しいことと、表現が等しいことが同値になり、等価性の判定を成分の比較で済ませられます。ハッシュ値を成分から計算してよいのも同じ理由です。

加法を $(p, q) + (p', q') = (pq' + p'q,\ qq')$ とだけ実装すると、（保存）が破れます。$(1, 2) + (1, 2) = (4, 4)$ で $\gcd = 4$ です。$\alpha$ の値は $1$ で正しいので、足し算の結果を表示するだけのテストは通りますが、$(4, 4)$ と $(1, 1)$ の成分比較は「等しくない」と答えます。結果を $g = \gcd(pq' + p'q, qq')$ で割って $((pq' + p'q)/g,\ qq'/g)$ を返せば、分母は正のまま、成分は互いに素になり、（保存）が成り立ちます。構築子も同じ正規化をして、$q = 0$ を事前条件で排除し、$q \lt 0$ なら符号を分子に移す必要があります。

7. 振る舞いの部分型：契約の強弱と差し替え

インターフェースを通してモジュールを使う利点は、実装を取り替えられることでした。取り替えてよい条件を、契約の強弱で述べます。

定義 7.1（契約の精密化（振る舞いの部分型））↗

$\mathcal{C}, \mathcal{C}'$ を契約表（定義 3.7）とする。すべての $(m, P, Q) \in \mathcal{C}$ に対して、

$$P \Rightarrow P' \qquad \text{かつ} \qquad Q' \Rightarrow Q$$

を満たす $(m, P', Q') \in \mathcal{C}'$ が存在するとき、$\mathcal{C}'$ は $\mathcal{C}$ を精密化するという。$\mathcal{C}$ を上位型の契約、$\mathcal{C}'$ を下位型の契約とみるとき、下位型は上位型の振る舞いの部分型であるという。

下位型は、事前条件を弱めてよく（より多くの状況で呼べる）、事後条件を強めてよい（より多くを約束する）。逆は許されません。

定理 7.2（置換原則）✓

契約表 $\mathcal{C}'$ が $\mathcal{C}$ を精密化し、解釈 $\mathcal{M}'$ が $\mathcal{C}'$ を満たすとする。このとき

1. $\mathcal{M}'$ は $\mathcal{C}$ も満たす。
2. $\vdash_{\mathcal{C}} \{A\}\ c\ \{B\}$ ならば $\models_{\mathcal{M}'} \{A\}\ c\ \{B\}$ である。すなわち、上位型の契約だけを使って導出した呼び出し側の三つ組は、操作を下位型の実装に差し替えても部分正当である。

証明（定理 7.2）

(1) $(m, P, Q) \in \mathcal{C}$ をとります。精密化の定義から、$P \Rightarrow P'$ かつ $Q' \Rightarrow Q$ を満たす $(m, P', Q') \in \mathcal{C}'$ があり、$\mathcal{M}'$ は $\mathcal{C}'$ を満たすので $\models_{\mathcal{M}'} \{P'\}\ \mathtt{call}\ m\ \{Q'\}$ です。$P(\sigma)$ かつ $\langle \mathtt{call}\ m, \sigma \rangle \Downarrow \sigma'$（$\mathcal{M}'$ のもとで）とすると、$P \Rightarrow P'$ より $P'(\sigma)$、したがって $Q'(\sigma')$、$Q' \Rightarrow Q$ より $Q(\sigma')$ です。よって $\models_{\mathcal{M}'} \{P\}\ \mathtt{call}\ m\ \{Q\}$ で、これがすべての $(m, P, Q) \in \mathcal{C}$ について成り立つので、$\mathcal{M}'$ は $\mathcal{C}$ を満たします。この議論は帰結の規則 (H-Conseq) の正しさと同じものです。

(2) (1) より $\mathcal{M}'$ は $\mathcal{C}$ を満たすので、定理 3.8 を契約表 $\mathcal{C}$ と解釈 $\mathcal{M}'$ に使えば $\models_{\mathcal{M}'} \{A\}\ c\ \{B\}$ です。

∎

この定理は、B. Liskov と J. Wing が 1994 年に定式化した置換原則の、契約による形です。定理の内容は「呼び出し側の証明は、操作の実装ではなく契約表 $\mathcal{C}$ にしか依存しない」ことに尽きます。健全性定理を、解釈を任意にとって述べておいたのはこのためです。

型との対応。 関数型の部分型は、引数について反変、戻り値について共変でした（命題 6.7［プログラミング言語論］）。型 $T$ を「値が $T$ に属する」という表明とみれば、関数型 $S_1 \to S_2$ は契約（事前条件 $x \in S_1$、事後条件 結果 $\in S_2$）です。$T_1 \le S_1$ は「$x \in T_1 \Rightarrow x \in S_1$」、$S_2 \le T_2$ は「結果 $\in S_2 \Rightarrow$ 結果 $\in T_2$」なので、$S_1 \to S_2 \le T_1 \to T_2$ の条件は、定義 7.1 で上位型を $T_1 \to T_2$、下位型を $S_1 \to S_2$ としたものにちょうど一致します。型検査器が確かめられるのは型で書ける契約だけで、「高さは変わらない」のような契約は型では書けないので、型検査を通る下位クラスが振る舞いの部分型であるとは限りません。次の例がそれです。

例 7.3（正方形は長方形の振る舞いの部分型か）

長方形の操作 set_width(w) の契約を、実行前の高さ $h_0$ ごとに

• 事前条件 $P$: $w \gt 0 \wedge \mathit{height} = h_0$
• 事後条件 $Q$: $\mathit{width} = w \wedge \mathit{height} = h_0$

とします。「正方形は長方形の一種」なので下位クラスにしたくなりますが、正方形は幅を変えると高さも変わります。

# Python 3.12.14（標準ライブラリのみ）
class Rectangle:
    """契約: set_width(w) は w > 0 を事前条件とし、事後に width == w かつ height は変わらない。"""
    def __init__(self, width, height):
        self.width, self.height = width, height
    def set_width(self, w):
        self.width = w
    def area(self):
        return self.width * self.height

class Square(Rectangle):
    """事後条件を弱めた下位クラス: 「height は変わらない」を守らない。"""
    def __init__(self, side):
        super().__init__(side, side)
    def set_width(self, w):
        self.width = self.height = w

class SmallRectangle(Rectangle):
    """事前条件を強めた下位クラス: w <= 10 を要求する。"""
    def set_width(self, w):
        if w > 10:
            raise ValueError("w は 10 以下")
        self.width = w

def client(r):
    """Rectangle の契約だけを使って書いた呼び出し側。事前条件 w > 0 は満たしている。"""
    h = r.height
    r.set_width(20)
    assert r.area() == 20 * h, f"面積 {r.area()} != {20 * h}"
    return r.area()

for obj in (Rectangle(3, 5), Square(5), SmallRectangle(3, 5)):
    try:
        print(type(obj).__name__, "->", client(obj))
    except (AssertionError, ValueError) as e:
        print(type(obj).__name__, "->", type(e).__name__ + ":", e)

Rectangle -> 100
Square -> AssertionError: 面積 400 != 100
SmallRectangle -> ValueError: w は 10 以下

client は、契約 $(P, Q)$ から「set_width(20) のあとの面積は $20 h_0$」を導いています。これは $\vdash_{\mathcal{C}}$ の導出で、Rectangle では 定理 3.8 のとおり成り立ちます。

Square の set_width の事後条件は $Q'$: $\mathit{width} = w \wedge \mathit{height} = w$ です。$h_0 = 5$、$w = 20$ のとき $Q'$ を満たす状態は $\mathit{height} = 20$ で、$Q$ を満たしません。$Q' \Rightarrow Q$ が成り立たないので 定義 7.1 の条件が破れ、定理 7.2 は適用できません。実際に呼び出し側の表明が落ちています。SmallRectangle は事前条件が $P'$: $0 \lt w \le 10 \wedge \mathit{height} = h_0$ で、$P \Rightarrow P'$ が成り立ちません（$w = 20$）。呼び出し側は上位型の事前条件を守っているのに、例外を受け取ります。

Square を「幅と高さが等しい」という不変条件をもつ不変な値（set_width を持たない）として設計すれば、問題は起きません。壊れるのは「正方形は長方形である」という包含関係ではなく、「正方形は、長方形の変更操作の契約を守る」という主張です。

8. 契約を検査する：実行時の表明と、その限界

契約を assert としてコードに書くと、実行のたびに検査できます。二分探索に、事前条件・ループ不変条件・変量・事後条件をすべて書いてみます。

例 8.1（表明つきの二分探索と、誤りが見つかる入力）

buggy=True のとき、hi = mid を hi = mid - 1 と誤ります（mid 自身がまだ答えの候補であることを忘れる、よくある誤りです）。$\{0, 1, 2\}$ 上の長さ $4$ 以下の昇順の列すべてと、$x \in \{0, 1, 2, 3\}$ の組 $140$ 個を入力にします。

# Python 3.12.14（標準ライブラリのみ）
from itertools import combinations_with_replacement

def lower_bound(a, x, buggy=False):
    """a[i] >= x となる最小の i を返す（無ければ len(a)）。契約を assert で書いたもの。"""
    n = len(a)
    assert all(a[i] <= a[i + 1] for i in range(n - 1)), "事前条件: a は昇順"
    lo, hi = 0, n
    while lo < hi:
        assert 0 <= lo <= hi <= n, "不変条件 I1"
        assert all(a[i] < x for i in range(lo)), "不変条件 I2"
        assert all(a[i] >= x for i in range(hi, n)), "不変条件 I3"
        variant = hi - lo
        mid = lo + (hi - lo) // 2
        if a[mid] < x:
            lo = mid + 1
        else:
            hi = mid - 1 if buggy else mid      # 誤り: mid 自身を答えの候補から外してしまう
        assert 0 <= hi - lo < variant, "変量 hi - lo が減り、負にならない"
    assert 0 <= lo <= hi <= n, "不変条件 I1"
    assert all(a[i] < x for i in range(lo)), "不変条件 I2"
    assert all(a[i] >= x for i in range(hi, n)), "不変条件 I3"
    assert lo == sum(1 for v in a if v < x), "事後条件: 返り値は下限位置"
    return lo

def survey(buggy):
    total, failed, first = 0, {}, None
    for n in range(0, 5):
        for a in combinations_with_replacement(range(3), n):   # {0,1,2} 上の昇順の列
            for x in range(4):
                total += 1
                try:
                    lower_bound(list(a), x, buggy)
                except AssertionError as e:
                    failed[str(e)] = failed.get(str(e), 0) + 1
                    first = first or (list(a), x, str(e))
    return total, failed, first

for buggy in (False, True):
    total, failed, first = survey(buggy)
    print("誤りあり" if buggy else "正しい実装", "| 入力", total, "個 | 表明違反", sum(failed.values()), "個")
    for k, v in sorted(failed.items()):
        print("   ", k, ":", v)
    if first:
        print("    最初の違反:", first)

正しい実装 | 入力 140 個 | 表明違反 0 個
誤りあり | 入力 140 個 | 表明違反 53 個
    不変条件 I3 : 15
    変量 hi - lo が減り、負にならない : 38
    最初の違反: ([0], 0, '変量 hi - lo が減り、負にならない')

読み取れることが 3 つあります。

1. 誤った実装でも、$140$ 個のうち $87$ 個の入力では、どの表明も落ちません。 たとえば $x$ が配列のどの要素よりも大きい入力では、誤った枝を一度も通りません。入力の選び方しだいで、誤りは見えないままです。
2. 表明を外して返り値だけを正解と比べると、返り値が誤るのは $140$ 個のうち $15$ 個です（表明なしの版を別に実行して数えました。たとえば $a = [0, 1]$、$x = 1$ で、正しい答え $1$ に対して $0$ を返します）。残りの $38$ 個は、途中で $hi \lt lo$ という「あってはならない状態」を通るのに、返り値は偶然正しい入力です。途中の表明は、最終結果に現れない誤りも捕まえます。 次章で、これを「感染したが伝播しなかった」誤りと呼びます。
3. 最初に落ちるのは長さ $1$ の配列です。$a = [0]$、$x = 0$ で $mid = 0$、$hi = -1$ となり、変量が負になります。小さい入力を系統的に試すことの効き目が分かります。

命題 8.2（契約の検査の限界）✓

1. （実行時検査）仕様 $(D, S)$ と実装 $f$（定義 2.1）に対し、違反入力の集合を $V = \{x \in D \mid f(x) \text{ が定まらないか、} (x, f(x)) \notin S\}$ とする。$f$ が仕様を満たすことは $V = \emptyset$ と同値である。有限集合 $T \subseteq D$ の各入力で $f$ を実行し、止まった結果について $(x, f(x)) \in S$ を検査する実行時検査は、$T \cap V = \emptyset$ のとき違反を 1 つも報告しない。$V \ne \emptyset$ であっても同じである。
2. （静的な判定）$\mathcal{L}$ をチューリング完全なプログラミング言語とする。$\mathcal{L}$ のプログラム $c$ について、三つ組 $\{\mathrm{true}\}\ c\ \{\mathrm{false}\}$ が部分正当であるかどうか（すなわち、$c$ がどの入力でも停止しないかどうか）は決定可能でない。したがって、プログラムと契約 $(P, Q)$ から $\{P\}\ c\ \{Q\}$ の部分正当性を判定するアルゴリズムは存在せず、「受理したものは必ず部分正当」である決定可能な検証器は、部分正当なのに受理しない三つ組を必ずもつ。

証明（命題 8.2）

(1) $f$ が仕様を満たすとは、すべての $x \in D$ で $f(x)$ が定まり $(x, f(x)) \in S$ となることで、これは $V$ に元が無いことです。実行時検査が違反を報告するのは、ある $x \in T$ で $f(x)$ が定まり $(x, f(x)) \notin S$ のときだけで、そのような $x$ は $T \cap V$ に属します。$T \cap V = \emptyset$ ならば報告はありません。この議論は $V$ が空かどうかを使っていません。

(2) 部分正当性の定義（定義 3.3）から、$\{\mathrm{true}\}\ c\ \{\mathrm{false}\}$ が部分正当であることは、「どの状態 $\sigma$ からも、$c$ が停止して至る状態 $\sigma'$ が無い」こと、すなわち $c$ がどの状態からも停止しないことと同値です（$\mathrm{false}$ を満たす $\sigma'$ は無いので）。

停止問題の集合 $K$（定義 7.1［計算可能性］）の元かどうかを判定したい番号 $e$ が与えられたとします。$\mathcal{L}$ はチューリング完全なので、入力を無視して「機械 $M_e$ を入力 $e$ で模倣し、模倣が止まったら自分も止まる」プログラム $c_e$ を、$e$ から機械的に作れます。これは健全な静的検査の不完全性（定理 5.6［プログラミング言語論］）の証明で使われたのと同じ構成です。$c_e$ は、$e \in K$ ならどの状態からも停止し、$e \notin K$ ならどの状態からも停止しません。よって

$$\{\mathrm{true}\}\ c_e\ \{\mathrm{false}\} \text{ が部分正当} \iff e \notin K$$

です。左辺を判定するアルゴリズムがあれば、$e$ から $c_e$ を作ってそれに渡し、答えを反転することで $K$ を判定できます。これは $K$ が決定可能でないこと（定理 7.2［計算可能性］）に反します。

後半。$(P, Q) = (\mathrm{true}, \mathrm{false})$ の場合がすでに判定できないので、一般の契約についても判定できません。検証器が受理する三つ組の集合 $C$ が決定可能で、部分正当な三つ組の集合 $V'$ に含まれるとします。$C = V'$ なら $V'$ が決定可能になって矛盾するので、$C \subsetneq V'$ です。

∎

(1) は当たり前の主張ですが、次章の出発点です。テストで分かるのは $T \cap V$ が空かどうかだけで、知りたいのは $V$ が空かどうかです。両者の差を埋める方法は 2 つあります。1 つは、$T$ を $V$ に当たりやすいように選ぶこと（テストの設計。次章と次々章）。もう 1 つは、$V = \emptyset$ をすべての入力について証明すること（この章の Hoare 論理）。(2) は後者に機械的な近道がないことを言っています。それでも、例 3.10 のように人が不変条件を与えれば、残りの検証条件の多くは機械で確かめられます。決定不能性は「どんなプログラムにも通用する全自動の方法はない」と言っているだけで、目の前の 1 つのプログラムを証明できないとは言っていません。

注意 8.3（この記事で扱わなかったこと）

言語 W にはポインタも並行性もありません。ヒープ上のデータ構造と別名を扱うには、表明に「ヒープのこの部分とあの部分は重ならない」と書ける分離論理（J. Reynolds、P. O’Hearn ら）が使われ、例 6.3 のような別名の問題を論理の中で扱えます。並行プログラムでは、ほかのスレッドが途中で状態を変えるので、表明が「ほかのスレッドの動作で壊れない」ことの検査（Owicki–Gries の方法、依存・保証による推論）が加わります。抽象仕様から実装を段階的に導く精密化計算（R.-J. Back、C. Morgan）は、命題 6.4 の考え方を開発の手順にしたものです。いずれも、この記事の「意味論を定め、規則の健全性を証明する」という枠組みの延長にあります。

9. 演習

演習 9.1易

$A, B$ を整数の定数とする。命令 $c$ を $x := x + y;\ y := x - y;\ x := x - y$ とするとき、$\mathrm{wlp}(c,\ x = A \wedge y = B)$ を 定理 4.2 (5) の計算規則で求めよ。この命令は何をしているか。

解答

後ろから順に代入します。$Q_0$ を $x = A \wedge y = B$ とします。

• $x := x - y$ について: $Q_1 = Q_0[x - y/x] = (x - y = A \wedge y = B)$。
• $y := x - y$ について: $Q_2 = Q_1[x - y/y] = (x - (x - y) = A \wedge x - y = B) = (y = A \wedge x - y = B)$。
• $x := x + y$ について: $Q_3 = Q_2[x + y/x] = (y = A \wedge (x + y) - y = B) = (y = A \wedge x = B)$。

逐次の規則から $\mathrm{wlp}(c, Q_0) = Q_3 = (x = B \wedge y = A)$ です。実行前に $x = B$、$y = A$ なら実行後に $x = A$、$y = B$ なので、$c$ は補助変数を使わずに $x$ と $y$ の値を入れ替えています。言語 W の整数は範囲が無限なので正しいのですが、有限の整数型では $x + y$ が範囲を超える場合があり、例 5.4 と同じ注意が要ります。

演習 9.2標準

$X \ge 0$、$Y \gt 0$ を整数の定数とする。次のプログラムについて、事後条件 $X = q \times Y + r \wedge 0 \le r \lt Y$ を導くループ不変条件と、停止性を示すループ変量を与え、条件を確かめよ。

$$q := 0;\ r := X;\ \mathtt{while}\ Y \le r\ \mathtt{do}\ (r := r - Y;\ q := q + 1)$$

解答

不変条件を $I$: $X = q \times Y + r \wedge r \ge 0$ とします。

初期化。 $(I[X/r])[0/q]$ は $X = 0 \times Y + X \wedge X \ge 0$ で、$X \ge 0$ から成り立ちます。

保存。 $\mathrm{wlp}(r := r - Y;\ q := q + 1,\ I)$ は、まず $I[q + 1/q] = (X = (q + 1) Y + r \wedge r \ge 0)$、次に $r$ を $r - Y$ に置き換えて $X = (q + 1) Y + (r - Y) \wedge r - Y \ge 0$、すなわち $X = qY + r \wedge r \ge Y$ です。これは $I \wedge Y \le r$ から従います。

終了時。 $I \wedge \lnot(Y \le r)$ は $X = qY + r \wedge 0 \le r \lt Y$ で、求める事後条件そのものです。定理 3.8 により部分正当です。

変量。 $v = r$ とします。$I \wedge Y \le r$ のもとで $r \ge Y \gt 0$ なので $v \ge 0$。本体は代入 2 つなので停止し、$I$ を保ち、$r$ は $Y \ge 1$ だけ減るので $v$ は真に減ります。定理 5.2 より、プログラムは全正当です。$Y \gt 0$ を仮定から外すと、$Y = 0$ のとき $v$ が減らず、実際にループは止まりません。

演習 9.3標準

$w = \mathtt{while}\ b\ \mathtt{do}\ c$ とする。任意の表明 $Q$ について

$$\mathrm{wlp}(w, Q) = \bigl(b \wedge \mathrm{wlp}(c, \mathrm{wlp}(w, Q))\bigr) \vee \bigl(\lnot b \wedge Q\bigr)$$

が成り立つことを示せ。

解答

$\sigma$ を状態とします。

$\llbracket b \rrbracket\sigma = \mathrm{ff}$ のとき。$w$ の実行の導出は (WhF) でしか終われないので、$\langle w, \sigma \rangle \Downarrow \sigma'$ は $\sigma' = \sigma$ と同値です。よって $\sigma \in \mathrm{wlp}(w, Q)$ は $Q(\sigma)$ と同値で、右辺に属すること（$b$ の側は成り立たないので $Q(\sigma)$）と一致します。

$\llbracket b \rrbracket\sigma = \mathrm{tt}$ のとき。$w$ の実行の導出は (WhT) でしか終われないので、$\langle w, \sigma \rangle \Downarrow \sigma'$ は「$\langle c, \sigma \rangle \Downarrow \sigma_1$ かつ $\langle w, \sigma_1 \rangle \Downarrow \sigma'$ となる $\sigma_1$ がある」ことと同値です。これは $\langle c; w, \sigma \rangle \Downarrow \sigma'$ と同じ条件なので、$\sigma \in \mathrm{wlp}(w, Q)$ は $\sigma \in \mathrm{wlp}(c; w, Q)$ と同値で、定理 4.2 (5) の逐次の規則により $\sigma \in \mathrm{wlp}(c, \mathrm{wlp}(w, Q))$ と同値です。右辺に属することもこれと一致します。

この等式は $\mathrm{wlp}(w, Q)$ を自分自身で表しているので、計算規則にはなりません。ループ不変条件 $I$ は、この方程式の解の代わりに人が与える「$I \wedge b \Rightarrow \mathrm{wlp}(c, I)$ かつ $I \wedge \lnot b \Rightarrow Q$」を満たす表明です。

演習 9.4標準

口座の操作 withdraw(n) の上位型の契約を、実行前の残高 $b_0$ ごとに「事前条件 $0 \lt n \le b_0 \wedge \mathit{balance} = b_0$、事後条件 $\mathit{balance} = b_0 - n$」とする。次の 3 つの下位型のうち、振る舞いの部分型（定義 7.1）であるものはどれか。そうでないものについては、上位型の契約を守っているのに困る呼び出し側を挙げよ。

• (a) 事前条件 $0 \lt n \le b_0 + 100 \wedge \mathit{balance} = b_0$、事後条件 $\mathit{balance} = b_0 - n$（$100$ まで貸し越せる）。
• (b) 事前条件 $0 \lt n \le b_0 \wedge n \le 1000 \wedge \mathit{balance} = b_0$、事後条件 $\mathit{balance} = b_0 - n$（1 回の上限つき）。
• (c) 事前条件は上位型と同じ、事後条件 $\mathit{balance} = b_0 - n - 1$（手数料 $1$ を引く）。

解答

(a) は振る舞いの部分型です。$0 \lt n \le b_0$ ならば $0 \lt n \le b_0 + 100$ なので $P \Rightarrow P'$、事後条件は同じなので $Q' \Rightarrow Q$ です。定理 7.2 により、上位型の契約で証明された呼び出し側はそのまま正しい。上位型の事前条件を守る呼び出し側は貸し越しを起こさないので、追加された動作に出会いません。

(b) は部分型ではありません。$b_0 = 5000$、$n = 2000$ は $P$ を満たし $P'$ を満たさないので、$P \Rightarrow P'$ が破れます。残高の範囲内で $2000$ を引き出す呼び出し側は、上位型の契約を守っているのに、下位型では事前条件違反になります。

(c) も部分型ではありません。$Q'$ を満たす状態は $\mathit{balance} = b_0 - n - 1$ で、$Q$（$\mathit{balance} = b_0 - n$）を満たさないので、$Q' \Rightarrow Q$ が破れます。「残高をちょうど $0$ にするために withdraw(balance) を呼ぶ」呼び出し側は、実行後の残高が $-1$ になります。そもそも $n = b_0$ は事前条件を満たすので、(c) は残高が負にならないという不変条件があればそれも破ります。

参考文献

1. C. A. R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM 12 (1969), 576–580. doi:10.1145/363235.363259 — 三つ組と推論規則の原論文。
2. E. W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976 — 最弱事前条件によるプログラムの意味づけと、不変条件・変量からのプログラムの導出。
3. G. Winskel, The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993 — 第 2 章（操作的意味論）、第 6 章（Hoare 規則と健全性）、第 7 章（相対完全性）。
4. B. Meyer, Object-Oriented Software Construction, 2nd ed., Prentice Hall, 1997 — 第 11 章（契約による設計）。
5. B. H. Liskov, J. M. Wing, “A behavioral notion of subtyping”, ACM Transactions on Programming Languages and Systems 16 (1994), 1811–1841. doi:10.1145/197320.197383 — 振る舞いの部分型の定式化。
6. C. A. R. Hoare, “Proof of correctness of data representations”, Acta Informatica 1 (1972), 271–281 — 表現不変条件と抽象化関数。
7. S. A. Cook, “Soundness and completeness of an axiom system for program verification”, SIAM Journal on Computing 7 (1978), 70–90 — 相対完全性。