Fixed unsoundness (and also allowed other, sound cases) in the admissability checks for co-recursive calls

2 files changed, 37 insertions, 11 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 97097cfd..36a6eda9 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1151,8 +1151,11 @@ Execution trace:
 Corecursion.dfy(50,5): Error: cannot prove termination; try supplying a decreases clause

 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)

+Execution trace:

+    (0,0): anon5_Else

 

-Dafny program verifier finished with 5 verified, 2 errors

+Dafny program verifier finished with 7 verified, 3 errors

 

 -------------------- CoResolution.dfy --------------------

 CoResolution.dfy(14,9): Error: member Undeclared# does not exist in class _default

@@ -1696,36 +1699,36 @@ Execution trace:
 Dafny program verifier finished with 1 verified, 4 errors

 

 -------------------- Superposition.dfy --------------------

-
+

 Verifying CheckWellformed$$_0_M0.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_0_M0.C.M ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.P ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.Q ...

   [3 proof obligations]  error

 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_0_M0.C.R ...

   [3 proof obligations]  error

 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_1_M1.C.M ...

   [1 proof obligation]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.P ...

   [1 proof obligation]  error

 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.

@@ -1734,10 +1737,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon9_Then

     (0,0): anon6

-
+

 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.R ...

   [0 proof obligations]  verified

 

diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index 0918d6f5..6d3a0e13 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -50,3 +50,26 @@ module CoRecursionNotUsed {
     Diverge(n)  // error: cannot prove termination

   }

 }

+

+// --------------------------------------------------

+

+module EqualityIsSuperDestructive {

+  codatatype Stream<T> = Cons(head: T, tail: Stream)

+

+  function F(s: Stream<int>): Stream<int>

+  {

+    // Co-recursive calls are not allowed in arguments of equality, so the following call to

+    // F(s) is a recursive call.

+    if Cons(1, F(s)) == Cons(1, Cons(1, s))  // error: cannot prove termination

+    then Cons(2, s) else Cons(1, s)

+  }

+

+  ghost method lemma(s: Stream<int>)

+  {

+    // The following three assertions follow from the definition of F, so F had better

+    // generate some error (which it does -- the recursive call to F in F does not terminate).

+    assert F(s) == Cons(1, s);

+    assert F(s) == Cons(2, s);

+    assert false;

+  }

+}