Fixed soundness bug with co-recursive calls: co-recursive calls may now no longer to to functions with ensures clauses

4 files changed, 35 insertions, 8 deletions

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);