Alloy
モデル検査をする形式手法言語
SATソルバで制約を満たすモデルを見つける？
ソフトウェア検証のプログラム
()ではなく、[]を関数の括弧として使う。理由は難しい…。
本
『抽象によるソフトウェア設計 Alloyではじめる形式手法』