I would like to know how a JML expression of the form \old(Expression[Id]) is evaluated, i.e. if I have the \old(vector[value-1]) expression, does the \old also refer to "value" or just the to the value of the vector[value-1]. Thanks in advance!
Well hopefully you found the answer to your question elsewhere, but it's the first one:
\old(vector[value-1]) is the value in the old vector at \old(value)-1.