Dafny: allow a refinement to provide a function/method body if the function/method being refined didn't have one

2 files changed, 16 insertions, 6 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 71089e91..57d44098 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1338,11 +1338,18 @@ Execution trace:
 Refinement.dfy(61,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Refinement.dfy(70,17): Error: assertion violation

+Refinement.dfy(71,17): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Refinement.dfy(69,15): Error: possible violation of function postcondition

+Execution trace:

+    (0,0): anon3_Else

+Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this return path.

+Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 29 verified, 4 errors

+Dafny program verifier finished with 28 verified, 6 errors

 

 -------------------- RefinementErrors.dfy --------------------

 RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index 96fe056f..d99ffdc9 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -66,6 +66,7 @@ module C_AnonymousClass refines B_AnonymousClass {
 
 module BodyFree {
   function F(x: int): int
+    ensures 0 <= F(x);
   method TestF() {
     assert F(6) == F(7);  // error: no information about F so far
   }
@@ -86,10 +87,12 @@ module SomeBody refines BodyFree {
 }
 
 module FullBodied refines BodyFree {
-//SOON:  method M() returns (a: int, b: int)
-//  {  // error: does not establish postcondition
-//    a := b + 1;
-//  }
+  function F(x: int): int
+  { x } // error: does not meet the inherited postcondition (note, confusing error-message location)
+  method M() returns (a: int, b: int)
+  {  // error: does not establish postcondition
+    a := b + 1;
+  }
 }
 
 // ------------------------------------------------