diff options
| author |  Rustan Leino <unknown> | 2014-02-23 21:39:57 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-23 21:39:57 -0800 |
| commit | 297f9d4f1b409b2204b536f8393db3f6ccec18e2 (patch) | |
| tree | 36a23fdbd252203ed66afe8781fdc1781ce87517 /Test/dafny0/Coinductive.dfy | |
| parent | c09533b5979a46e8fbb5944e00d26b55594c9d3e (diff) | |
Fixed some checking of recursive method/copredicate calls
Diffstat (limited to 'Test/dafny0/Coinductive.dfy')
| -rw-r--r-- | Test/dafny0/Coinductive.dfy | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy index 27b279c3..d6466f73 100644 --- a/Test/dafny0/Coinductive.dfy +++ b/Test/dafny0/Coinductive.dfy @@ -129,6 +129,27 @@ module CoPredicateResolutionErrors { ensures Even(Doubles(n));
{
}
+
+ copredicate CoStmtExpr_Good(s: Stream<int>)
+ {
+ s.head > 0 && (MyLemma(s.head); CoStmtExpr_Good(s.tail))
+ }
+
+ lemma MyLemma(x: int)
+ {
+ }
+
+ copredicate CoStmtExpr_Bad(s: Stream<int>)
+ {
+ s.head > 0 &&
+ (MyRecursiveLemma(s.head); // error: cannot call method recursively from copredicate
+ CoStmtExpr_Bad(s.tail))
+ }
+
+ lemma MyRecursiveLemma(x: int)
+ {
+ var p := CoStmtExpr_Bad(Upward(x));
+ }
}
// --------------------------------------------------
|