diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-16 11:49:01 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-16 11:49:01 -0700 |
| commit | 2b24e9d819cf4b00b06f2dce68766200768ed609 (patch) | |
| tree | 29cd499ebd450d9d25ec02042d4631df48f7d453 /Test/dafny1 | |
| parent | 650ad1ee685b599b08717a3d83a31c0689b006e9 (diff) | |
Dafny: added some test cases that use nat
Diffstat (limited to 'Test/dafny1')
| -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);
+ }
+ }
}
// -----------------------------------
|