diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/Induction.dfy | 13 |
2 files changed, 14 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 0111f9af..5ee9f921 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -81,7 +81,7 @@ Dafny program verifier finished with 6 verified, 0 errors -------------------- Induction.dfy --------------------
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 29 verified, 0 errors
-------------------- Rippling.dfy --------------------
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 -----------------
|