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

Question

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

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

标签： dafny

Answer 1

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

当一个表达式在 a 中求值时old，它的所有堆解引用都指向方法开始处的堆。任何不是堆取消引用的东西都不会受到old.

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

然而，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;
}