形式仕様記述

数学的な論理や集合論に基づく形式言語を使って、ソフトウェアの仕様を厳密に記述すること。自然言語で書いた仕様のあいまいさや矛盾をなくし、仕様の正しさを機械的に検証できる。VDMやZ記法などがある。

形式手法の一つで、IBMウィーン研究所で生まれた仕様記述の方法とその言語（VDM-SL、VDM++）。データの型と不変条件、操作の事前条件・事後条件で仕様を厳密に書き、ツールによる構文・型の検査や、仕様を実行して確かめることができる。

集合論と一階述語論理に基づく形式仕様記述言語。システムの状態と操作を、宣言部と述語部からなるスキーマという単位で記述する。オックスフォード大学を中心に開発され、ISO/IEC 13568として標準化されている。

システムを有限の状態遷移モデルとして表し、到達しうるすべての状態を網羅的に調べて、満たすべき性質（デッドロックが起きないなど）が成り立つかを自動的に検証する手法。テストでは再現しにくい並行処理の不具合を見つけられ、性質が成り立たない場合はそこに至る手順を反例として示す。

集合論と述語論理に基づいて仕様を厳密に記述する形式仕様記述言語。曖昧さのない仕様を作れる。

形式仕様記述と段階的詳細化によってソフトウェアを開発する手法。VDMToolsなどの支援ツールがある。