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

9 files changed, 174 insertions, 25 deletions

diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index ba293008..70522aaf 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -35,8 +35,11 @@ class Benchmark1 {
 

   method Mul(x: int, y: int) returns (r: int)

     ensures r == x*y;

+    decreases x < 0, x;

   {

-    if (x < 0) {

+    if (x == 0) {

+      r := 0;

+    } else if (x < 0) {

       call r := Mul(-x, y);

       r := -r;

     } else {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5dadda4b..ae2aa454 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -6,7 +6,7 @@ class MyClass<T, U> {
   var x: int;

 

   method M(s: bool, lotsaObjects: set<object>)

-      returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>):

+      returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)

     requires s;

     modifies this, lotsaObjects;

     ensures t == t;

@@ -266,10 +266,24 @@ Execution trace:
 Dafny program verifier finished with 21 verified, 29 errors

 

 -------------------- Modules0.dfy --------------------

+Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

 Modules0.dfy(13,7): Error: module T named among imports does not exist

 Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G

-Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

-3 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)

+Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)

+Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)

+Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module $default must transitively import YY)

+7 resolution/type errors detected in Modules0.dfy

+

+-------------------- Modules1.dfy --------------------

+Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0

+Execution trace:

+    (0,0): anon0

+Modules1.dfy(61,3): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 16 verified, 2 errors

 

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

 

@@ -300,31 +314,31 @@ Dafny program verifier finished with 10 verified, 0 errors
 Dafny program verifier finished with 13 verified, 0 errors

 

 -------------------- Use.dfy --------------------

-Use.dfy(15,18): Error: assertion violation

