Evaluación JML de \ old (Expression [Id])

Question

Me gustaría saber cómo se evalúa una expresión JML de la forma \old(Expression[Id]), es decir, si tengo la expresión \old(vector[value-1]), ¿el \old también se refiere a " value " o simplemente al valor de vector[value-1]. Gracias de antemano!

Answer 1

Bueno, espero que hayas encontrado la respuesta a tu pregunta en otro lado, pero es la primera:

\old(vector[value-1]) es el valor en el vector antiguo en \old(value)-1.