diff options
| author |  rustanleino <unknown> | 2011-02-02 23:23:14 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-02 23:23:14 +0000 |
| commit | 9f2be05e55c8fcb8e753afb965ff242d79327691 (patch) | |
| tree | e5418c4c1217e763542dfdf36c0f26a059b5393f /Test/dafny1/TerminationDemos.dfy | |
| parent | 9d24f5281d326d92b3cc738bcc6e870ee43f1653 (diff) | |
Dafny: added ensures clauses to functions
Diffstat (limited to 'Test/dafny1/TerminationDemos.dfy')
| -rw-r--r-- | Test/dafny1/TerminationDemos.dfy | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index fb530258..76925e8e 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -30,6 +30,19 @@ 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);
+ {
+ if m == 0 then
+ n + 1
+ else if n == 0 then
+ G(m - 1, 1)
+ else
+ G(m - 1, G(m, n - 1))
+ }
+*/
}
// -----------------------------------
|