高品質ソフトウェアの開発をめざしているソフトウェア開発現場の読者を想定し、日本で大規模システムの開発に実際に形式手法を適用した経験に基づき、形式手法の概要とともに、形式手法適用の第一歩となる形式仕様記述言語について解説。