CODEWITHSUNDEEP
dafny
MissyR
MissyR

Reputation: 23

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

For an array in Dafny, what's the difference between old(a[0]) and old(a)[0]?

A method modifies an array 'a' by adding 1 to the first element. At the conclusion of the method, what is the value of old(a[0]) and old(a)[0]?

Upvotes: 2

Views: 1512

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

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

Upvotes: 1

Related Questions