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