Alloyコードを集合論的に解釈
高抽象度のOOP的解釈でもなく、低抽象度のatom,relations解釈でもなく、集合的に解釈するのが一番便利だろうmrsekut.icon
(Alloyであるとか関係なく)集合を論理式で記述する、と捉えれば自然に宣言的になるわけだし
以下のようなコードがあった時
code:alloy(ts)
sig S extends E {
F: one T
}
fact {
all s:S | s.F in T
}
以下のように解釈できる
SやEは集合である
$ S\sube E
extendsは部分集合
Fは、Sを(一つの)Tに関連付ける関係である
$ F: S\to Tのイメージ
(上記コード内に含まれていないがTはsigで宣言されている)
なので、当然s.F$ \inTになる
上記のfactの記述は冗長なのでわざわざ書いている意味がないmrsekut.icon
s: Sは、$ s\in Sを表す
.は複数の関係の合成
. composes relations
s.F composes the unary relation s with the binary relations F, returning a unary relation of type T
この説明では、一番左の項である値のことを「unary relation (単行関係?)」と呼んでる
一番左の項は値なので、hsの.よりは|>の方が近そう
上記のページには書かれていないけど、Signature同士を+や-で演算できるのも、集合と解釈していれば自然に理解できるmrsekut.icon