diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 21 | ||||
| -rw-r--r-- | Test/dafny3/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny3/SimpleCoinduction.dfy | 12 |
4 files changed, 32 insertions, 10 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index cc26eea2..4b5fef51 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -271,6 +271,13 @@ namespace Microsoft.Dafny fn.IsRecursive = true;
}
}
+ if (fn.IsRecursive && fn is CoPredicate) {
+ // this means the corresponding prefix predicate is also recursive
+ var prefixPred = ((CoPredicate)fn).PrefixPredicate;
+ if (prefixPred != null) {
+ prefixPred.IsRecursive = true;
+ }
+ }
}
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index afc075e5..684841e6 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -9093,13 +9093,20 @@ namespace Microsoft.Dafny { var exp = e.Args[i];
if (DafnyOptions.O.InductionHeuristic < 6) {
variantArgument = rec;
- } else if (f is ImplicitFormal) {
- variantArgument = true;
- } else {
- // The argument position is considered to be "variant" if the function is recursive and the argument participates
- // in the effective decreases clause of the function. The argument participates if it's a free variable
- // of a term in the explicit decreases clause.
- variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, false, f));
+ } else if (rec) {
+ // The argument position is considered to be "variant" if the function is recursive and...
+ // ... it has something to do with why the callee is well-founded, which happens when...
+ if (f is ImplicitFormal) {
+ // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix method, or
+ variantArgument = true;
+ } else if (decr.Exists(ee => ContainsFreeVariable(ee, false, f))) {
+ // ... it participates in the effective decreases clause of the function, which happens when it is
+ // a free variable of a term in the explicit decreases clause, or
+ variantArgument = true;
+ } else {
+ // ... the callee is a prefix predicate.
+ variantArgument = true;
+ }
}
if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) {
return true;
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index c4e75986..418ca164 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -17,7 +17,7 @@ Dafny program verifier finished with 47 verified, 0 errors -------------------- SimpleCoinduction.dfy --------------------
-Dafny program verifier finished with 28 verified, 0 errors
+Dafny program verifier finished with 31 verified, 0 errors
-------------------- CalcExample.dfy --------------------
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy index 5a8ab288..cc92a6f1 100644 --- a/Test/dafny3/SimpleCoinduction.dfy +++ b/Test/dafny3/SimpleCoinduction.dfy @@ -64,7 +64,6 @@ copredicate True(s: Stream) comethod AlwaysTrue(s: Stream)
ensures True(s);
{
- AlwaysTrue(s.tail); // WHY does this not happen automatically? (Because 's' is not quantified over)
}
copredicate AlsoTrue(s: Stream)
@@ -75,7 +74,16 @@ copredicate AlsoTrue(s: Stream) comethod AlsoAlwaysTrue(s: Stream)
ensures AlsoTrue(s);
{
- // AlsoAlwaysTrue(s); // here, the recursive call is not needed, because it uses the same 's', so 's' does not need to be quantified over
+}
+
+copredicate TT(y: int)
+{
+ TT(y+1)
+}
+
+comethod AlwaysTT(y: int)
+ ensures TT(y);
+{
}
// -----------------------------------------------------------------------
|