Alloyガール5
ここまでの話はこちら: Alloy
第5回
Alloy: もしかしてStateManager.stateがStateManagerのメンバ変数だとか、State.belongがStateのメンバ変数だとか勘違いしているんじゃない？
僕: えっ、違うの？
Alloy: ぜんぜん違う。オブジェクト指向に毒されているわね。
おさらい
Alloy: まずおさらいしてみましょう。
one sig StateManager {
state: set State
}
sig State {
}
fact {
all s: State | s in StateManager.state
}
run {} for exactly 3 StateAlloy: このとき、Stateとはなんでしょう？
JS: クラス？
僕: いや、クラスじゃなくてシグニチャだよね。
Alloy: ふーん、君はそう認識しているのか。じゃあ、シグニチャとはなんでしょう？
僕: えっ。
Alloy: それが説明できないのでは「sig = シグニチャ」っていう一欠片の知識をオウム返ししているだけね。何も理解していないのと同じだわ。
僕: うむむ、えっと、型？
Alloy: じゃあ、型とは何？
僕: うーん……、変数についたメタデータ、ってのはこの場合しっくりこないから……値の集合？
Alloy: そうね。じゃあEvaluatorで実際の値を眺めてみましょうか。
Evaluatorを使う
Alloy: 事例を可視化したウィンドウでEvaluatorのボタンを押せば、その実例においてStateとかが具体的にどういう値になっているか観察できるわ。
Alloy: つまりStateは3つのアトムState$0, State$1, State$2から構成された集合ということね。
JS: アトム？
Alloy: アトムは分割ができず、時間によって変化せず、意味を持たないもの。
僕: ただのラベルのようなものだね。
Alloy: そう。そしてstateは関係の集合。{StateManager$0 -> State$0, StateManager$0 -> State$1, StateManager$0 -> State$2}。ここで問題です。関係とは何でしょう。はい、僕君！
僕: えっ、あっ、アトムが2個ペアになったもの？
Alloy: そうね。2個とまで言い切ってしまうと「二項関係」って前提が入っちゃってるけど。例えばこれをみて。
sig X{
rel: X -> X
}
run {
one rel
} for exactly 2 XAlloy: これならrelは例えば{X$0 -> X$1 -> X$0}になるわ。
僕: これは3つのアトムの組だと考えていいの？
Alloy: ええ。この場合relは三項関係ね。
