From cf44e57370a6043b5a3409d6683610dc872f13e9 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 4 Aug 2013 23:16:47 -0700 Subject: Allow co-predicates to be wrapped inside bounded existential quantifiers --- Source/Dafny/Resolver.cs | 18 ++++++++---------- Test/dafny0/Answer | 17 ++++++++++++----- Test/dafny0/Coinductive.dfy | 28 ++++++++++++++++++++++++++++ 3 files changed, 48 insertions(+), 15 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 94ff6dd3..81980936 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1865,10 +1865,10 @@ namespace Microsoft.Dafny if (!(e.Function is CoPredicate)) { Error(e, "a recursive call from a copredicate can go only to other copredicates"); } else if (cp != CallingPosition.Positive) { - var msg = "a recursive copredicate call can only be done in positive positions"; + var msg = "a copredicate can be called recursively only in positive positions"; if (cp == CallingPosition.Neither) { - // this may be inside a - msg += " and cannot sit inside an existential quantifier"; + // this may be inside an existential quantifier + msg += " and cannot sit inside an unbounded existential quantifier"; } else { // the co-call is not inside an existential quantifier, so don't bother mentioning the part of existentials in the error message } @@ -1921,14 +1921,12 @@ namespace Microsoft.Dafny } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; if ((cp == CallingPosition.Positive && e is ExistsExpr) || (cp == CallingPosition.Negative && e is ForallExpr)) { - // Don't allow any co-recursive calls under an existential, because that can be unsound. - // (TODO: be more liberal here--also allow this if the range is finite) - cp = CallingPosition.Neither; - } - if (e.Range != null) { - Visit(e.Range, e is ExistsExpr ? Invert(cp) : cp); + if (e.MissingBounds != null && e.MissingBounds.Count != 0) { + // Don't allow any co-recursive calls under an existential with an unbounded range, because that can be unsound. + cp = CallingPosition.Neither; + } } - Visit(e.Term, cp); + Visit(e.LogicalBody(), cp); return false; } else if (expr is ConcreteSyntaxExpression) { // do the sub-parts with the same "cp" 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) { !Even(s) // here, negation is fine -- cgit v1.2.3