開発手法の構造的比較

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

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

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

アジャイルの「動くソフトウェアを優先する」という価値観に対し、形式手法は「正しい仕様を優先する」という立場をとります。アジャイルでは要件の不確実性をリリース後のフィードバックで吸収しますが、形式手法では仕様段階での数学的検証によって不確実性を事前に排除することを目指します。

TDDは有限個のテストケース（帰納的アプローチ）で正しさを確認します。100個のテストをパスしても、101番目のケースで失敗する可能性は排除できません。形式手法は数学的な論理証明（演繹的アプローチ）により、すべてのケースで仕様が満たされることを保証します。

ただし、これは形式手法がTDDを否定するということではありません。形式手法で仕様の正しさを保証した上で、TDDを実装レベルの品質管理に併用することも有効です。両者は補完関係にあります。