Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts)

1 files changed, 21 insertions, 0 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 4e3fab69..87bfd35f 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -85,6 +85,27 @@ class Modifies {
     }

   }

 

+  method Aprime(p: Modifies)

+    modifies this, p;

+  {

+    x := x + 1;

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

+      decreases if p != null then 75 - p.x else 0;  // given explicitly (but see Adoubleprime below)

+    {

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

+    }

+  }

+

+  method Adoubleprime(p: Modifies)

+    modifies this, p;

+  {

+    x := x + 1;

+    while (p != null && p.x < 75)  // here, the decreases clause is heuristically inferred (to be the

+    {                              // same as the one in Aprime above)

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

+    }

+  }

+

   method B(p: Modifies)

     modifies this;

   {