对于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])获得数组"的第0个值；指向"；通过旧堆中的CCD_ 9。

然而，a本身并不是堆解引用，它只是本地函数的一个参数，其值永远不会改变。所以old(a) == a。考虑这一点的一种方式是CCD_；地址"；的地址，并且该地址在方法的生存期内不会更改。

既然我们知道了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;
}