Dafny:

* Added modules with imports.  These can be used to deal with termination checks without going into method/function implementations.  Imports must be acyclic.

* Added a default module.  It contains all classes/datatypes defined outside the lexical scope of any other module.

* Added a default class.  It contains all class members defined outside the lexical scope of any module and class.  This means that one can write small Dafny programs without any mention of a "class"!

* Revised scheme for termination metrics.  Inter-module calls are allowed iff they follow the import relation.  Intra-module calls where the callee is in another strongly connected component of the call graph are always allowed.  Intra-module calls in the same strongly connected component are verified to terminate via decreases clauses.

* Removed previous hack that allowed methods with no decreases clauses not to be subjected to termination checking.

* Removed or simplified decreases clauses in test suite, where possible.

* Fixed error in Test/VSI-Benchmarks/b1.dfy

1 files changed, 4 insertions, 2 deletions

diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index f429b9ed..97317792 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -36,6 +36,7 @@ class Main {
     requires (forall n :: n in S && n.marked ==>

                 n in stackNodes ||

                 (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

+    requires (forall n :: n in stackNodes ==> n != null && n.marked);

     modifies S;

     ensures root.marked;

     // nodes reachable from 'root' are marked:

@@ -46,6 +47,7 @@ class Main {
     ensures (forall n :: n in S ==>

                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

+    decreases S - stackNodes;

   {

     if (! root.marked) {

       root.marked := true;

@@ -66,6 +68,7 @@ class Main {
       {

         var c := root.children[i];

         if (c != null) {

+          var D := S - stackNodes;  assert root in D;

           call RecursiveMarkWorker(c, S, stackNodes + {root});

         }

         i := i + 1;

@@ -146,7 +149,6 @@ class Main {
   function Reachable(from: Node, to: Node, S: set<Node>): bool

     requires null !in S;

     reads S;

-    decreases 1;

   {

     (exists via: Path :: ReachableVia(from, via, to, S))

   }

@@ -154,7 +156,7 @@ class Main {
   function ReachableVia(from: Node, via: Path, to: Node, S: set<Node>): bool

     requires null !in S;

     reads S;

-    decreases 0, via;

+    decreases via;

   {

     match via

     case Empty => from == to