+Use.dfy(14,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(26,18): Error: assertion violation

+Use.dfy(24,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(35,18): Error: assertion violation

+Use.dfy(33,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(56,12): Error: assertion violation

+Use.dfy(52,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(88,17): Error: assertion violation

+Use.dfy(82,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(130,23): Error: assertion violation

+Use.dfy(124,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(144,5): Error: assertion violation

+Use.dfy(136,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(144,5): Error: assertion violation

+Use.dfy(136,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(215,19): Error: assertion violation

+Use.dfy(207,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 276b6c0e..714e9d58 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -55,6 +55,7 @@ class IntSet {
     ensures n == null ==> fresh(m.footprint) && m.contents == {x};

     ensures n != null ==> m == n && n.contents == old(n.contents) + {x};

     ensures n != null ==> fresh(n.footprint - old(n.footprint));

+    decreases if n == null then {} else n.footprint;

   {

     if (n == null) {

       m := new Node;

@@ -145,6 +146,7 @@ class Node {
   method Find(x: int) returns (present: bool)

     requires Valid();

     ensures present <==> x in contents;

+    decreases footprint;

   {

     if (x == data) {

       present := true;

@@ -164,6 +166,7 @@ class Node {
     ensures node != null ==> node.Valid();

     ensures node == null ==> old(contents) <= {x};

     ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {x};

+    decreases footprint;

   {

     node := this;

     if (left != null && x < data) {

@@ -201,6 +204,7 @@ class Node {
     ensures node == null ==> old(contents) == {min};

     ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {min};

     ensures min in old(contents) && (forall x :: x in old(contents) ==> min <= x);

+    decreases footprint;

   {

     if (left == null) {

       min := data;

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index cf616fba..0e0d3ab3 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -32,3 +32,75 @@ module I imports J {
 

 module J imports G, M {

 }

+

+// --------------- calls

+

+module X2 imports X1 {

+  class MyClass2 {

+    method Down(x1: MyClass1, x0: MyClass0) {

+      call x1.Down(x0);

+    }

+    method WayDown(x0: MyClass0, g: ClassG) {

+      call x0.Down();

+      call g.T();  // allowed, because this follows import relation

+      var t := g.TFunc();  // allowed, because this follows import relation

+    }

+    method Up() {

+    }

+    method Somewhere(y: MyClassY) {

+      call y.M();  // error: does not follow import relation

+    }

+  }

+}

+

+module X1 imports X0 {

+  class MyClass1 {

+    method Down(x0: MyClass0) {

+      call x0.Down();

+    }

+    method Up(x2: MyClass2) {

+      call x2.Up();  // error: does not follow import relation

+    }

+  }

+}

+

+module X0 {

+  class MyClass0 {

+    method Down() {

+    }

+    method Up(x1: MyClass1, x2: MyClass2) {

+      call x1.Up(x2);  // error: does not follow import relation

+    }

+  }

+}

+

+module YY {

+  class MyClassY {

+    method M() { }

+    method P(g: ClassG) {

+      call g.T();  // allowed, because this follows import relation

+      var t := g.TFunc();  // allowed, because this follows import relation

+    }

+  }

+}

+

+class ClassG {

+  method T() { }

+  function method TFunc(): int { 10 }

+  method V(y: MyClassY) {

+    call y.M();  // error: does not follow import relation

+  }

+}

+

+method Ping() {

+  call Pong();  // allowed: intra-module call

+}

+

+method Pong() {

+  call Ping();  // allowed: intra-module call

+}

+

+method ProcG(g: ClassG) {

+  call g.T();  // allowed: intra-module call

+  var t := g.TFunc();  // allowed: intra-module call

+}

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
new file mode 100644
index 00000000..cfefa7fa
--- /dev/null
+++ b/Test/dafny0/Modules1.dfy
@@ -0,0 +1,62 @@
+module A imports B {

+  class X {

+    function Fx(z: Z): int

+      requires z != null;

+      decreases 5, 4, 3;

+    { z.G() }  // fine; this goes to a different module

+  }

+  datatype Y {

+    Cons(int, Y);

+    Empty;

+  }

+}

+

+class C {

+  method M() { }

+  function F(): int { 818 }

+}

+

+method MyMethod() { }

+

+var MyField: int;

+

+module B {

+  class Z {

+    method K() { }

+    function G(): int

+      decreases 10, 8, 6;

+    { 25 }

+  }

+}

+

+static function MyFunction(): int { 5 }

+

+class D { }

+

+method Proc0(x: int)

+  decreases x;

+{

+  if (0 <= x) {

+    call Proc1(x - 1);

+  }

+}

+

+method Proc1(x: int)

+  decreases x;

+{

+  if (0 <= x) {

+    call Proc0(x - 1);

+  }

+}

+

+method Botch0(x: int)

+  decreases x;

+{

+  call Botch1(x - 1);  // error: failure to keep termination metric bounded

+}

+

+method Botch1(x: int)

+  decreases x;

+{

+  call Botch0(x);  // error: failure to decrease termination metric

+}

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

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index b627df75..ba6c8e0c 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -2,7 +2,7 @@ class Node {
   var next: Node;

 

   function IsList(r: set<Node>): bool

-    reads r; 

+    reads r;

   {

     this in r &&

     (next != null  ==>  next.IsList(r - {this}))

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index e006823e..58cb6bea 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -2,7 +2,6 @@ class T {
   var x: int;

 

   use function F(y: int): int

-    decreases 0;

   {

     2*y

   }

@@ -16,7 +15,6 @@ class T {
   }

 

   use function FF(y: int): int

-    decreases 1;

   {

     F(y)

   }

@@ -36,12 +34,10 @@ class T {
   }

 

   use function G(y: int): bool

-    decreases 0;

   {

     0 <= y

   }

   use function GG(y: int): bool

-    decreases 1;

   {

     G(y)

   }

@@ -58,13 +54,11 @@ class T {
 

   use function H(): int

     reads this;

-    decreases 0;

   {

     x

   }

   use function HH(): int

     reads this;

-    decreases 1;

   {

     H()

   }

@@ -133,13 +127,11 @@ class T {
 

   use function K(): bool

     reads this;

-    decreases 0;

   {

     x <= 100

   }

   use function KK(): bool

     reads this;

-    decreases 1;

   {

     K()

   }

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 2bec0a4d..003566f3 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (BQueue.bpl) do (
 )

 

 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy

-            Modules0.dfy Queue.dfy ListCopy.dfy

+            Modules0.dfy Modules1.dfy Queue.dfy ListCopy.dfy

             BinaryTree.dfy ListReverse.dfy ListContents.dfy

             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy