JML Auswertung von \ alt (Ausdruck [Id])

Question

Ich würde gerne wissen, wie ein JML-Ausdruck der Form \old(Expression[Id]) ausgewertet wird, dh wenn ich den \old(vector[value-1]) Ausdruck habe, bezieht sich der \old auch auf "Wert" oder nur die auf den Wert der vector[value-1]. Danke im Voraus!

Answer 1

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

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