Alloy で形式手法を始めてみた！～述語，関数，実行編～
ここでは，述語 (pred) や関数 (fun) の書き方を説明します．その前に，述語内に記述する
条件式について説明します．
条件式
述語を説明する前に，プログラミングでいう if にあたる条件式の書き方を説明します．
Alloy では if ではなく，A implies B else C のような書き方をします．
implies は，英語の意味そのままで「〇〇であれば××」を表します．
A implies B
A implies B は，
- A が false であるか，
- A と B が共に true の場合
に true となります．数学では，前提条件が false であれば A → B は必ず true ですよね．
例えば，以下の例では，B のインスタンスが一つの場合しかインスタンスが生成されません．
one sig A {
}
sig B {}
fact {#A = 1 implies #B =1}
しかし，以下のように変えると（#A の条件を変更），B のインスタンスが見つかります．
one sig A {
}
sig B {}
fact {#A > 1 implies #B =1}
A implies B else C
A implies B else C は，先ほどと違って else がついています．この場合，通常のプログラミングと同じように，
- A が true かつ B が true の場合，
- A が false かつ C が true の場合
に true となります．
例えば，次の場合， #A > 1` は成り立ちませんから，` #C > 0
one sig A, B {
}
sig C {}
fact {#A > 1 implies #B = 1 else #C > 0 }
A iff B
iff は数学で使う場合と同様，if and only if の略，つまり同値という意味です．
したがって， A iff B
例えば，以下の例では唯一つインスタンスが見つかります．
one sig A, B {
}
fact {#A > 1 iff #B > 1}
しかし，次の例ではインスタンスは見つかりません．
one sig A, B {
}
fact {#A > 1 iff #B = 1}述語 (pred)
pred は
pred name[a: Set1, b:Set2...] {
constraint
}の形で記述します．name をつけることで，名前をつけることができます．引数は省略可能です．
pred を書いたあと， run
sig A, B {}
pred AisAtLeastOne {
#A > 0
}
pred AandBisAtLeastOne {
AisAtLeastOne and #B > 0
}
run AandBisAtLeastOne
上記の例のように，pred の中から pred を呼び出すこともできます．
以下は，引数をもたせた場合の実行例です．
one sig Kansai, Kanto {}
abstract sig Prefecture {
region: one Kansai + Kanto
}
one sig Osaka, Tokyo extends Prefecture {}
fact {
Osaka.region in Kansai and
Tokyo.region in Kanto
}
pred kansai[p: Prefecture] {
p.region = Kansai
}
run {one tokyo: Tokyo | kansai[tokyo]} // こちらを実行してもインスタンスは見つからない
run {one osaka: Osaka | kansai[osaka]} // こちらを実行するとインスタンスが見つかる関数 (fun)
関数は述語とほぼ同じですが，値を返すという点で述語と異なります．
以下のように記述します．
fun name[a: Set1, b: Set2,...]: returnType {
expression
}先程 Osaka と Tokyo に Kansai, Kanto を fact の中で割り当てていましたが，
今度は fun の中で割り当ててみます．
abstract sig Region {}
one sig Kansai, Kanto extends Region {}
abstract sig Prefecture {
region: one Kansai + Kanto
}
one sig Osaka, Tokyo extends Prefecture {}
fact {
Osaka.region in getRegion[Osaka] and
Tokyo.region in getRegion[Tokyo]
}
fun getRegion[pref: one Prefecture] : Region {
pref in Osaka implies Kansai else Kanto
}
なお，述語と関数は一般には再帰呼び出しはできません．限られた回数のみであれば可能なようです．
事実 (fact)
これまでおまじない的に使ってきた "fact" ですが，Analyzer がインスタンスを探索する際に fact に記述された条件を合致するもののみ探索対象とします．
言い換えると，必ず成り立ってほしい条件を記述するためのものということになります．
表明 (assertion)
ある性質が成り立つかどうかをチェックするために使用します．
pred とほぼ同じですが， run` コマンドではなく` check
Analyzer は，表明が成り立たないようなインスタンス（反例）を探索します．
abstract sig Region {}
one sig Kansai, Kanto extends Region {}
abstract sig Prefecture {
region: one Kansai + Kanto
}
one sig Osaka, Tokyo extends Prefecture {}
fact {
Osaka.region in getRegion[Osaka] and
Tokyo.region in getRegion[Tokyo]
}
fun getRegion[pref: one Prefecture] : Region {
pref in Osaka implies Kansai else Kanto
}
assert OsakaisKansai {
Osaka.region in getRegion[Osaka]
}
assert OsakaisKanto {
Osaka.region in getRegion[Tokyo]
}
check OsakaisKansai // 反例は見つからない
check OsakaisKanto // 反例が見つかる実行 (run) コマンドとスコープ
run コマンドは，
run predication scopeの形で記述します．
run {} for 5
すべてのシグネチャが高々 5 個のインスタンスが探索されます．
sig A, B, C {}
run {} for 5
run {} for 5 but 2 A
A のインスタンスは高々 2 個までしか探索されません．
sig A, B, C {}
run {} for 5 but 2 A
run {} for 5 but exactly 2 A
A のインスタンスがちょうど 2 個のインスタンスが探索されます．
sig A, B, C {}
run {} for 5 but exactly 2 A
最後に
今回でようやく，ツールがまともに実行できるところまで説明できました．
今後は，module の説明をできるよう勉強していこうと思いますので，次回の投稿までかなり時間が空きそうです．
参考
非公式ドキュメントですが，基本的にはここを参照しています．
公式の言語リファレンスも参考にしています．
過去の投稿
では！
コメント