1 files changed, 86 insertions, 0 deletions
diff --git a/Test/dafny4/McCarthy91.dfy b/Test/dafny4/McCarthy91.dfy
new file mode 100644
index 00000000..2e599f0d
--- /dev/null
+++ b/Test/dafny4/McCarthy91.dfy
@@ -0,0 +1,86 @@
+// RUN: %dafny /compile:3 /rprint:"%t.rprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// The usual recursive method for computing McCarthy's 91 function
+
+method Main() {
+  var s := [3, 99, 100, 101, 1013];
+
+  var n := 0;
+  while n < |s| {
+    var m := M(s[n]);
+    print "M(", s[n], ") = ", m, "\n";
+    n := n + 1;
+  }
+
+  n := 0;
+  while n < |s| {
+    print "mc91(", s[n], ") = ", mc91(s[n]), "\n";
+    n := n + 1;
+  }
+
+  n := 0;
+  while n < |s| {
+    var m := Mc91(s[n]);
+    print "Mc91(", s[n], ") = ", m, "\n";
+    n := n + 1;
+  }
+
+  n := 0;
+  while n < 5 {
+    var m := iter(n, mc91, 40);
+    print "iter(", n, ", mc91, 40) = ", m, "\n";
+    n := n + 1;
+  }
+}
+
+method M(n: int) returns (r: int)
+  ensures r == if n <= 100 then 91 else n - 10
+  decreases 100 - n
+{
+  if n <= 100 {
+    r := M(n + 11);
+    r := M(r);
+  } else {
+    r := n - 10;
+  }
+}
+
+// Same as above, but as a function
+
+function method mc91(n: int): int
+  ensures n <= 100 ==> mc91(n) == 91
+  decreases 100 - n
+{
+  if n <= 100 then
+    mc91(mc91(n + 11))
+  else
+    n - 10
+}
+
+// Iterating a function f e times starting from n
+
+function method iter(e: nat, f: int -> int, n: int): int
+  requires forall x :: f.requires(x) && f.reads(x) == {}
+{
+  if e == 0 then n else iter(e-1, f, f(n))
+}
+
+// Iterative version of McCarthy's 91 function, following in lockstep
+// what the recursive version would do
+
+method Mc91(n0: int) returns (r: int)
+  ensures r == mc91(n0)
+{
+  var e, n := 1, n0;
+  while e > 0
+    invariant iter(e, mc91, n) == mc91(n0)
+    decreases 100 - n + 10 * e, e
+  {
+    if n <= 100 {
+      e, n := e+1, n+11;
+    } else {
+      e, n := e-1, n-10;
+    }
+  }
+  return n;
+}