AlloyのRelation
signature内で定義されるフィールドは、Relationを表す
code:alloy
sig Book {
addr: Name -> lone Addr
}
Bookは
addr
fieldを持ち、NameをAddrに関連付ける
lone
は多重度を表す予約語
Alloyの限量
上記だとNameとAddrが1対1であることを表す
関係演算子
/mrsekut-book-4274068587/071 (3.4.3 関係演算子)
https://alloytools.org/spec.html#:~:text=expr%20%3A%3A%3D%20(%20expr%20)-,Relational%20Expressions,-An%20expression%20may
Alloyの(->)
Alloyの(.)
[]
/mrsekut-book-4274068587/077 (3.4.3.3 ボックス結合)
結合
以下は等価
e1 [e2]
e2.e1
~e
^e
*e
<:
:>
Alloyの(++)