对于Dafny中的数组，olda [0]和olda[0]之间有什么区别

如何解决对于Dafny中的数组，olda [0]和olda[0]之间有什么区别

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

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

解决方法

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

在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;
}