perfbook 形式的検証の章、公理論的アプローチの訳