形式手法における検証法は2通りある。 仕様を「定理」とみなし、「公理」と「推論規則」を使って証明する方法。 仕様を「モデル」として構築し、要求として与えられる条件を満たす可能性を計算機上で探索する方法。 1つめの方法に用いるツールは「定理証明系…