形式手法
システムの設計・振る舞いを形式的な言語で記述し、その正しさを検証する手法
形式的な言語とは、厳密に決められた記号・構文を持ち、曖昧さのない言語のこと
2つのアプローチがある
定理証明
一連の要件から特定の結論が論理的に導かれることを証明するアプローチ
システムを一連の論理式 Γ として記述し、システムが満たすべき性質はまた別の論理式の集合 𝜙 で表す
Γ から 𝜙 を導出するような証明を見つけることで、システムの正しさを検証する
モデル検査
特定のシステムのモデルが与えられた仕様を満たすことを計算によって決定するアプローチ
関連
2025-06 形式手法入門：生成 AI 時代の『設計』のあり方について
2026-01 形式手法特論：コンパイラの「正しさ」は証明できるか？
2013
「形式手法の独学」のPFD
命題論理、述語論理をはじめとし、Alloy, SPINによるモデル検査の学習パス
IPA 実務家のための形式手法厳密な仕様記述を志すための形式手法入門厳密な仕様記述入門
平易な説明とVDMによる入門