diff options
| author |  leino <unknown> | 2016-04-01 14:58:14 -0700 |
|---|---|---|
| committer | leino <unknown> | 2016-04-01 14:58:14 -0700 |
| commit | feeca51eca5daf1025a3e941887725a7060d1265 (patch) | |
| tree | fda2dba5c175cbe0a91640a4b843d8e6b46ee844 /Test | |
| parent | 3fdaa8a4562929f0202c582699d574f1a7beefac (diff) | |
New test file, for recursive and iterative versions of McCarthy's 91 function
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny4/McCarthy91.dfy | 86 | ||||
| -rw-r--r-- | Test/dafny4/McCarthy91.dfy.expect | 25 |
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 |