Объявление 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», и не было бы проблем, если бы после него была формула в паранах » П (...)". Как отмечает Питер, это также казалось разумным, поскольку он похож на оператор реляционного поиска, и это имеет смысл, особенно для функций. Мы добавили возможность объявлять предикаты и функции с помощью [] для согласованности, но не видели причин для предотвращения () в decls (поскольку там нет возможной двусмысленности).

Answer 2

Я думаю, что скобки изначально использовались для предикатов и функций. Однако они были изменены в пользу квадратных скобок, потому что это выглядело более реляционным. Я смутно припоминаю, что Даниэль Джексон объясняет это в своей книге.

При этом нужно спрашивать, потому что вы, кажется, сами это доказали? : -)