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 | |
| parent | 5dfb4de30b28fa239dcaeff23b21a8d97df70f4d (diff) | |
Allow co-predicates to be wrapped inside bounded existential quantifiers
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 17 | ||||
| -rw-r--r-- | Test/dafny0/Coinductive.dfy | 28 |
2 files changed, 40 insertions, 5 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index b462465d..7e5baa4b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1195,11 +1195,18 @@ Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
-Coinductive.dfy(90,8): Error: a recursive copredicate call can only be done in positive positions
-Coinductive.dfy(91,8): Error: a recursive copredicate call can only be done in positive positions
-Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier
-Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier
-8 resolution/type errors detected in Coinductive.dfy
+Coinductive.dfy(90,8): Error: a copredicate can be called recursively only in positive positions
+Coinductive.dfy(91,8): Error: a copredicate can be called recursively only in positive positions
+Coinductive.dfy(92,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(92,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(98,5): Error: a copredicate can be called recursively only in positive positions
+Coinductive.dfy(101,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(102,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(103,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(113,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(119,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(120,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+15 resolution/type errors detected in Coinductive.dfy
-------------------- Corecursion.dfy --------------------
Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)
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
|