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~
#形式手法