1 files changed, 0 insertions, 26 deletions
diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy
deleted file mode 100644
index 585c998e..00000000
--- a/Test/dafny2/TuringFactorial.dfy
+++ /dev/null
@@ -1,26 +0,0 @@
-function Factorial(n: nat): nat
-{
-  if n == 0 then 1 else n * Factorial(n-1)
-}
-
-method ComputeFactorial(n: int) returns (u: int)
-  requires 1 <= n;
-  ensures u == Factorial(n);
-{
-  var r := 1;
-  u := 1;
-  while (r < n)  
-    invariant r <= n;
-    invariant u == Factorial(r);
-  { 
-    var v, s := u, 1;
-    while (s < r + 1)
-      invariant s <= r + 1;
-      invariant v == Factorial(r) && u == s * Factorial(r);
-    {
-      u := u + v;
-      s := s + 1;
-    }
-    r := r + 1;
-  }
-}