形式手法の未来

形式手法と漠然と呼ばれているソフトウェア開発手法があって、それなりに盛り上がったり盛り上がらなかったりしている訳だけど、その未来は明るいのだろうか。少し考えてみたい。

まず形式手法として最近主にネットで少し盛り上がっているのが定理証明支援系、例えばCoqやAgdaを使った開発だと思う。で、こういった手法に未来はあるだろうか。大方の見方に反して、私は無いと思う。まあこれは私が習得することが出来なかったという面もあるかもしれないけど、それだけじゃなくて、定理証明支援系自体の問題もあると思う。

定理証明支援系の問題は、まずとにかく使いこなすのが難しいこと。それからたとえ使えても証明を手作業でするので時間がかかること。短期間、少ないコストでソフトウェアを開発することが要求されている今のソフトウェア開発の現場に導入するのは無理だと思う。定理証明支援系を使って開発しても、仕様自体にバグがある可能性があるからバグはゼロにはならないし、正しさの証明ができるといっても、ほとんどのエンジニアは証明とはなにか理解できていないので、結局、現場には定理証明支援系の良さは理解されないだろう。

定理証明支援系の問題はもうひとつ有って、それは他の手法の問題点でもあるのだけど、仕様やプログラムを独自の記述言語で表現すること。これらの言語で完全に閉じた開発が出来ればいいのだろうけど、例えばCoqが生成したOCamlコードは遅すぎて実用に供するには手を加える必要があったりするように、他の言語への変換が発生するのが普通だと思う。そうすると、その変換をどう正当化するのかという問題が生ずる。OCamlとか実際に使われている言語でかかれたプログラムをそのままの形でそれについて推論できるくらいになってほしい。

さて、では定理証明支援系と並んで重要な形式手法であるモデル検査はどうかというと、これも微妙な気がする。少なくとも現在使われているSpinやSMVは上の定理証明支援系と同じく翻訳の問題がある。非形式的な言語から形式的な言語への翻訳を完全に正当化するのは不可能だし、不完全な正当化をするにしても、例えば自然言語で書かれた仕様書からPromelaのコードに落とすとことを考えると、その落とす過程を文書化する必要がある。たとえば仕様書を分析して流れ図を書いたりと、ペーパーワークを沢山する必要があって、何だかなあという気がしてしまう。


なので、これからの方向性としては、独自言語ではなく実際に現場で使われている仕様記述言語（UMLとか）を直接検証できるといいような気がする。まあfUMLを検証する話とか、あるみたいだし。

それ以外の形式手法についてだが、まずAlloyのことはよく知らないのでコメントできない。ただ、やはり独自の言語を持っているということで、上に挙げた翻訳の問題はあるんじゃないかと思う。

それから、メモリ操作を含むプログラムのseparation logicを使った検証という話がある。定理証明支援系ｎ上にseparation logicを実装する話もあるけれど、私が面白いと思っているのがJavaやCのソースコードの自動検証を行うもの。オープンソースだとjStar,プロプライエタリだとinferがある。私は触ったことが無いので具体的にはコメントできないけど、形式手法の将来としては、これらのツールが目指しているようなソースコードの自動検証になるのかもしれない。