以前、完全なテストは不可能だ という稿を書いたのですが、これに対して 反論しているページ を見つけたので考察しておきます。

反論の骨子

該当ページの文章が短いので全文引用となってしまいますが、法的な引用の要件を満たせると思うので引用します。

思うに、それは論理学でいうところの帰納法で解決できるのではなかろうか。

完全なテストは不可能だ:
さて、プログラムの話に戻ります。intの引数を2個とる場合、その組み合わせは1600京ほどに なるということを先の稿で述べました。 そして、バグが「ある」ことを証明する場合、バグの例をひとつ探し出せばよいのに対し、 バグが「ない」ことを証明するにはこの1600京のパターンすべてを網羅して検査し、 全て正常に動いたということを提示しなければなりません。

数学でも、全ての数を計算したわけではないのに成立している定理は山ほどある。というかそうでないものの方が少ないはず。

悪魔の証明、という目の付けどころは悪くないのに。まあ、ちょと前に自分でも取り上げたわけだが。

つまり、帰納法を用いることで全てを演算することなく正しさを証明できるのではないか？という主張ですね。

帰納法とは何か？

まず帰納法とはなんでしょうか。概要を知るにはwikipediaがてっとり早いので該当項目を見て見ましょう。

http://ja.wikipedia.org/wiki/%E5%B8%B0%E7%B4%8D

帰納（きのう、Induction）法とは、個別的・特殊的な事例から一般的・普遍的な規則を見出そうとする推論方法のこと。対義語は演繹法。演繹においては前提が真であれば結論も必然的に真であるが、帰納においては前提が真であるからといって結論が真であることは保証されない。

帰納法は真実を得られません。一部の事例から、全体を推論するのですが、論理の飛躍が含まれます。
例えば、intを引数にとるメソッドに対し、-1,0,1の３つの値を入れた際にうまく動いたからといって、 すべての値に対して正しく動作するとは言えませんよね。

帰納法とは3つうまくいったんだから、全部の値でうまくいくはずだという推論ですから、 帰納法を用いてメソッドの完全性を求めることはできません。

数学的帰納法という名の演繹法

「数学でも、全ての数を計算したわけではないのに成立している定理は山ほどある。」と述べていることから、 「帰納法」といっているのは多分、数学的帰納法のことを指しているのではないかと思われます。

さて、数学的帰納法というのは帰納法という名が付いていますが、実際には演繹法（えんえきほう）です。

http://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E7%9A%84%E5%B8%B0%E7%B4%8D%E6%B3%95

数学的帰納法（すうがくてききのうほう）とは、有限回の議論で可算無限個の対象に対する命題を証明するための数学の論法である。次のような手順で自然数全体に関する命題 P(n) (n∈N) が真であることを証明する論法である。

1. P(0) は真である。
2. 任意の自然数 k に対し，P(k) が真であれば，P(k+1) も真である。

よって任意の自然数 n について P(n) は真である。

イメージとしては、2 により次々と次の命題の正しさが伝播されていくことになる。つまり、1 によりまず P(0) は正しく、P(0) と 2 により P(1) は正しく、P(1) と 2 により P(2) は正しく、以下これが果てしなく続いていく。このことによって任意の自然数 n について P(n) が正しいことが保証される。

なお、数学的「帰納法」という名前がつけられているが、数学的帰納法の解法プロセス自体は帰納法ではなく演繹法である。先に述べた、「2 により次々と次の命題の正しさが伝播されてい」った結果証明されていく様子が帰納のように見えるためつけられたにすぎない。

これは、学校で習いましたよね。
数学的帰納法はドミノ倒しに似ています。

• あるドミノが倒れたら、次のドミノが倒れるようにしておく
• 最初のドミノを倒す

このふたつがポイントです。ドミノを倒すことで全ての数を計算するのです。
ですから、「数学でも、全ての数を計算したわけではないのに成立している定理は山ほどある」というのは 多分に誤解を含んでいます。数学的帰納法に拠らない証明で成立している定理もありますが、 数学的帰納法で証明されている定理に関して言えば全てを計算しているのです。

ドミノが勝手に倒れてくれるので準備を整えたら無限のかなたまで手間無く一瞬で計算できるだけのことです。

テストに数学的帰納法を適用するには

ブラックボックステストで数学的帰納法を扱う術はありません。 あるドミノが倒れたら次のドミノも倒れるという証明ができないからです。
ブラックボックステストでは実行した結果を仕様と照らし合わせて等しいかみる必要があります。 実行せずに正しい答えを返すことを証明することは不可能です。

となれば、ホワイトボックステスト的な手法をとらざるを得ません。 それはもはや、プログラムのコードが正しく機能することを数学的に証明を導くことに等しい重労働です。

このようなアプローチは 形式的検証 と呼ばれています。

このアプローチでプログラムの完全な正しさを証明しようとするのであれば、 数学者を大量に雇いいれ、幾千もあるメソッドに対してそれぞれ独自の証明を人力で解いていかないといけません。 複雑なメソッドの正しさを数学的に証明しようとした場合、それは世紀の難問にも等しい難度を誇ることでしょう。

指摘もとのblogの言葉を借りるならば「帰納法、という目の付けどころは悪くないのに。」といったところでしょうか。