Z記法
#TODO_2
Z記法(ぜっときほう、Z Notation)
抽象化、表記法、実行不能、ツール群
昔からある形式手法の形式仕様記述の記法
Z記法は公理的な集合論(ZF公理系(ZF)) + 一階述語論理(FOL) + 型理論を合わせたもの
選択公理は含まないらしい
以下のPDFに記法が載っている。
ISO/IEC 13568:2002 Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics
参考
Z言語 - Wikiwand
『仕様記述言語Zと証明環境 Isabelle/HOL-Z』
『形式手法教科書』 P139～
#形式手法