La pregunta probablemente tiene una respuesta sí / no. Considere el fragmento:

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 y single2 son exactamente iguales?

Parecen serlo, pero ¿me estoy perdiendo algo?

1
Michalis Famelis 29 abr. 2020 a las 23:20

2 respuestas

La mejor respuesta

Cuando ampliamos la sintaxis en Alloy 4, cambiamos las invocaciones de predicados a []. Recuerdo que lo hicimos para facilitar el análisis, de modo que si tuviera un predicado P sin argumentos, podría llamarlo simplemente "P", y no habría problemas si fuera seguido de una fórmula en parens " PAGS (...)". Como señala Peter, también parecía razonable ya que es similar al operador de búsqueda relacional, y esto tiene sentido especialmente para las funciones. Agregamos la capacidad de declarar predicados y funciones con [] para mantener la coherencia, pero no vimos ninguna razón para prevenir () en decls (ya que no hay una posible ambigüedad allí).

1
Daniel Jackson 30 abr. 2020 a las 12:50

Creo que los paréntesis se usaron originalmente para predicados y funciones. Sin embargo, se cambiaron a favor de los corchetes porque lo hacía parecer más relacional. Recuerdo vagamente que Daniel Jackson explica esto en su libro.

Dicho esto, ¿por qué preguntar porque parece que lo has probado tú mismo? :-)

1
Peter Kriens 30 abr. 2020 a las 08:02