合金pred声明：方括号和圆括号有区别吗？答案

【问题标题】：Alloy pred declaration: is there a difference between square brackets and parentheses?合金pred声明：方括号和圆括号有区别吗？
【发布时间】：2020-04-29 20:20:55
【问题描述】：

这个问题可能有一个是/否的答案。考虑 sn-p：

sig A { my : lone B }
sig B { }

pred single1 [x:A]{ // defined using []
    #x.my = 0
}
pred single2 (x:A){ // defined using ()
    #x.my = 0
}

// these two runs produce the exact same results
run single1 for 3 but exactly 1 A
run single2 for 3 but exactly 1 A

check oneOfTheMostTrivialQuestionsOnStackOverflow { all x: A | 
    single1[x] iff single2[x] // pred calls use [], so as expected, single2(x) would cause a syntax error
} for 3000 but exactly 1 A // assertion holds :)

single1 和 single2 完全一样吗？

他们似乎是，但我错过了什么吗？

【问题讨论】：

标签： alloy

【解决方案1】：

当我们在 Alloy 4 中扩展语法时，我们将谓词调用更改为 []。我的回忆是我们这样做是为了让解析更容易，所以如果你有一个没有参数的谓词 P，你可以把它称为“P”，如果它后面跟一个括号中的公式就没有问题“ P（...）”。正如 Peter 所指出的，这似乎也是合理的，因为它类似于关系查找运算符，这对于函数来说尤其有意义。我们添加了使用 [] 声明谓词和函数以保持一致性的能力，但没有理由在 decls 中阻止 ()（因为那里没有可能的歧义）。

【讨论】：

感谢您的澄清！

【解决方案2】：

我认为括号最初是用于谓词和函数的。但是，它们被更改为有利于方括号，因为它看起来更具关联性。我依稀记得丹尼尔杰克逊在他的书中解释了这一点。

也就是说，为什么要问，因为您似乎已经证明了这一点？ :-)

【讨论】：

我只是在范围内证明了它；）
如果您不购买小范围假设，请不要使用 Alloy :-) 无论如何，在这个问题上，我认为您已经有了坚实的基础。如果小范围假设可以得到一些显示其局限性的理论，那就太好了。应该有可能以某种方式证明这个问题不会增加超过 2 个 B 的结构复杂性。假设 1 A、0 和 1 B 给出不同的结构，但 2B 在结构上与 1 B 相同。如果小范围假设有理论基础，Alloy 会更有用。