帰納関数はなぜ安全か？ -- 帰納的テストに関する考察

ソフトウェアのテスト技法は数学の証明でたとえるなら、場合わけをして、各ケースを証明することに相当する。例えば、マトリックスを書いてテストをするなんていうのは典型的な例で、実際にはすべての例を挙げることはできないので、できるだけ重要なケースを網羅することがテストでは重要になる。
でも数学では場合わけ以外にも証明方法はあるわけで、例えば帰納法はソフトウェアテストに使えないだろうか?

とりあえず、関数レベルのテストで考えてみよう。
イメージ的にはある限界値入力（n = 0など）のケースを実際にテストした上で、 n = a で正しいと仮定したときに n = a + 1 で正しいことを証明すれば「すべての入力に対して動作が正しい」と証明したことになる。全入力値に対してテストするexhaustive testと同じことが1ケースのテスト＋αで終わることになる。

でももちろん「α」がむちゃくちゃ難しいわけで、とりあえず挙げてみても次の３つの問題がある。
1. 入力を整数にマッピングできるのか？
2. 入力の次元が高いときは？
3. n = aで正しいときに n = a + 1 で正しいことを証明する方法は？

1番目はそういう関数でないと、ダメなんでしょうな。
2番目は私の数学の素養がないので、実際どうなのかよくわからない。
3番目はそれこそ実際にテストではできないので、静的解析に頼れれば、と思うのだけど、「普通の関数」は、明示的に n = a + 1 の動作が n = a の動作に依存しているわけではないので、一般的には無理な感じ。

唯一の例外は再帰関数。こいつは入力 n = a に対する動作が、別の値の入力に直接依存しているので帰納的なソフトウェアテストができる可能が高い。
そもそも、再帰関数をコードレビューすると、自然と帰納法の証明と同じことをやっていることになる。そう考えると再帰関数って言うのは慣れていないと分かりにくいけど数学的に正しさを証明しやすい貴重な書き方なのかもしれない。

ただ、繰り返しを再帰に変換することは可能だし、もしかしたら一般的な関数の正しさを証明できたりするのかもしれない。
賢い静的解析ツールなら、関数を等価な再帰関数に変換して正しさを解析できるかもしれない。
ただ、私が思いつくぐらいなので、すでに研究されているだろうし、それでも静的解析のツールで「正しさを証明します」なんて話を聞いたことはないのでやっぱり無理なんだろうなぁ。