【发布时间】：2009-06-26 19:45:32
【问题描述】：
我想知道如何评估 \old(Expression[Id]) 形式的 JML 表达式，即，如果我有 \old(vector[value-1]) 表达式，\old 是否也指“值”或仅指vector[value-1]。提前致谢！
【问题讨论】：
标签： java static-analysis formal-verification jml
【发布时间】：2009-06-26 19:45:32
【问题描述】：
希望您在其他地方找到问题的答案，但这是第一个：
\old(vector[value-1]) 是旧向量中\old(value)-1 的值。
【讨论】：