形式手法とアジャイル - masateruk’s blog

　私は形式手法にはソフトウェアの品質を高める力があると信じている。一方、プロジェクトの進め方に関して言えばアジャイルのようなやり方が有効だと思っている。しかし、私が形式手法とアジャイルの両方に興味を持つ事に関して、そういう人は珍しいと言う意見を何度か耳にした。どうもアジャイルと形式手法が相容れないと考える人が多いようである。その気持ちは何となく分かるが、私としては両立すると思っているので、今日はその事を書きたい。

私の主張は以下の通りである。

アジャイルなプロジェクトで形式手法を活用する事ができる。

それに対して、よく（？）聞かれる反対意見は以下のようなものである。

アジャイルなプロジェクトでは、前払いの設計を行わない。形式手法を適応する場はないのではないか？
設計で形式手法を使った場合通常より時間がかかるのではないか？その結果、開発の速度を落とすのでは？
テスト駆動開発で開発しているから検証は十分ではないか？
形式手法のツールを使いこなすのが難しい。学習に時間がかかる。
証明までしなくても良いのでは？過剰品質では？

以下、それぞれの反対意見に反論してみよう。

1. アジャイルなプロジェクトでは、前払いの設計を行わない。形式手法を適応する場はないのではないか？
　「アジャイルなプロジェクトでは、前払いの設計を行わない」と言われているが、まったく設計を行わないわけではない。確かに設計書とかアーキテクチャ説明書のような文書は作らないかもしれないが、プログラマが実装する（まさにソースコードを編集する）前には頭の中で設計という行為が行われている。そこでは、メソッドや変数の名前を決めたり、クラス間の関係を考えたり、クラスの状態遷移を思い浮かべシミュレーションしたりする。これらはその結果を文書の形で残さなくても立派な設計行為である。そして、この設計した結果を検証するのに形式手法を用いる事ができる。特に振る舞いを検証するときには形式手法のツールが役に立つだろう。

2. 設計で形式手法を使った場合通常より時間がかかるのではないか？その結果、開発の速度を落とすのでは？
　確かに設計に費やす時間が増える可能性はある。しかし、仮に設計に多くの時間がかかったとしても従来のやり方では設計段階で見つけられなかった不具合を見つける事ができれば、デバッグと修正にかかる時間が削減できるためトータルでは時間を短くすることができる。形式手法やツールについて不慣れなうちは設計にかかる時間が従来に比べてかなり多くなるだろうが、それは経験を重ねることによって徐々に改善される。私は何度か実プロジェクトでモデル検査を使用した事があるが、以前マルチスレッドのライブラリにおける関数呼び出しとコールバックについてデッドロックが起きないかをSPINで検証したときは、スクラッチからモデルをつくって検証を終えるのに約1時間であった。同じことをテストでやったとしても同程度の時間がかかるのではないかと思う。しかもテストではなかなか網羅的にテストすることは難しいが、モデル検査ならば全ケースを網羅的に調べてくれる。

3. テスト駆動開発で開発しているから検証は十分ではないか？
　十分ではない（ことがある）。理由は、網羅的にテストをすることは（主に時間の都合で）難しく、その結果不具合を見逃す事があるからである。テスト駆動開発で書かれるテストは決して十分ではない。テスト駆動開発のテストは単体テストとは異なり、網羅して不具合を出し切ることが目的ではなく、実装にあたり大きな考え違いはないかを見つけたり、使用者にとって使いやすい仕様になっているか確認したり、そして実装者に少しだけの自信を与えるたりするものである。検証という点では十分とは言いがたい。

4. 形式手法のツールを使いこなすのが難しい。学習に時間がかかる。
　確かにそういう点はある。しかし、先日IPAで開催されたVDMのセミナーによると一週間の教育期間をもうければ、あとはエキスパートの助言を受けながら開発をすることはできるという。そのセミナーでも言われていたのだが、自分のものにするには教科書の問題である程度練習したら、実践することが一番である。実際のプロジェクトで頭をフル回転させながら挑めば、あっという間に上達するだろう。そして上達した暁には、以前より正確なプログラムを速く開発できるようになる。ということでこの意見に対しては、最初は時間はかかるだろうけど、そのうち学習時間を取り消すくらいの効果がある。というのが私の意見である。

5. 証明までしなくても良いのでは？過剰品質では？
　確かにプログラムの正当性を証明するとなるとツールのサポートがあったとしても時間がかかるだろう。そしてその時間と結果として担保される品質を天秤にかけたとき、過剰品質となる場合はある。しかし、形式手法だからといって必ずプログラムの正当性を証明しないといけない訳ではない。たとえば、モデル検査は有限の状態空間がある性質を保持するかを検査する方法で、証明よりもずっと手軽にできる。マルチスレッドやマルチプロセスのシステムでは、テストではタイミングに依存するため不具合を捕捉しきれないことがあるが、モデル検査を使えば網羅的に検査する事ができる。またAlloyというツールを使えば、仕様に暗黙の前提を置いていないかとか抜けや漏れがないかを確かめる事ができる。それぞれの手法（ツール）には得意とするところがあり、求める品質と対象のシステムの特徴をよく考えて、適した手法を用いれば過剰品質という状態は避けられるだろう。

以上の議論から私を主張をまとめると以下の通りである。

アジャイル開発においても形式手法を用いる場面はある。ただし、最初の学習段階ではエキスパートの助けがあった方がいいことと問題に適した手法を採用することが大事である。