Z記法

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

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

形式仕様記述の手法の一つ。仕様記述言語（VDM-SLなど）で、扱うデータの型や不変条件、操作の事前条件と事後条件を厳密に記述し、仕様の検証や段階的な詳細化を行う。IBMのウィーン研究所で開発された。

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

システムの状態遷移を網羅的に探索し、満たすべき性質が成り立つかを機械的に検証する手法。テストでは見つけにくい並行処理の不具合を検出できる。

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

数学的に厳密な表記と論理に基づいて、システムの仕様を記述し、その正しさを検証する手法の総称。仕様を形式的に書く形式仕様記述と、モデル検査や定理証明による検証があり、鉄道、航空、ICカードなど高い信頼性が求められる分野で使われる。