JML Оценка \ old (выражение [Id])

Question

Я хотел бы знать, как оценивается выражение JML формы \old(Expression[Id]), т. Е. Если у меня есть выражение \old(vector[value-1]), имеет ли значение \old значение «значение» или просто до значения vector[value-1]. Заранее спасибо!

Answer 1

Ну, надеюсь, что вы нашли ответ на свой вопрос в другом месте, но это первый один:

\old(vector[value-1]) это значение в старом векторе на \old(value)-1.