Dafny: cleaned up test scripts a little

1 files changed, 26 insertions, 0 deletions

diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy
new file mode 100644
index 00000000..585c998e
--- /dev/null
+++ b/Test/dafny2/TuringFactorial.dfy
@@ -0,0 +1,26 @@
+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;

+  }

+}