合金古怪的行为？
abstract sig S {}
one sig S1, S2 in S {}
fact {S1 != S2}
run {-1 < S1.(S2 -> 1)}当我打开实例时，我得到
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7, S$0, S$1}
Int={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/S={S$0, S$1}
this/S1={S$1}
this/S2={S$0}从评价者那里，
(1) S1.(S2 -> 1)求值为{} (2) none = S1.(S2 -> 1)求值为真 (3) -1 < S1.(S2 -> 1)求值为true //为什么整数小于空集？ (4) -1 < none给出类型错误//这看起来不错，但是给(3)，为什么这会给类型错误？ (5) 0 <= S1.(S2->1)求值为真 (6) 0 >= S1.(S2->1)求值为真 (7) 0= S1.(S2->1)对false //给定(5) (6)求值，似乎是S1，(S2->1)求值为0，但不是. (8) 0=无计算为假 (9) 0 <= none给出类型错误/ (8) (9)似乎很有趣，因为"=“并不解释为整数比较。
有人能解释一下为什么(1) - (9)会发生吗？有窃听器吗？
回答 1
Stack Overflow用户
发布于 2017-04-04 17:00:49
(1)这应该是显而易见的原因:它是一个关系连接，S1与S2不一样
(2) none计算为空集，因此给出(1) none = S1.(S2->1)是有意义的
(3)由于-1的类型是int，而S1.(S2->1)的类型是S.(S->int)，所以没有类型错误。问题只是为什么-1小于计算为空集的整数类型表达式。首先，表达式-1 < S1.(S2->1)必须求值(也就是说，不能像在编程语言中那样抛出异常)。此外，这是一个布尔表达式，因此它必须计算为true或false。那么合金做了什么，为了计算<算子，它必须把两边转换成一个单一的(标量)整数，即使两边实际上都是整数集(所有的东西都是合金中的集合/关系)，它是通过总结每个集合中存在的所有原子来实现的。因此，只是为了算术比较，，S1.(S2->1)计算为0。
(4)现在应该很清楚，-1 < none确实是一个类型错误，因为左侧的类型是int，右侧的类型是none。
(5)、(6)与(3)相同的解释
(7) 0 = S1.(S2->1)是假的，因为=是，始终是集合比较，而不是整数比较。如果尝试类似于1 + 2 = 3的内容，就会得到false，因为集合{1，2}不是{3}。
(8)同样，=是一个集合比较
(9)同样的解释是(4)
https://stackoverflow.com/questions/43212417
复制相似问题
腾讯云开发者
