形式手法
システムの設計・振る舞いを形式的な言語で記述し、その正しさを検証する手法
形式的な言語とは、厳密に決められた記号・構文を持ち、曖昧さのない言語のこと
2つのアプローチがある
定理証明
一連の要件から特定の結論が論理的に導かれることを証明するアプローチ
システムを一連の論理式 Γ として記述し、システムが満たすべき性質はまた別の論理式の集合 𝜙 で表す
Γ から 𝜙 を導出するような証明を見つけることで、システムの正しさを検証する
モデル検査
特定のシステムのモデルが与えられた仕様を満たすことを計算によって決定するアプローチ
関連
形式手法入門：生成 AI 時代の『設計』のあり方について