要件仕様を「仕様記述言語」で厳密に定義する「フォーマルメソッド」と呼ぶ手法が、再び注目を集めている。要件仕様からあいまいさを排除できるために、システムの品質と開発生産性を大幅に向上できるからだ。フォーマルメソッドの基礎から、実際の開発事例までを紹介する。