検証と確信

「いやあ,そう思って,最新の検証技術であるところの MacroSoft Visual ProofSafe を使って仕様との適合性チェックを行っているんですよ。最新のソリューションが正しさを保証してくれるんですよ」

Visual ProofSafewww

こういうやつでしょうか。

「本当の仕様」と「プログラム」が一致しているか確認する方法は、二つあって、一つ目は実際にプログラムを作ってみて動かしてみる方法。これはみんなが大好きなアジャイルっていうやつだよね。これの問題は、実際に動かしてみてダメだったらとんでもないことになる場合は、この方法を採用できないこと。原発とかミサイルとか。

もう一つは、プログラムよりは読み易い仕様を作って、その仕様から正しいプログラムを生成するプログラムも作って、その仕様が本当の仕様と一致しているか確認する方法。例えば「Isabelleが読める仕様を書いて、そこからプログラムを自動で生成する」みたいな話。

後者の方法における問題は、プログラムよりは読み易い、とは言っても、やっぱり仕様を読み書きできる人間は限られることと、仕様から正しいプログラムを生成するプログラムが正しいことをどうやって保証するのかということ。まあ、後者の問題は、通常仕様から正しいプログラムが生成できることは、テストすればそれで良いんだからあんまり問題にならないような気がする。