Question regarding framing, loops, and debugging

Feb 26, 2014 at 9:21 PM

Before I post this, I did read through 'Tips on framing, loops, and debugging' and still couldn't solve my verification error.

Suppose I have a List<T> class and I want to create an array of type List<T>. Something like this:
var items := 10;
var anotherArrayList := new List<int>[items];

anotherArrayList[0] := new List<int>(10);  
// and initialize the other elements
Instead of initializing each element in the array individually, I'm trying to initialize each element in a loop and having a heck of a time verifying it. The verification error that doesn't make much sense to me is 'Error: call may violate context's modifies clause' in the following code:
var i := 0;
    while ( i < anotherArrayList.Length)
        modifies anotherArrayList;
        decreases anotherArrayList.Length-i;
        invariant  0 <= i <= anotherArrayList.Length;
        anotherArrayList[i] := new List<int>(10);
        assert anotherArrayList[i] != null && anotherArrayList[i].Valid &&  !anotherArrayList[i].isFull;
        i := i + 1;

    assume anotherArrayList[1] != null &&
        anotherArrayList[1].Valid &&

    anotherArrayList[1].append(5);          // modifies error
After the loop exits, Dafny doesn't see the anotherArrayList elements are initialized, but even if I assume those elements are initialized, I still get the 'modifies error.' I tried using fresh(..) as in 'Tips on Framing..' and I tried creating a lemma and predicate to show in the loop and the loop invariant that the anotherArrayList[ i ] element is initialized, but no success. I imagine my invariant doesn't have enough in it either, but I'm more concerned about the modifies error.

What is the modifies error referring to in this code? I want to call anotherArrayList[1].append( ), but according to this error, I cannot.
Mar 21, 2014 at 1:06 AM
There are two things going on. One is that the code needs a stronger loop invariant than what you've written above. The other is that Dafny's formalization of arrays was missing two crucial properties. I have now fixed the latter, in change sets 8f7ca6080e83 and 2d870bc53b40; these will appear on rise4fun next week. Let me explain what's missing in the loop invariant.

Your loop invariant says nothing about the elements of the array being initialized. For starters, the loop invariant needs to keep track of that, for every index j visited,
anotherArrayList[j] != null
Then, to live up to append's precondition, you need to know that anotherArrayList[j] is not full:
In addition, since you're using autocontracts, the append method will have an additional precondition, namely Valid(). So, you need to keep track of that each initialized array element satisfies Valid():
So far, these things are fairly straightforward, I would say. And indeed, you indicated after the loop--using an assume statement--that you knew these things were necessary. After adding the new loop invariants I have suggested, you can now convert the assume to an assert.

Two tricky things remain, and they regard framing (which is in the Subject of your question).

Let me do them in this order. First, to call append, the calling context must have permission to modify whatever append is going to modify. The modifies clause of append says this, listarray, and autocontracts adds Repr to that. Since Valid-ity implies that this and this.listarray are both in this.Repr, I will just think of it as Repr (indeed, since you're using autocontracts, you don't have to write that modifies clause explicitly). So, the proof obligation is to show the calling context (that is, method test()) is allowed to modify anotherArrayList[1].Repr.

Method test() has an empty modifies clause, but that still gives it the license to modify objects allocated on its behalf. Stated different, any object that was not allocated on entry to test() is an object whose state test() is allowed to modify. The jargon for "not allocated on entry [to the method]" is "fresh [to the method]". For this reason, we need to know, at the time of the call to append, that anotherArrayList[1].Repr is fresh. We can add that to the loop invariant:
Only one thing remains and that is to prove that the loop body maintains the Valid-ity of array elements visited in previous iterations. The explicit reads clause of Valid() says that Valid() depends on this, listArray, and the reads clause supplied by autocontracts is this, Repr. Again, since Valid-ity implies that this and listArray are in Repr, I will focus on just Repr (and, as before, you could have omitted the explicit reads clause, since you're using autocontracts).

The loop body performs two modifications in the heap. One is caused by allocating and constructing a new object, but that affects only objects that this operation allocates, so no previous Valid-ity is affected. The other modification the loop body performs is to update anotherArrayList[i]. So, if anotherArrayList were part of the Repr of some anotherArrayList[j], then its Valid-ity may have been affected. But this can't be the case--anotherArrayList is allocated before the loop, and each Repr only contains things allocated after the loop started. Yes, but the loop invariant about fresh(...Repr) only says that Repr doesn't contain any objects allocated on entry to test(), which does not include anotherArrayList, which is allocated inside test(). Therefore, we need to explicitly include in the loop invariant that anotherArrayList is not part of the Repr of any of the visited lists:
anotherArrayList !in anotherArrayList[j].Repr
In summary, the loop invariant you need to add to your loop is:
invariant forall j :: 0 <= j < i ==> anotherArrayList[j] != null && anotherArrayList[j].Valid();
invariant forall j :: 0 <= j < i ==> !anotherArrayList[j].isFull;
invariant forall j :: 0 <= j < i ==> fresh(anotherArrayList[j].Repr) && anotherArrayList !in anotherArrayList[j].Repr;
To verify your program, you need to pick up the fixes I just checked in. They are available in source form now, and I would expect them to be available on rise4fun sometime next week.

Here is a complete version of the program:, including some clean-up of things that autocontracts supplies for you.

Marked as answer by rustanleino on 3/20/2014 at 5:06 PM
Mar 25, 2014 at 9:12 PM

Thank you very much for the response. It's a great explanation. Before I posted this, I sort of knew I needed to show the array elements were initialized, but I didn't know the specifics. Now I do : )

I do need to play with that example some more. I can get 'anotherArrayList[1].append(5); ' to verify, but I cannot get 'anotherArrayList[1].append(2);' followed by 'anotherArrayList[2].append(2);' to verify. It's probably something wrong with the List class' spec, but that's an exercise I need to play with more.