diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 9 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 12 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 5 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 11 | ||||
| -rw-r--r-- | Test/dafny0/Corecursion.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny3/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny3/Streams.dfy | 24 |
7 files changed, 59 insertions, 10 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 61ed3419..f5010443 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3921,7 +3921,14 @@ namespace Microsoft.Dafny { public readonly IToken OpenParen; // can be null if Args.Count == 0
public readonly List<Expression/*!*/>/*!*/ Args;
public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // created, initialized, and used by resolution (and also used by translation)
- public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }
+ public enum CoCallResolution {
+ No,
+ Yes,
+ NoBecauseFunctionHasSideEffects,
+ NoBecauseFunctionHasPostcondition,
+ NoBecauseRecursiveCallsAreNotAllowedInThisContext,
+ NoBecauseIsNotGuarded
+ }
public CoCallResolution CoCall = CoCallResolution.No; // indicates whether or not the call is a co-recursive call; filled in by resolution
[ContractInvariantMethod]
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 762bcc7e..dd59bf57 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -7425,6 +7425,18 @@ namespace Microsoft.Dafny } else {
e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
}
+ } else if (e.Function.Ens.Count != 0) {
+ // this call is disqualified from being a co-call, because it has a postcondition
+ // (a postcondition could be allowed, as long as it does not get to be used with
+ // co-recursive calls, because that could be unsound; for example, consider
+ // "ensures false;")
+ if (!dealsWithCodatatypes) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.No;
+ } else if (coContext != null) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition;
+ } else {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
+ }
} else if (!allowCallsWithinRecursiveCluster) {
if (!dealsWithCodatatypes) {
e.CoCall = FunctionCallExpr.CoCallResolution.No;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index ba993caf..49173230 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3303,7 +3303,10 @@ namespace Microsoft.Dafny { string hint;
switch (e.CoCall) {
case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects:
- hint = "note that only functions without side effects can called co-recursively";
+ hint = "note that only functions without side effects can be called co-recursively";
+ break;
+ case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition:
+ hint = "note that only functions without any ensures clause can be called co-recursively";
break;
case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded:
hint = "note that the call is not sufficiently guarded to be used co-recursively";
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 36a6eda9..e20227e7 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1145,17 +1145,20 @@ Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in 8 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 called co-recursively)
+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)
Execution trace:
(0,0): anon3_Else
-Corecursion.dfy(50,5): Error: cannot prove termination; try supplying a decreases clause
+Corecursion.dfy(21,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively)
Execution trace:
(0,0): anon3_Else
-Corecursion.dfy(63,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
+Corecursion.dfy(56,5): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon3_Else
+Corecursion.dfy(69,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context)
Execution trace:
(0,0): anon5_Else
-Dafny program verifier finished with 7 verified, 3 errors
+Dafny program verifier finished with 7 verified, 4 errors
-------------------- CoResolution.dfy --------------------
CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy index 6d3a0e13..5025dae9 100644 --- a/Test/dafny0/Corecursion.dfy +++ b/Test/dafny0/Corecursion.dfy @@ -15,6 +15,12 @@ module CoRecursion { More(n, AscendingChainAndRead(n+1)) // error: cannot prove termination
}
+ function AscendingChainAndPostcondition(n: nat): Stream<int>
+ ensures false; // with an ensures clause, this function is not a co-recusvie function
+ {
+ More(n, AscendingChainAndPostcondition(n+1)) // error: cannot prove termination
+ }
+
datatype List<T> = Nil | Cons(T, List);
function Prefix(n: nat, s: Stream): List
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index 9c6a2598..6ca8aafa 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -5,7 +5,7 @@ Dafny program verifier finished with 15 verified, 0 errors -------------------- Streams.dfy --------------------
-Dafny program verifier finished with 50 verified, 0 errors
+Dafny program verifier finished with 52 verified, 0 errors
-------------------- Dijkstra.dfy --------------------
diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy index 1198c7e0..f13c5c0a 100644 --- a/Test/dafny3/Streams.dfy +++ b/Test/dafny3/Streams.dfy @@ -235,22 +235,40 @@ function PrependThenFlattenNonEmpties(prefix: Stream, M: Stream<Stream>): Stream // of a given stream of streams.
function Prepend<T>(x: T, M: Stream<Stream>): Stream<Stream>
- ensures StreamOfNonEmpties(Prepend(x, M));
{
match M
case Nil => Nil
case Cons(s, N) => Cons(Cons(x, s), Prepend(x, N))
}
+comethod Prepend_Lemma<T>(x: T, M: Stream<Stream>)
+ ensures StreamOfNonEmpties(Prepend(x, M));
+{
+ match M {
+ case Nil =>
+ case Cons(s, N) => Prepend_Lemma(x, N);
+ }
+}
+
ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)
- ensures FlattenStartMarker(M, startMarker) == FlattenNonEmpties(Prepend(startMarker, M));
+ ensures
+ StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;
+ // but until (co-)method can be called from functions,
+ // this condition is used as an antecedent here
+ FlattenStartMarker(M, startMarker) == FlattenNonEmpties(Prepend(startMarker, M));
{
+ Prepend_Lemma(startMarker, M);
Lemma_Flatten(Nil, M, startMarker);
}
comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)
- ensures PrependThenFlattenStartMarker(prefix, M, startMarker) == PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
+ ensures
+ StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;
+ // but until (co-)method can be called from functions,
+ // this condition is used as an antecedent here
+ PrependThenFlattenStartMarker(prefix, M, startMarker) == PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));
{
+ Prepend_Lemma(startMarker, M);
match (prefix) {
case Cons(hd, tl) =>
Lemma_Flatten(tl, M, startMarker);
|