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/dafny3 | |
| 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/dafny3')
| -rw-r--r-- | Test/dafny3/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny3/Streams.dfy | 24 |
2 files changed, 22 insertions, 4 deletions
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);
|