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/dafny1/TerminationDemos.dfy | |
| parent | b80c92bd5549e6c789764758dd90f0f74928d39a (diff) | |
Dafny: implemented a more precise scheme for allowing use of a function's rep axiom
Diffstat (limited to 'Test/dafny1/TerminationDemos.dfy')
| -rw-r--r-- | Test/dafny1/TerminationDemos.dfy | 3 |
1 files changed, 1 insertions, 2 deletions
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))
}
-*/
}
// -----------------------------------
|