ようやく第3章を終えます。今日は 3.7 「濃度制約と整数」。
- 関係に演算子 # を適用すると、タプルの数が得られる
- 整数の演算には plus, minus, mul, div, rem が利用できる
- Alloy では集合(関係)のほうが主役なので、整数の演算はアルファベットの演算子なんですね
- 比較演算子は記号 : = < > =< >= (>= は C などと記号の順番が逆)
- sum
- e.sum は整数の集合 e の総和
- sum x : e | ie は e の各要素について ie を評価した結果の整数の総和
- 整数は関係のアトムとして使える
- S =< T は S, T が整数の集合なら (S.sum) =< (T.sum) と解釈される
- ただし = は集合としての比較の意味のままなのでちょっとややこしい
長かった第3章も終わり、次は第4章「言語」に入ります。 Alloy の言語仕様についてですね。
