旧版本的JML评估(Expression[Id])

Question

我想知道\old(Expression[Id])形式的JML表达式是如何计算的，例如，如果我有\old(vector[value-1])表达式，那么\old是也引用" value“还是仅仅引用vector[value-1]的值。提前感谢！

Answer 1

希望你在别的地方找到了你的问题的答案，但这是第一个：

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