\old(Expression[Id]) 的 JML 评估
我想知道如何评估 \old(Expression[Id]) 形式的 JML 表达式，即如果我有 \old(vector[value-1]) code> 表达式中，\old 是否也引用“value”或仅引用 vector[value-1] 的值。 提前致谢！
I would like to know how a JML expression of the form \old(Expression[Id]) is evaluated, i.e. if I have the \old(vector[value-1]) expression, does the \old also refer to "value" or just the to the value of the vector[value-1]. Thanks in advance!
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
好吧，希望您在其他地方找到了问题的答案，但这是第一个：
\old(vector[value-1])是\old(value) 处旧向量中的值-1。Well hopefully you found the answer to your question elsewhere, but it's the first one:
\old(vector[value-1])is the value in the old vector at\old(value)-1.