From 72799f600cc520253f0fc26a0327466bbaa28903 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sat, 29 Jun 2013 12:40:57 -0700
Subject: Fixed soundness bug with co-recursive calls:  co-recursive calls may
 now no longer to to functions with ensures clauses

---
 Test/dafny3/Answer      |  2 +-
 Test/dafny3/Streams.dfy | 24 +++++++++++++++++++++---
 2 files changed, 22 insertions(+), 4 deletions(-)

(limited to 'Test/dafny3')

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);
-- 
cgit v1.2.3