このサンプルは TDDBC Online 2020 #1 のお題「整数の閉区間」を証明駆動開発（Proof Driven Development; PDD）で解いたものです。
現実的な開発でも TDD などのテスト技術に加えて、これから説明をする証明もできる方がより開発を効率化できることが多くあります。 ここでは TDD の一歩先として証明の雰囲気を伝えるために同じお題で PDD をやっています。
知識はいつかつながると思っているので、今は消化不良でも「そういえば証明とか聞いたことあったな」だけ覚えていただければ嬉しいです！
この例では、TDDBC のお題を「証明」駆動で開発しています。この「証明」は数学的な証明のことですが、実はこの証明は TDD のテストと似たことをできます。
TDD のテストは具体的なプログラムの入出力を比較するものでしたが、PDD では抽象的なプログラムの入出力を証明によって比較します：
| テストの形式 | 例 | |
|---|---|---|
| TDD のテスト | 具体的な入力値に対する具体的な出力値を検証する | add(1, 2) == 3 |
| PDD の証明 | 抽象的な入力値に対する抽象的な出力値を検証する | ∀x y. add x y = add y x （意味: どんな x y でも、add x y と引数をひっくり返した結果は一致する） |
前表のとおり、証明では入出力をいずれも抽象的にできるのが特徴です。抽象的であるメリットは「どんな入力値でも出力値はこうなる」というようにありえるすべての入出力を検証できることです（TDD のテストでは入力値すべての検証をできない）。
ただの足し算ではこのような入力値の網羅は必要ないと感じると思いますが、現実的なアプリケーションでも単体レベルを離れて結合レベルからみてみると入力値の組み合わせが天文学的な数になりがちです（下図は結合後の状態遷移図の例でこの経路の数だけ入力がある）：
しかし、TDD ではこの数すべてをテストしようとはしません（できません）。そこで同値分割・境界値分析を使って代表値だけをテストしているわけです。しかし結合レベルでは同値クラスや境界値を見誤ることが多く、バグを見逃しがちです。こう考えてみると、TDD では結合レベルでの設計の誤りは遅れて発見される運命ということでしょう。
しかし、この部分は証明によって補えるのです！
証明ではどんなに入力値の数があろうとも、論理的な推論「こういう入力でこの処理を経たならばこういう出力にしかならない」の連続によって出力を保証できます。このモチベーションの話は「自動テストに限界を感じた私がなぜ形式手法に魅了されたのか」に詳細に書いたので、ぜひ読んでみてください。
では、実際に証明の雰囲気をみていきましょう！
証明駆動開発のファイルは Range.thy に書いてあります。お題の記述のどこがどの部分に対応するのかをわかりやすくするため、以下のように仕様を分割して ID を振っています。
| 仕様番号 | 実装状況 | 仕様 |
|---|---|---|
| NLS-1 | X | 整数閉区間を示すクラス（あるいは構造体）をつくりたい。 |
| NLS-2 | X | 整数閉区間オブジェクトは下端点と上端点を持ち、 |
| NLS-3 | X | 文字列表現も返せる |
| NLS-4 | X | （例: 下端点 3, 上端点 8 の整数閉区間の文字列表記は "[3,8]"）。 |
| NLS-5 | X | ただし、上端点より下端点が大きい閉区間を作ることはできない。 |
| NLS-6 | X | 整数の閉区間は指定した整数を含むかどうかを判定できる。 |
| NLS-7 | X | また、別の閉区間と等価かどうかや、 |
| NLS-8 | X | 完全に含まれるかどうかも判定できる。 |
| NLS-9 | X | 例: 閉区間 [3,8] の場合[3,8] |
| NLS-10 | X | → 下端点 (lower endpoint) が 3 , 上端点 (upper endpoint) が 8 である整数閉区間 |
| NLS-11 | X | → 3 と 8 は区間に含まれる |
| NLS-12 | X | → つまり (整数閉区間だから) 3,4,5,6,7,8 |
NLS-12 の解釈を何も考えずに書いてあるとおり「集合 { 3, 4, 5, 6, 7, 8 } の要素を n とし、すべての要素について in_range n (3, 8) が真である」と解釈すると、実は雑な定義 in_range _ = True （どんな自然数でも真とする）で成立してしまう。
(* どんな自然数でも真とする FakeIt な関数 *)
fun in_range :: "int ⇒ (int × int) ⇒ bool" where
"in_range _ = True"
(* 集合 { 3, 4, 5, 6, 7, 8 } の要素を n とし、すべての要素について in_range n (3, 8) が真になることを証明する *)
example_3_8_strong: "∀n ∈ { 3, 4, 5, 6, 7, 8 }. in_range2 n (3, 8)"
apply(auto)
(* このときの証明の状態:
goal:
No subgoals!
FakeIt なのに証明が成功してしまった…
*)どうしてこんなことになるかというと、NLS-12 には 3, 4, 5, 6, 7, 8 で以外について明示的に仕様が書かれていないから。
一般に、明示的に仕様が書かれていない場合次の2つの場合がありうる：
- 未定義: どんな結果になってもいい
- 定義の書き漏れ: 実際には期待されている定義が存在するが、暗黙になってしまっている
今回のケースでは前者として解釈（つまり 3-8 以外ではどんな結果でもいい）としてしまうと、実装側はすべて真としてしまっても仕様を満たしていることになる。しかし、常識的にはすべてを真という関数が無益であるので変だと気づいて、後者の解釈（なんらかの結果が期待されている）で読まないといけない。
要するに、NLS-12 を読む際には心の中で「それ以外は False」と付け加えないといけない。このように NLS-12 を解釈して論理式に落とせれば雑な定義の証明は成功しない。
(* 自然数 n について、n が集合 { 3, 4, 5, 6, 7, 8 } の要素のときのみ in_range n (3, 8) が真になり、
そうでなければ in_range n (3, 8) は偽になることを証明する *)
theorem "∀n. n ∈ { 3, 4, 5, 6, 7, 8 } ⟷ in_range2 n (3, 8)"
apply(auto)
(* このときの証明の状態:
goal (1 subgoal):
1. ⋀n. ⟦n ≠ 3; n ≠ 4; n ≠ 5; n ≠ 6; n ≠ 8⟧ ⟹ n = 7
どんな自然数 n でも n が 3, 4, 5, 6, 8 のいずれでもないなら、n が 7 になることを証明しないといけない。
もちろん、そんなことは証明できないのでこの辺りで FakeIt 直し忘れてたと気づく。
ただし、もし in_range の定義域が自然数全体ではなく 3-8 だけだったならば、
3-8 以外のケースはないと言えるので証明できるという意味でもある。
*)