日本的なモデル検査・・・？
本日の懇親会で。某大手製造業の人と雑談していて出た話。最近、ヨーロッパを中心に、ソフトウェアの安全性と品質の保証ため、形式的手法による検証が実際のシステム設計現場などでも使われつつあります。では、なぜ日本ではそれが定着しないのか。
日本の「ものづくり」のスタイルは、例えば自動車業界なんかが典型的ですが、製造現場の創意工夫を最大限に生かすべく、現場レベルの裁量をなるべく大きくする*1、というボトムアップ型の構造が特色だ、と言われています。一方、システム検証は、まず上流工程で形式言語で書かれた仕様書を作る*2ことでしっかりとした骨組みを定め、あとはそれを逸脱しないように下流工程で肉付けをしていく、というトップダウン的な構造に特色があります（もちろん、普通にプログラムをしてからそのコードの検証作業をするのでもいいんですが、それには限界があり、やはり最初の段階から形式手法を使うべきだと思います）。
現在のところ、ボトムアップのやり方はソフトウェアにはなじまないと思われます。下流工程で「カイゼン」しようとして、例えば変数やメモリーの使い方を少しいじったら、全体に大きなエラーをもたらす、なんて良くある話です。例えると、論理体系で、例えばBanach-Tarskiの逆理が気に食わないからと選択公理を排除したら、Zornの補題も断念しなければならなくなったようなものでしょうか。
結局のところ問題は、トップダウン的なやり方は製造現場の文化になじまないが、一方現場の小規模なカイゼンが全体に問題を及ぼすことがないことを保証するためには、トップダウンな形式的手法を最初から採用していることが必要になる、という構造のようにも思えます。日本的なボトムアップなアプローチにふさわしい、ボトムアップベースで現場のある箇所のカイゼンが別の場所で問題を起こさないことだけを教えてくれるような検証技術は存在するのか？あればいいんですけれど、どうなんでしょうか。
