diff options
| author |  Rustan Leino <unknown> | 2013-08-04 23:16:47 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-04 23:16:47 -0700 |
| commit | cf44e57370a6043b5a3409d6683610dc872f13e9 (patch) | |
| tree | 0e9d19446af092ed6b6eef34589aa83b2c3ce758 /Test/dafny0/Coinductive.dfy | |
| parent | 5dfb4de30b28fa239dcaeff23b21a8d97df70f4d (diff) | |
Allow co-predicates to be wrapped inside bounded existential quantifiers
Diffstat (limited to 'Test/dafny0/Coinductive.dfy')
| -rw-r--r-- | Test/dafny0/Coinductive.dfy | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy index 4d197dd7..b31dc5be 100644 --- a/Test/dafny0/Coinductive.dfy +++ b/Test/dafny0/Coinductive.dfy @@ -92,6 +92,34 @@ module CoPredicateResolutionErrors { && (Even(s) <==> Even(s)) // error (x2): recursive copredicate calls allowed only in positive positions
}
+ copredicate CP(i: int)
+ {
+ CP(i) &&
+ !CP(i) && // error: not in a positive position
+ (forall j :: CP(j)) &&
+ (exists k :: 0 <= k < i*i && CP(k)) &&
+ (exists k :: 0 <= k && CP(k)) && // error: unbounded range
+ (exists k :: k < i*i && CP(k)) && // error: unbounded range
+ (exists l :: CP(l)) // error: unbounded range
+ }
+
+ copredicate CQ(i: int, j: int)
+ {
+ exists i :: i == 6 && if j % 2 == 0 then CQ(i, i) else CQ(j, j)
+ }
+
+ copredicate CR(i: int, j: int)
+ {
+ exists i :: i == if CR(i, j) then 6 else j // error: not allowed to call CR recursively here
+ }
+
+ copredicate CS(i: int, j: int)
+ {
+ exists i ::
+ i <= (if CS(i, j) then 6 else j) && // error: not allowed to call CS recursively here
+ (if CS(i, j) then 6 else j) <= i // error: not allowed to call CS recursively here
+ }
+
copredicate Another(s: Stream<int>)
{
!Even(s) // here, negation is fine
|