Dafny issue modifying array member of class

Question

I'm trying to modify an array member of a class in Dafny. These modifications may include re-assigning the array member, modifying elements of the array member, or both. For example, consider the following class definition:

class Class {
    var arrayMember : array<int>
}

The following verifies, which both reassigns the member and modifies an element:

method verifies(obj : Class)
modifies obj, obj.arrayMember
{
    if (obj.arrayMember.Length < 5) {
        obj.arrayMember := new int[5](i => 0);
    }
    obj.arrayMember[4] := 3;
}

However, when I pull the code which re-assigns the array out into a separate method, I start to get issues:

method expandArray(obj : Class, size : nat)
modifies obj
ensures obj.arrayMember.Length >= size
{
    if (obj.arrayMember.Length < size) {
        obj.arrayMember := new int[size](i => 0);
    }
}

method doesNotVerify(obj : Class)
modifies obj, obj.arrayMember
{
    expandArray(obj, 5);
    obj.arrayMember[4] := 3;
}

Specifically, obj.arrayMember[4] := 3 does not verify with assignment might update an array element not in the enclosing context's modifies clause. It seems to me that I should be able to modify obj.arrayMember as it is in the modifies clause of the method. I can only conclude that there must be something wrong with the expandArray method as the non-verifying method can be made to verify by inlining it (i.e. the first snippet of code I wrote, which verifies).

Any idea why this code won't verify?

Answer 1

The problem is that expandArray is allowed to reassign the array to point to some other array, and Dafny is worried that it might have reassigned the array to point to some existing array that is not in the modifies clause of doesNotVerify. You can add additional postconditions to expandArray to tell Dafny that the method only assigns "fresh" (ie, newly allocated) arrays to the array member:

ensures obj.arrayMember == old(obj.arrayMember) || fresh(obj.arrayMember)

This says that either expandArray does not change which array obj.arrayMember points to, or, if it does change it, it changes it to point to a freshly allocated array, not some existing array.

---

If you want to go deeper into building mutable heap data structures in Dafny, I recommend checking out sections 0 and 1 of Specification and Verification of Object-Oriented Software. (Note that this paper is quite old now, so some minor things are out of date. But the key ideas are there.) In particular, check out the footprint set and the Valid predicate to manage the "footprint" (all transitively reachable mutable references).