diff options
| author |  rustanleino <unknown> | 2011-03-05 04:04:39 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-05 04:04:39 +0000 |
| commit | 6834a1c28b973ded258ecf530efdc2a439890b6a (patch) | |
| tree | 2af5dd7fdd05979d375454c0f958aa4321316b47 /Test/dafny0/Termination.dfy | |
| parent | 4323f8e89d6f10730bcea0e2800f5e3a509b05de (diff) | |
Dafny: Added heuristic for when to turn on the induction tactic
Diffstat (limited to 'Test/dafny0/Termination.dfy')
| -rw-r--r-- | Test/dafny0/Termination.dfy | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 779c9892..226eadbe 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -310,5 +310,19 @@ function ReachBack(n: int): bool requires 0 <= n;
ensures ReachBack(n);
{
- (forall m :: 0 <= m && m < n ==> ReachBack(m))
+ // Turn off induction for this test, since that's not the point of
+ // the test case.
+ (forall m {:induction false} :: 0 <= m && m < n ==> ReachBack(m))
}
+
+function ReachBack_Alt(n: int): bool
+ requires 0 <= n;
+{
+ n == 0 || ReachBack_Alt(n-1)
+}
+
+ghost method Lemma_ReachBack()
+{
+ assert (forall m :: 0 <= m ==> ReachBack_Alt(m));
+}
+
|