Framing confusion

Mar 14, 2014 at 11:31 PM
In the fragment below, it's sufficient to declare "modifies A" in Swap; but "reads A" in Sorted does not work --- I need what's shown there.

So I'm missing something, I guess. Could someone explain why the modifies and the reads have to be different in these two cases?

Thanks!

class QuickSort {
var A: array<int>;

method Swap(i: int, j: int)
    requires A!=null; modifies A;
    requires 0<=i<A.Length && 0<=j<A.Length;
    ensures old(multiset(A[..]))==multiset(A[..]);

    ensures old(A[i])==A[j] && old(A[j])==A[i];
    ensures forall k:: 0<=k<A.Length && i!=k && j!=k ==> old(A[k])==A[k];

{ A[i],A[j]:= A[j],A[i]; }  

predicate Sorted(low:int,high:int)
    // reads A;
    // reads this.A;
    reads this; reads this.A; // Need both.
    requires A!=null;
    requires 0<=low && high<=A.Length;
{ forall i,j:: low<=i<j<high ==> A[i]<=A[j] }
}
Coordinator
Mar 18, 2014 at 2:59 AM
The "modifies" and "reads" clauses are analogous, as they govern modifications (in a method) and dependencies (of a function), respectively. Each specifies a "frame". The frame is specified by a set of object references. The modifies clause says that the method has license to modify the state of any of those objects, and the reads clause says that the function is allowed to depend on the state of any of those objects. (In addition, non-ghost methods are allowed to allocate new objects and modify their state.)

Syntactically, the argument to "modifies" and "reads" can be an expression whose type is a set of object references. But you can also list just an object reference, which Dafny will treat as the singleton set consisting of that reference. Moreover, you can give several arguments, with the effect of taking the union of these, and you can give multiple modifies/reads clauses, also with the effect of taking the union of these. So, if "r" is an object reference (let's say, of type "object") and "S" is a set of objects, each of the following lines means the same thing:
modifies S + {r};
modifies S, {r};
modifies S, r;
modifies S; modifies r;
Now, more specifically to your question.

Method Swap modifies the state of the array referenced by "this.A". Therefore, it suffices to say "modifies this.A" (or, equivalently, "modifies A"). In performing its job, Swap must read the "A" field of (the object referenced by) "this"--that is, it will read the state of "this". Also, because the right-hand side of the assignment in Swap reads elements of the array referenced by A, the Swap method also reads the state of "this.A". Methods are allowed to read whatever they want, so these reads do not need to be specified. Therefore, "modifies A" suffices.

If the method would sometimes also change the value of the "A" field, then it would be modifying the state of "this". In that case, the method would also have to declare "modifies this".

Function "Sorted" also reads the state of "this.A" (more precisely, it reads the elements of "A" with indices "[low..high]"). But, in order to read any element of the array referenced by "this.A", the body of "Sorted" must first obtain a reference to that array. It does so by reading the "A" field of the reference "this". In other words, "Sorted" is given the pointer "this", it dereferences "this" to read the reference stored in the "A" field (which necessitates "this" being in the "reads" clause), and then it dereferences "this.A" to get to the elements of the array (which necessitates "this.A" being in the "reads" clause).

One can concoct an example where "Sorted" will be able to read the elements of "this.A" without first dereferencing "this" in its body. (Maybe I should stop here and leave that as an exercise. :) But I'll go on.) To do so, "Sorted" would have to obtain the reference "this.A" some other way. If that other way goes via the object store (that is, the heap), then those reads will have to be declared in the "reads" clause as well. But it can also be done with an extra parameter, like this:
class QuickSort {
  var A: array<int>;

  predicate Sorted(low:int, high:int, a: array<int>)  // note the extra parameter "a"
    requires A != null && a == A;  // note the extra precondition "a == this.A"
    requires 0<=low && high<=A.Length;
    reads A;
  { forall i,j:: low<=i<j<high ==> a[i]<=a[j] }  // note that there is no use of "this" here
}
Rustan
Marked as answer by rustanleino on 3/17/2014 at 6:59 PM
Mar 18, 2014 at 11:11 AM
Thanks Rustan. In a nutshell, then, could the difference be that
Swap does not need to modify this.A in order to modify this.A[i], whereas
Sorted -does- need to read this.A in order to read this.A[i].
And that accounts for Swap's needing only one modifies clause, whereas Sorted needs two reads clauses.
Coordinator
Mar 18, 2014 at 5:58 PM
Precisely.
Aug 30, 2014 at 11:19 AM
Edited Aug 30, 2014 at 11:21 AM
Hi,
I found this example and discussion very useful in preparing new lectures on Dafny for my students.
I just would like to precise that the matter (in a nutshell) is:
Swap does not need to modify this in order to modify this.A. Therefore, it does not need "modifies this", but only "modifies A" (which is the same of "modifies this.A").

Sorted needs "reads this, this.A;"  because it need to "read this" in order to "read this.A".
Isn't it?

Thanks,
Paqui
Coordinator
Sep 10, 2014 at 12:43 AM
Correct, Paqui.
Coordinator
Sep 10, 2014 at 1:01 AM
With the recent addition of first-class functions (that is, higher-order functions) to Dafny, it became important to be stricter about reads clauses. Previously, there was no reads checking in reads and requires clauses of functions, but now there is. In particular, the reads clause now needs to mention all the things that are read (that is, depended on) by the reads clause itself and by the requires clause.

A consequence of the new rule is that you are no longer allowed to supply just the following:
reads this.A;
Instead, you also need to list that you are reading this. Here is the correct form:
reads this, this.A;
Under the new rule, my concocted Sorted predicate above is no longer accepted -- Dafny reports that you do not have license to read this.A in reads A;. An attempted fix of this would be to change the reads clause to reads a;, but that would instead produce a complaint that you do not have license to read this.A in the requires clause. The fix is thus to say:
reads this, A;
(or reads this, a;)

Rustan

PS. This new version of Dafny is checked in as source. This update will soon make it to rise4fun as well.