Error with modifies clause

[dreamqin68]

Hi All,

I have a question and hope to get help. Thanks.

class TestType
{
    var id:int
}

method test1(element:TestType) returns(b:array<TestType>)
    ensures b.Length == 3;
    ensures fresh(b)
{
    var a := new TestType;
    b:= new TestType[3](_=>a);
    b[0] := element;
}

method test2(b:array<TestType>)
    requires b.Length == 3
    modifies b, b[..]
{
    b[0].id := 1;
}

method Main()
{
    var element := new TestType;
    element.id := 2;

    var b:= test1(element);
    test2(b); //Error    
}

After verification shows Error: call might violate context's modifies clause in the above code.

This error may be related to modifies b[..]. How to resolve this issue?

[atomb]

This is a very subtle issue! The following modified program passes:

class TestType
{
    var id:int
}

method test1(element:TestType) returns(b:array<TestType>)
    ensures b.Length == 3;
    ensures fresh(b)
    ensures fresh(b[1])
    ensures fresh(b[2])
    ensures b[0] == element
{
    var a := new TestType;
    b:= new TestType[3](_=>a);
    b[0] := element;
}

method test2(b:array<TestType>)
    requires b.Length == 3
    modifies b, b[..]
{
    b[0].id := 1; // Allowed because b[0] is equal to element, allocated in main
    b[1].id := 1; // Allowed because b[1] is fresh after test1
}

method Main()
{
    var element := new TestType;
    element.id := 2;

    var b:= test1(element);
    test2(b); // No error    
}

Several things are key to point out here:

• Since element was allocated in Main, code called from Main is allowed to modify it. However, for Dafny to know that element is the thing being modified, the contract on test1 must provide more information (ensures b[0] == element).
• If test1 also ensures that b[1] and b[2] are fresh (in addition to b itself), then Main is allowed to modify them.

[atomb]

Loops require their own modifies clauses in Dafny. I think if you add modifies i, b, b[..] to the loop, it should go through.

[dreamqin68]

I add modifies b, b[..] to the loop, but it still shows Error: call might violate context's modifies clause.

[atomb]

Okay, this is another tricky case. :) It turns out you just want modifies b[..]. The reason is that, if the loop actually modifies b on one iteration (that is to say, changes what objects it contains), then the objects it might modify on the next iteration could change, and those new objects might be outside of the modifies clause. By only including b[..], you state that the set of objects in the array b doesn't change, but the fields of those objects might change.

[dreamqin68]

Gotta, Thank you!

[rsingha108]

This is super useful. @atomb Can you tell me what to provide in the modifies clause of the loop if I am modifying the field of a field of some b[i].

i.e.

inside the while loop:
b[i].x.y := z