AlloyのAssertion

モデルの特定の特性をテストするための命題を定義する

別の箇所で書かれている仕様に対して「この条件が満たされているか？」を確認する

満たしていない場合は反例が得られる

この時チェックされるのは1つのAssertionだけであり、他のAssertionは無視される

例

code:alloy

assert acyclic { show2[] implies noSelfLoop[] }

code:alloy

abstract sig FSObject { parent: lone Dir }

sig Dir extends FSObject { contents: set FSObject }

sig File extends FSObject { }

one sig Root extends Dir { } { no parent }

fact { all d: Dir, o: d.contents | o.parent = d }

fact { FSObject in Root.*contents }

// 上記の仕様に対し、循環してないことを確認

assert acyclic { no d: Dir | d in d.^contents }

check acyclic for 5

以下2つは同値らしい

code:alloy

moveOkay: check {

all fs, fs': FileSystem, x: FSObject, d:Dir |

} for 5

code:alloy

assert moveOkay {

all fs, fs': FileSystem, x: FSObject, d:Dir |

}

check moveOkay for 5