Z記法

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

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

Web APIのための問合せ言語と、その実行環境の仕様。クライアントが必要なデータの項目と構造を問合せで指定し、1つのエンドポイントから過不足なく取得できるため、RESTで起こりやすいデータの過剰取得や、複数回のリクエストを減らせる。スキーマでデータの型を定義する。

データベースの構造を定義・変更・削除するための言語。SQLではCREATE TABLE、ALTER TABLE、DROP TABLE、CREATE VIEW、CREATE INDEXなどの文が該当する。データを操作するDML、権限などを制御するDCLと区別される。

集合論や論理学などの数学的な表記法を使い、システムの仕様を曖昧さなく記述すること。自然言語の仕様に比べて解釈の違いが生じず、矛盾や漏れを機械的に検査できる。代表的な言語にVDMやZ記法がある。

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

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