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!
views:
61answers:
1
A:
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
.
Pascal Cuoq
2009-08-03 22:16:00