# 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.

Scroll to Top