契約の検査の限界

命題 8.2（「契約による設計」§8）・ ✓公理まで証明済み

（実行時検査）仕様 $(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$ であっても同じである。
（静的な判定） $\mathcal{L}$ をチューリング完全なプログラミング言語とする。 $\mathcal{L}$ のプログラム $c$ について、三つ組 $\{\mathrm{true}\}\ c\ \{\mathrm{false}\}$ が部分正当であるかどうか（すなわち、 $c$ がどの入力でも停止しないかどうか）は決定可能でない。したがって、プログラムと契約 $(P, Q)$ から $\{P\}\ c\ \{Q\}$ の部分正当性を判定するアルゴリズムは存在せず、「受理したものは必ず部分正当」である決定可能な検証器は、部分正当なのに受理しない三つ組を必ずもつ。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 9 件、定義なども含めて 12 件）。

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

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

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