java - \old(Expression[Id]) 的 JML 评估

Question

我想知道如何\old(Expression[Id])评估表单的 JML 表达式，即如果我有\old(vector[value-1])表达式，是否\old也指“值”或仅指vector[value-1]. 提前致谢！

Answer 1

好吧，希望您在其他地方找到了问题的答案，但这是第一个：

\old(vector[value-1])是旧向量中的值\old(value)-1。