形式仕様記述（Z記法・VDM）とは？
形式仕様記述（Z記法・VDM）とは、仕様を数学的な記法で厳密に書き、あいまいさを排したうえで性質を証明・検証できるようにする手法。事前条件・事後条件・不変条件を明示するのが基本形になる。高い信頼性が要る領域で、どこまでを適用範囲とし費用に見合わせるかの判断が問われる。
けいしきしようきじゅつ
形式仕様記述（Z記法・VDM）の意味
仕様を数学的な記法で厳密に書き、あいまいさを排したうえで性質を証明・検証できるようにする手法。事前条件・事後条件・不変条件を明示するのが基本形になる。高い信頼性が要る領域で、どこまでを適用範囲とし費用に見合わせるかの判断が問われる。
形式仕様記述（Z記法・VDM）の具体例
鉄道の連動論理について「同時に競合する進路が開通しない」という不変条件をZ記法で記述し、モデル検査で反例が存在しないことを確認する。適用は安全に関わる中核部分だけに絞り、周辺の画面や帳票は通常の設計書で記述して費用と期間を抑える。
形式仕様記述（Z記法・VDM）は試験でどう引っ掛けられる？
記述どおりに動くことは証明できても、要求そのものが誤っていれば意味がない。すなわち検証はできても妥当性確認は別問題である。習得と記述の負担が大きく、全機能へ一律に適用するのは現実的でないという制約も押さえる。
形式仕様記述（Z記法・VDM）と関連する用語
最終更新：2026-08-25／解説は資格暗記が独自に作成しています。 過去問の出典は各問題に記載のとおりです。