Question about the modifies clause

Sep 28, 2012 at 6:02 PM

Hi,

I'm having a tough time understanding why Dafny can't verify this code:

 

 

class A {
  var arr: array;
  predicate Valid
    reads this;
  {
    arr	!= null	&& arr.Length == 5;
  }

  method Init()
    modifies this;
    ensures Valid;
  {
    arr	:= new int[5];
  }

  method Add()	
    modifies arr;
    requires Valid;
    ensures Valid;
  {
    arr[3] := 3;
  }
}

method Test()
{
  var a	:= new A;
  a.Add();
}

Dafny complains about "a.Add()" in method Test():

array.dfy(28,5): Error: call may violate context's modifies clause

Obviously Test() doesn't have a modify clause, but I don't really know what would be the right clause for it.

I appreciate your help.

Coordinator
Sep 29, 2012 at 7:26 AM

The issue is that your Test() method calls a.Add(), which says it modifies the elements of a.arr.  However, Test() itself is declared with an empty modifies clause, so why would Test() be allowed to modify the elements of a.arr?  [theatrical pause]  In addition to what is mentioned in a method's explicit modifies clause, a method is allowed to modify the state of newly allocated objects (and arrays).  So, if Test() can prove that the allocation of a.arr took place after the execution of Test() started (we say that "a.arr" is "fresh" in Test()), then Test() will be allowed to modify the elements of a.arr.

To do this, Init() must promise to assign to "arr" a newly allocated value, which is expressed by putting "fresh(arr)" in the postcondition.  That will verify this program, see http://rise4fun.com/Dafny/pxJz (which also shows some other corrections).

Thinking about this situation a little more, you will probably become disappointed with mentioning "arr" in the specifications of Init() and Add().  That is, you probably want to hide "arr" from callers.  To solve this problem, Dafny offers "dynamic frames" as a specification idiom.  To learn more about these, I recommend reading Section 1 of these Marktoberdorf 2008 lecture notes and/or Section 1.5 of this Dafny paper.

  Rustan

Sep 30, 2012 at 12:17 AM

Thanks very much for your reply.

Here is a follow-up variant. Dafny complains about the following program:

 

class B {}
class A {
  var arr: array;
  predicate Valid
    reads this;
  {
    arr != null && arr.Length == 5
  }

  method Init()
    modifies this, arr;
    ensures Valid && fresh(arr);
  {
    arr := new B[5];
    var i := 0;
    while (i < arr.Length)
      invariant arr != null && arr.Length == 5;
    {
      arr[i] := null;
      i := i + 1;
    }
  }

}

method  Test()
{
  var a := new A.Init();
}

 

 array.dfy(18,10): Error: assignment may update an array element not in the enclosing context's modifies clause.

I think I specified "modifies this, arr" in Init(), but I'm still getting this err.

I appreciate your help.

Coordinator
Sep 30, 2012 at 1:13 AM

There are few things going on here.  First, in this program and the previous, I don't see how you even get it through the compiler, because you need to give the element type of "array".  I'm guessing this must just be a transcription error when you've copied this program into your message?

Second, modifies clauses are interpreted in the method's initial state.  In the specification of Init(), you're giving Init() license to modify the elements of this.arr for the initial value of this.arr.  Since Init() is an initializing method, the initial value of this.arr is irrelevant.  Indeed, the first thing the body of Init() does is assign to this.arr, so whatever initial value this.arr had is then overwritten.  So, my suggestion is that you drop "arr" from the modifies clause of Init(), leaving just "this".

Third, your actual question.  To reason about a loop, you need to have information about what the loop iterations may modify.  It is easy to determine which local variables are modified by a loop, because that can be done by a syntactic inspection.  But if any portion of the heap is modified by the loop, a more detailed analysis is needed.  By default, Dafny applies a method's modifies clause to every loop in the method body (and, as for the modifies clause of the method, remember that this implicitly includes the state of freshly allocated objects).  In your case, that means that Dafny treats each loop iteration as potentially modifying the fields of "this", which in particular means that the verifier thinks that the value of this.arr can be modified by the loop.  So, as the verifier sees things, this.arr has some arbitrary value inside the loop and then the loop body modifies the elements of that this.arr, which is potentially a violation of the method's modifies clause.

There are several ways to fix this problem.

