形式手法とは？けいしきしゅほう
形式手法とは、数学的に厳密な記法で仕様を記述し、その性質を証明や網羅的検査で確かめる開発技法。VDM（Vienna Development Method）やZ記法などの、仕様を数学的な記法で書くための言語（形式仕様記述言語）を用いる。自然言語の曖昧さに起因する仕様の矛盾や抜けを、実装前に機械的に検出できる点が特徴。
最終更新：2026-10-10
基本情報を最短で暗記・合格する →背景
自然言語（日本語などの普通の文章）で書いた仕様書は、読む人によって解釈が分かれ、矛盾や抜けが実装やテストの段階まで気づかれずに残りやすい。後の工程で見つかるほど直す費用が大きくなるため、仕様を数学的に厳密な記法で書き、実装の前に機械的に確かめる手法が考えられた。
具体例
鉄道の連動装置や決済の中核処理など、障害の影響が甚大で仕様の抜けが許されない部分に限定して適用する。全体に適用すると習得コストと記述量が見合わないため、重要度の高いモジュールだけに絞る判断が現実的になる。
試験での引っ掛け
「証明したから欠陥ゼロ」ではない。証明されるのは仕様に対する整合性であり、仕様自体が業務要求を取り違えていれば意味がない。また、ありうる状態をすべて調べる検査（モデル検査）は、対象が大きいと調べる状態の数が膨大になるため、対象を要点だけに絞って単純化できるかが結果を左右する。
関連用語
出典・参考
解説は資格暗記が独自に作成しています。過去問の出典は各問題に記載のとおりです。