diff options
| author |  rustanleino <unknown> | 2011-02-03 18:17:08 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-03 18:17:08 +0000 |
| commit | b8b0627fcb22c5637829e564ea2f42f44d4b8097 (patch) | |
| tree | a4679069d1bda862d9f737740d9eb0aaa8eacdde /Test | |
| parent | b80c92bd5549e6c789764758dd90f0f74928d39a (diff) | |
Dafny: implemented a more precise scheme for allowing use of a function's rep axiom
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/TerminationDemos.dfy | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 5b51b3e4..d737a8cd 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -53,7 +53,7 @@ Dafny program verifier finished with 17 verified, 0 errors -------------------- TerminationDemos.dfy --------------------
-Dafny program verifier finished with 10 verified, 0 errors
+Dafny program verifier finished with 11 verified, 0 errors
-------------------- Substitution.dfy --------------------
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 76925e8e..01a7c7bd 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -30,7 +30,7 @@ class Ackermann { else
F(m - 1, F(m, n - 1))
}
-/*
+
function G(m: int, n: int): int
requires 0 <= m && 0 <= n;
ensures 0 <= G(m, n);
@@ -42,7 +42,6 @@ class Ackermann { else
G(m - 1, G(m, n - 1))
}
-*/
}
// -----------------------------------
|