One way is simply to provide a more restrictive modifies clause for the loop:  add "modifies arr;" next to the loop invariant, as shown here: http://rise4fun.com/Dafny/hWNy.  Now Dafny knows that you only intend to modify the elements of this.arr in the loop (but not the fields of "this" and in particular not the field "this.arr"), and Dafny then both enforces this intention and uses it.  Note that "arr" is now part of the loop's modifies clause, so you may wonder why you didn't need it in the method's modifies clause.  The answer is that the method's modifies clause is interpreted in the method's pre-state and it implicitly includes all objects that are freshly allocated in the method body.  So, the method's modifies clause implicitly includes the array that the body allocates and assigns to this.arr.  The modifies clause of the loop is interpreted in the loop's pre-state (and it implicitly includes all objects that are freshly allocated in the loop body).  Thus, putting "modifies arr;" on the loop says that the loop iterations may modify the elements of the array to which this.arr points on entry to the loop.

A different way to solve the problem is to include in the loop invariant the fact that "arr" is fresh:  invariant fresh(arr);, see http://rise4fun.com/Dafny/NO8c.  This solution is also pretty natural--the condition fresh(arr) is established before the loop and it is needed after the loop to show the postcondition.

Another way to solve the problem is to assign the newly allocated array not directly into this.arr, but into a local variable, see http://rise4fun.com/Dafny/vmSJ.  Dafny can then tell, by a simple syntactic scan, that the local variable is not changed by the loop, so the verifier will know that the loop continues to hold a non-null, freshly allocated array of length 5--hence, you don't need a loop invariant at all.  After the loop, assign the local variable to the field "arr".

All of what I have said applies to loops and modifies clauses in general, so they are good things to understand.  In your case, the loop is simple and Dafny offers a feature that lets you avoid the loop altogether.  And if you don't have a loop, you don't need a loop invariant and such things.  To avoid the loop, use Dafny's "parallel" construct:

    arr := new B[5];
    parallel (i | 0 <= i < arr.Length) {
     arr[i] := null;
    }

For the full program, see http://rise4fun.com/Dafny/o6yf.  After this statement, Dafny will also know that all array locations have the value null.  If you wanted to get that from a loop, you also need a loop invariant that says that:

invariant i <= b.Length && forall j :: 0 <= j < i ==> b[j] == null;

See http://rise4fun.com/Dafny/CgIr.

Happy looping,
  Rustan

Oct 4, 2012 at 12:23 AM

Thanks very much for clarifying all these details. With your help I've successfully made some progress.

However, it seems the same error is still bothering me. Here is the link to the more realistic(unfortunately larger) code:

http://rise4fun.com/Dafny/slLJK

I'm getting the "call may violate context's modifies clause" error from method Add() (Line 129).

Based on my understanding of your posts, it seems that the "modifies descriptors" clause of the method Add() is causing the problem.

 

Interestingly, if I substitute line 127 with line 126, that is, using the statement

var fd := 5;

instead of 

 var fd := fdtable.FindNextEmptySlot();

The verification will go through. Otherwise i'm getting the "call may violate context's modifies clause" error.

 

I get two questions: (1) is "modifies descriptors" the right annotation for the method? (2) why calling FindNextEmptySlot() will make a difference?

Your reply is highly appreciated.

Oct 5, 2012 at 10:02 AM
Edited Oct 5, 2012 at 10:02 AM

Method "FindNextEmptySlot" (it is called before method "Add" in "Test") can change value of the field "descriptors" to the newly allocated object. So you should add this property of method "FindNextEmptySlot" as this postcondition using "fresh" keyword of Dafny.

 

ensures if forall k :: 0 <= k < old(descriptors.Length) ==> old(descriptors[k]) != null
then fresh(descriptors) else descriptors == old(descriptors);
Coordinator
Oct 16, 2012 at 2:41 AM

In your example, you can get away with a less specific postcondition like

descriptors == old(descriptors) || fresh(descriptors)

Here is a version of your program that includes this postcondition, along with some other minor adjustments (mostly stylistic--you may or may not like them, but they show you some things you can do):  http://rise4fun.com/Dafny/lmlhu

By the way, I would suggest hiding the "descriptors" array from clients.  That is, only mention "Contents" in the method specifications, not "descriptors".  To pull this off, you need a variable like the standard "Repr" ghost field in dynamic frames.

  Rustan