diff options
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/TerminationDemos.dfy | 22 |
2 files changed, 23 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d0eba7cb..0111f9af 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -65,7 +65,7 @@ Dafny program verifier finished with 4 verified, 0 errors -------------------- TerminationDemos.dfy --------------------
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 14 verified, 0 errors
-------------------- Substitution.dfy --------------------
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 01a7c7bd..49f5a075 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -42,6 +42,28 @@ class Ackermann { else
G(m - 1, G(m, n - 1))
}
+
+ function H(m: nat, n: nat): nat
+ {
+ if m == 0 then
+ n + 1
+ else if n == 0 then
+ H(m - 1, 1)
+ else
+ H(m - 1, H(m, n - 1))
+ }
+
+ method ComputeAck(m: nat, n: nat) returns (r: nat)
+ {
+ if (m == 0) {
+ r := n + 1;
+ } else if (n == 0) {
+ call r := ComputeAck(m - 1, 1);
+ } else {
+ call s := ComputeAck(m, n - 1);
+ call r := ComputeAck(m - 1, s);
+ }
+ }
}
// -----------------------------------
|