形式仕様記述
形式仕様記述(けいしきしようきじゅつ、formal specification)
何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述
ルールチェック付き仕様記述
形式手法のレベル
でいうとレベル0
詳細化(リファインメント)
形式仕様記述
Z記法
VDM
VDM-SL
VDM++
Bメソッド
Event-B
ProB
定理証明支援系
Agda
Coq
Isabelle
PVS
モデル検査
Alloy
TLA+
SPIN
NuSMV
LTSA
?
KML
ProVerif
確認用
参考
形式手法のまとめ - Qiita
形式仕様記述 - Wikipedia
関連
形式検証
#形式手法