1 files changed, 0 insertions, 111 deletions
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
deleted file mode 100644
index 0aa36a10..00000000
--- a/Test/dafny1/TerminationDemos.dfy
+++ /dev/null
@@ -1,111 +0,0 @@
-class Example {
-  method M(n: int)
-  {
-    var i := 0;
-    while (i < n)
-    {
-      i := i + 1;
-    }
-  }
-}
-
-// -----------------------------------
-
-class Fibonacci {
-  function Fib(n: int): int
-  {
-    if n < 2 then n else Fib(n-2) + Fib(n-1)
-  }
-}
-
-// -----------------------------------
-
-class Ackermann {
-  function F(m: int, n: int): int
-  {
-    if m <= 0 then
-      n + 1
-    else if n <= 0 then
-      F(m - 1, 1)
-    else
-      F(m - 1, F(m, n - 1))
-  }
-
-  function G(m: int, n: int): int
-    requires 0 <= m && 0 <= n;
-    ensures 0 <= G(m, n);
-  {
-    if m == 0 then
-      n + 1
-    else if n == 0 then
-      G(m - 1, 1)
-    else
-      G(m - 1, G(m, n - 1))
-  }
-
-  function H(m: nat, n: nat): nat
-  {
-    if m == 0 then
-      n + 1
-    else if n == 0 then
-      H(m - 1, 1)
-    else
-      H(m - 1, H(m, n - 1))
-  }
-
-  method ComputeAck(m: nat, n: nat) returns (r: nat)
-  {
-    if (m == 0) {
-      r := n + 1;
-    } else if (n == 0) {
-      r := ComputeAck(m - 1, 1);
-    } else {
-      var s := ComputeAck(m, n - 1);
-      r := ComputeAck(m - 1, s);
-    }
-  }
-}
-
-// -----------------------------------
-
-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()
-  }
-}