对于 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;
}