Z言語 (ぜっどげんご) は、Z記法 (ぜっどきほう) ともいい、形式仕様記述言語であり、コンピュータシステムの記述とモデリングを行うために使われる。 ZはZF集合論から名前をとって命名された。 Zは次のことに焦点を当てている。 コンピュータプログラムの簡明な仕様の記述。 意図するプログラムの振る舞いの証明の形式化。 Zは、もともとは1977年に Jean-Raymond Abrial により Steve Schuman とバートランド・メイヤーの支援を得て開発された[1]。 Zの開発は、オクスフォード大学のプログラミング研究グループでさらに続けられた。 Abrial は、1980年前半にこの研究グループで開発作業を行った。 Zは、公理的集合論とラムダ計算、一階述語論理で使われる標準的な数学的記法に基づいている。 Zで記述されたあらゆる式は型づけられており、それにより素朴集合論のパラドック
