对于 Dafny 中的数组，old(a[0]) 和 old(a)[0] 之间有什么区别

Question

对于 Dafny 中的数组，old(a[0]) 和 old(a)[0] 有什么区别？

一种方法通过将 1 添加到第一个元素来修改数组 'a'。在该方法的结论中，old(a[0]) 和 old(a)[0] 的值是多少？

Answer 1

好问题！是的，它们是不同的。

当在 old 中计算表达式时，它的所有 堆取消引用 都引用方法开头的堆。 old.

不会影响任何非堆取消引用的内容

在您的示例中，a[0] 是堆取消引用，因此 old(a[0]) 获取旧堆中 a“指向”的数组的第 0 个值。

然而，a 本身并不是堆取消引用，它只是本地函数的一个参数，其值永远不会改变。所以old(a) == a。一种思考方式是 a 存储数组的“地址”，并且该地址在方法的生命周期内不会改变。

既然我们知道 old(a) == a，那么接下来就是 old(a)[0] == a[0]。换句话说，old 在你的第二个例子中没有效果。

这里有一个小例子来演示：

method M(a: array<int>)
  requires a.Length >= 2
  requires a[0] == 1
  modifies a
  ensures a[1] == old(a[0])  // so far so good
  ensures old(a) == a        // perhaps surprising: Dafny proves this!
  ensures a[1] == old(a)[0]  // but this is not necessarily true, 
                             // because old(a)[0] actually means the same thing as a[0]
{
  a[1] := 1;
}

对于 Dafny 中的数组，old(a[0]) 和 old(a)[0] 之间有什么区别

For an array in Dafny whats the difference between old(a[0]) and old(a)[0]

dafny