合金pred声明：方括号和括号之间是否有区别？

Question

该问题可能回答是/否。考虑一下代码段：

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完全相同吗？

他们似乎是，但是我想念什么吗？

Answer 1

当我们扩展Alloy 4中的语法时，我们将谓词调用更改为[]。我的回忆是，我们这样做是为了使解析更加容易，因此，如果您拥有不带参数的谓词P，则可以将其称为“ P”，并且如果在parens中使用公式后跟它也不会有问题“ P（...）”。正如Peter所指出的那样，这也似乎是合理的，因为它类似于关系查找运算符，这对于功能尤其有意义。我们增加了使用[]声明谓词和函数以保持一致性的功能，但没有理由在decls中阻止（）（因为那里没有歧义）。

Answer 2

我认为括号最初是用于谓词和函数的。但是，由于方括号使它们看起来更具关联性，因此更改了方括号。我隐约记得丹尼尔·杰克逊（Daniel Jackson）在他的书中对此做了解释。

就是说，为什么要问，因为您似乎已经证明了它？ ：-）