summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar leino <unknown>2016-04-01 14:58:14 -0700
committerGravatar leino <unknown>2016-04-01 14:58:14 -0700
commitfeeca51eca5daf1025a3e941887725a7060d1265 (patch)
treefda2dba5c175cbe0a91640a4b843d8e6b46ee844
parent3fdaa8a4562929f0202c582699d574f1a7beefac (diff)
New test file, for recursive and iterative versions of McCarthy's 91 function
-rw-r--r--Test/dafny4/McCarthy91.dfy86
-rw-r--r--Test/dafny4/McCarthy91.dfy.expect25
2 files changed, 111 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;
+}
diff --git a/Test/dafny4/McCarthy91.dfy.expect b/Test/dafny4/McCarthy91.dfy.expect
new file mode 100644
index 00000000..bbc91c35
--- /dev/null
+++ b/Test/dafny4/McCarthy91.dfy.expect
@@ -0,0 +1,25 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
+Program compiled successfully
+Running...
+
+M(3) = 91
+M(99) = 91
+M(100) = 91
+M(101) = 91
+M(1013) = 1003
+mc91(3) = 91
+mc91(99) = 91
+mc91(100) = 91
+mc91(101) = 91
+mc91(1013) = 1003
+Mc91(3) = 91
+Mc91(99) = 91
+Mc91(100) = 91
+Mc91(101) = 91
+Mc91(1013) = 1003
+iter(0, mc91, 40) = 40
+iter(1, mc91, 40) = 91
+iter(2, mc91, 40) = 91
+iter(3, mc91, 40) = 91
+iter(4, mc91, 40) = 91