diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 18:31:53 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 18:31:53 -0700 |
| commit | 1acd05253ea0fc614ac3e6a612be19a3f3bcf6a4 (patch) | |
| tree | 690ff82d9e2764aa54a076ad895bad0858dc25d1 /Test/dafny1/Induction.dfy | |
| parent | 3e31a8d7c1445748450c258a50160c37e112a702 (diff) | |
Dafny: fixed bug in induction-tactic heuristic (should never pick values whose type is a type parameter)
Diffstat (limited to 'Test/dafny1/Induction.dfy')
| -rw-r--r-- | Test/dafny1/Induction.dfy | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index d785eead..7c7d3baf 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -156,6 +156,19 @@ class DatatypeInduction<T> { }
// see also Test/dafny0/DTypes.dfy for more variations of this example
+
+ function OccurrenceCount<T>(tree: Tree<T>, x: T): int
+ {
+ match tree
+ case Leaf(t) => if x == t then 1 else 0
+ case Branch(left, right) => OccurrenceCount(left, x) + OccurrenceCount(right, x)
+ }
+ method RegressionTest(tree: Tree<T>)
+ // the translation of the following line once crashed Dafny
+ requires forall y :: 0 <= OccurrenceCount(tree, y);
+ {
+ }
+
}
// ----------------------- Induction and case splits -----------------
|