FactとAssetionの違い
使い道を間違えないようにしないといけない
クレカ決済のモデルを書く時に「キャンセル処理中に無効な状態にならない」というのをAlloyのFactで書いてはいけない そういうスコープを切って検査してしまう
factは仕様で、assertionは仕様の確認という感じか
Assertionはtest codeに近いイメージ
だから、仮にAlloyで検証したモデルを別のコードで書き直すときは、
factはコードに落とすが、Assertionは別に落とす必要はない
「Discussion: Facts vs. Assertions」の節