Alloyの限量
Q x:e | Fという形式で書く
e.g. one x: Hoge | F
lone
Less than Or equal to oNEらしい
NEってなんやねんという感じするが
0 or 1
one
ちょうど1つ
some
1以上
no
all
例
大学内の各学生は、1つ以上の研究室に所属している ( = 担当の教授がいる)
code:alloy
sig University {
groupMember: Student -> some Professor
}
全ての教授が、自分の研究室に少なくとも一人の学生がいる
code:alloy
sig University {
groupMember: Student some -> Professor
}
someが->の前にある
これ、some Student -> ...と書くのとは違うのか？mrsekut.icon
->の前後に多重度記号があるのはUML図っぽいけど
e.g.
量化制約one x: S | F
制約Fを満たすxがちょうど1つ存在する
読み方としては、x:Sは普通に型付なので1セットとみなして仮にXと置くと
$ \exist X [F] と書いてる感じ
この|は論理式に出てくる[...]と同じようなも
あるいは、Haskellのリスト内包表記内に出てくる|と同じイメージ
量化制約lone e
式eが最大1つのタプルを含む関係を示す
セット宣言 x: some S
Sが単項型を持つ場合、xをSから取り出された要素の非空のセットとして宣言する
関係宣言r: A one -> one B
rをAからBへの1対1の関係として宣言する
シグネチャ宣言one sig S {...}
Sをちょうど1つの要素を含むシグネチャのセットとして宣言する
「set variable」という単語が急に出てきて、ここでしか使われてない...mrsekut.icon