Dafny:

* Added "decreases" clauses to methods.
* Interpret the filename stdin.dfy as an indication to read the program from standard input.

4 files changed, 92 insertions, 9 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 540bcb4b..95302b05 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -8,8 +8,7 @@ class MyClass<T, U> {
   method M(s: bool, lotsaObjects: set<object>)

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

     requires s;

-    modifies this;

-    modifies lotsaObjects;

+    modifies this, lotsaObjects;

     ensures t == t;

     ensures old(null) != this;

   {

@@ -195,3 +194,7 @@ Dafny program verifier finished with 7 verified, 0 errors
 -------------------- SumOfCubes.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- TerminationDemos.dfy --------------------

+

+Dafny program verifier finished with 7 verified, 0 errors

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 54a98a56..5f56cf40 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -1,6 +1,6 @@
 class IntSet {

-  var contents: set<int>;

-  var footprint: set<object>;

+  ghost var contents: set<int>;

+  ghost var footprint: set<object>;

 

   var root: Node;

 

@@ -48,7 +48,7 @@ class IntSet {
     footprint := root.footprint + {this};

   }

 

-  method InsertHelper(x: int, n: Node) returns (m: Node)

+  class method InsertHelper(x: int, n: Node) returns (m: Node)

     requires n == null || n.Valid();

     modifies n.footprint;

     ensures m != null && m.Valid();

@@ -97,9 +97,9 @@ class IntSet {
 }

 

 class Node {

-  var contents: set<int>;

-  var footprint: set<object>;

-  

+  ghost var contents: set<int>;

+  ghost var footprint: set<object>;

+

   var data: int;

   var left: Node;

   var right: Node;

diff --git a/Test/dafny0/TerminationDemos.dfy b/Test/dafny0/TerminationDemos.dfy
new file mode 100644
index 00000000..6b63bfec
--- /dev/null
+++ b/Test/dafny0/TerminationDemos.dfy
@@ -0,0 +1,80 @@
+class Example {

+  method M(n: int)

+  {

+    var i := 0;

+    while (i < n)

+      decreases n - i;

+    {

+      i := i + 1;

+    }

+  }

+}

+

+// -----------------------------------

+

+class Fibonacci {

+  function Fib(n: int): int

+    decreases n;

+  {

+    if n < 2 then n else Fib(n-2) + Fib(n-1)

+  }

+}

+

+// -----------------------------------

+

+class Ackermann {

+  function F(m: int, n: int): int

+    decreases m, n;

+  {

+    if m <= 0 then

+      n + 1

+    else if n <= 0 then

+      F(m - 1, 1)

+    else

+      F(m - 1, F(m, n - 1))

+  }

+}

+

+// -----------------------------------

+

+class List {

+  var data: int;

+  var next: List;

+  ghost var ListNodes: set<List>;

+  function IsAcyclic(): bool

+    reads *;

+    decreases ListNodes;

+  {

+    this in ListNodes &&

+    (next != null ==>

+      next.ListNodes <= ListNodes && this !in next.ListNodes &&

+      next.IsAcyclic())

+  }

+

+  method Singleton(x: int) returns (list: List)

+    ensures list != null && list.IsAcyclic();

+  {

+    list := new List;

+    list.data := x;

+    list.next := null;

+    list.ListNodes := {list};

+  }

+

+  method Prepend(x: int, tail: List) returns (list: List)

+    requires tail == null || tail.IsAcyclic();

+    ensures list != null && list.IsAcyclic();

+  {

+    list := new List;

+    list.data := x;

+    list.next := tail;

+    list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes;

+  }

+

+  function Sum(): int

+    requires IsAcyclic();

+    reads *;

+    decreases ListNodes;

+  {

+    if next == null then data else data + next.Sum()

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 64efe27b..c1837b43 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -21,7 +21,7 @@ for %%f in (TypeTests.dfy SmallTests.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

-            SumOfCubes.dfy) do (

+            SumOfCubes.dfy TerminationDemos.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% %* %%f