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

Good question! Yes, they are different.

When an expression is evaluated inside an old, all of its heap dereferences refer to the heap at the beginning of the method. Anything that is not a heap dereference is not affected at all by old.

In your example a[0] is a heap dereference, so old(a[0]) gets the 0-th value of the array “pointed to” by a in the old heap.

However, a by itself is not a heap dereference, it’s just a parameter to the local function whose value never changes. So old(a) == a. One way to think about this is that a stores the “address” of the array, and that address doesn’t change over the lifetime of the method.

Now that we know old(a) == a, it follows that old(a)[0] == a[0]. In other words, the old has no effect in your second example.

Here is a small example to demonstrate:

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

CLICK HERE to find out more related problems solutions.

Leave a Comment

Your email address will not be published.

Scroll to Top