Dafny:

* Modifies clause checking is now done with each update, instead of at the end of the method.  Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time.
* bugfix: range expressions of foreach statements were previously ignored during Translation

3 files changed, 106 insertions, 6 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index e3a91ab2..d45db684 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -10,8 +10,6 @@
 // pperm, had to write invariants over p and perm rather than pperm and we couldn't use 

 // "x in p".

 

-//would be nice if we could mark pperm as a ghost variable

-

 class Queue<T> {

   var contents: seq<T>;

   method Init();

@@ -43,7 +41,7 @@ class Comparable {
 class Benchmark3 {

 

 

-  method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)

+  method Sort(q: Queue<int>) returns (r: Queue<int>, ghost perm:seq<int>)

     requires q != null;

     modifies q;

     ensures r != null && fresh(r);

@@ -59,7 +57,7 @@ class Benchmark3 {
   {

     r := new Queue<int>;

     call r.Init();

-    var p:= [];

+    ghost var p:= [];

     

     var n := 0;

 	while (n < |q.contents|)

@@ -72,7 +70,7 @@ class Benchmark3 {
 		n := n + 1;

    }

    perm:= [];

-   var pperm := p + perm; 

+   ghost var pperm := p + perm; 

    

     while (|q.contents| != 0)

       invariant |r.contents| == |old(q.contents)| - |q.contents|;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1edbeedc..d46dc7fe 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -98,8 +98,26 @@ Execution trace:
     (0,0): anon3

     (0,0): anon11_Then

     (0,0): anon6

+SmallTests.dfy(95,5): Error: call may violate caller's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

+SmallTests.dfy(108,7): Error: call may violate caller's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+SmallTests.dfy(110,7): Error: call may violate caller's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+SmallTests.dfy(150,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

 

-Dafny program verifier finished with 6 verified, 4 errors

+Dafny program verifier finished with 10 verified, 8 errors

 

 -------------------- Queue.dfy --------------------

 

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 6ac9879d..3a2ca13c 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -67,3 +67,87 @@ class Node {
     12

   }

 }

+

+// ------------------ modifies clause tests ------------------------

+

+class Modifies {

+  var x: int;

+  var next: Modifies;

+

+  method A(p: Modifies)

+    modifies this, p;

+  {

+    x := x + 1;

+    while (p != null && p.x < 75)

+      decreases 75 - p.x;

+    {

+      p.x := p.x + 1;

+    }

+  }

+

+  method B(p: Modifies)

+    modifies this;

+  {

+    call A(this);

+    if (p == this) {

+      call p.A(p);

+    }

+    call A(p);  // error: may violate modifies clause

+  }

+

+  method C(b: bool)

+    modifies this;

+    ensures !b ==> x == old(x) && next == old(next);

+  {

+  }

+

+  method D(p: Modifies, y: int)

+    requires p != null;

+  {

+    if (y == 3) {

+      call p.C(true);  // error: may violate modifies clause

+    } else {

+      call p.C(false);  // error: may violation modifies clause (the check is done without regard

+                        // for the postcondition, which also makes sense, since there may, in

+                        // principle, be other fields of the object that are not constrained by the

+                        // postcondition)

+    }

+  }

+

+  method E()

+    modifies this;

+  {

+    call A(null);  // allowed

+  }

+

+  method F(s: set<Modifies>)

+    modifies s;

+  {

+    foreach (m in s | 2 <= m.x) {

+      m.x := m.x + 1;

+    }

+    if (this in s) {

+      x := 2 * x;

+    }

+  }

+

+  method G(s: set<Modifies>)

+    modifies this;

+  {

+    var m := 3;  // this is a different m

+

+    foreach (m in s | m == this) {

+      m.x := m.x + 1;

+    }

+    if (s <= {this}) {

+      foreach (m in s) {

+        m.x := m.x + 1;

+      }

+      call F(s);

+    }

+    foreach (m in s) {

+      assert m.x < m.x + 10;  // nothing wrong with asserting something

+      m.x := m.x + 1;  // error: may violate modifies clause

+    }

+  }

+}