開発手法の構造的比較

両者とも「仕様を重視する」姿勢を持ちます。上流工程で仕様を確定させ、それに基づいて設計・実装を進めるという基本構造は共通しています。

ウォーターフォールの仕様は自然言語で書かれるため、読み手による解釈の差が避けられません。形式手法は数学的記法で仕様を記述するため、解釈の余地を大幅に減らせます。また、ウォーターフォールでは仕様の矛盾は実装・テスト段階まで発見されないことが多いのに対し、形式手法では仕様レベルで機械的に検出できます。

いずれも、最初から完璧な仕様を作ることは困難であるという認識を前提としています。アジャイルはリリース後のフィードバックで反復的に改善し、形式手法は仕様の段階的詳細化によって精度を高めていきます。

アジャイルの「動くソフトウェアを優先する」という価値観に対し、形式手法は「正しい仕様を優先する」という立場をとります。アジャイルでは要件の不確実性をリリース後のフィードバックで吸収しますが、形式手法では仕様段階で曖昧さや矛盾を明示し、機械的に扱える形へ近づけます。

TDDは有限個のテストケース（帰納的アプローチ）で正しさを確認します。100個のテストをパスしても、101番目のケースで失敗する可能性は排除できません。形式手法で定理証明まで行った場合、証明対象として定式化された性質について、すべてのケースで成り立つことを演繹的に示せます。

TDDにはもう一つの本質的な問題があります。テストを書く際に参照される「仕様」が具現化されていないという点です。TDDでは「テストを先に書く」ことが原則ですが、そのテストケースの正しさを担保する仕様はどこにあるのでしょうか。多くの場合、それはテストを書く開発者の頭の中に暗黙的に存在するだけです。書かれるテストケースは、開発者が「おそらくこう動くべきだろう」と考えた振る舞いの断片に過ぎず、網羅性も正確性も保証されません。

さらに深刻なのは、既存コードに対してテストを後付けする場合です。テスト作成者は現在の実装を読んで「このコードは何をすべきか」を推測しますが、このとき参照しているのは本来あるべき仕様ではなく、現状の実装そのものです。コードにバグがあれば、そのバグを含んだ振る舞いを「正しい」としてテストが固定化してしまいます。つまり、テストが品質を保証するどころか、バグを制度化する装置になりかねません。

形式手法ではこの問題が構造的に回避されます。VDM-SLなどの形式言語で仕様を明文化するため、「テストの根拠となる仕様」が具体的な成果物として存在します。テストケースは仕様から導出されるものであり、開発者の暗黙知やコードの現状に依存しません。

ただし、これは形式手法がTDDを否定するということではありません。形式手法で仕様を厳密化し、必要な性質を証明対象として検証した上で、TDDを実装レベルの品質管理に併用することも有効です。両者は補完関係にあります。