diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-06-29 12:40:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-06-29 12:40:57 -0700 |
| commit | 72799f600cc520253f0fc26a0327466bbaa28903 (patch) | |
| tree | 5580bddeaeb4ffeb1b049b32ad436e03ba454ac1 /Test/dafny0/Corecursion.dfy | |
| parent | 141863d4677fc7bd7b2c6891d6f354b7d9237036 (diff) | |
Fixed soundness bug with co-recursive calls: co-recursive calls may now no longer to to functions with ensures clauses
Diffstat (limited to 'Test/dafny0/Corecursion.dfy')
| -rw-r--r-- | Test/dafny0/Corecursion.dfy | 6 |
1 files changed, 6 insertions, 0 deletions
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
|