JML Bewertung der \ alt (Expression [Id])

Question

Ich möchte wissen, wie ein JML Ausdruck der Form \old(Expression[Id]) ausgewertet wird, das heißt, wenn ich den \old(vector[value-1]) Ausdruck haben, wird der \old auch auf „Wert“ oder nur die auf den Wert des vector[value-1] beziehen. Vielen Dank im Voraus!

Answer 1

Nun hoffentlich finden Sie die Antwort auf Ihre Frage an anderer Stelle, aber es ist das erste:

\old(vector[value-1]) ist der Wert in dem alten Vektor bei \old(value)-1.