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

4 files changed, 82 insertions, 53 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 58dcc262..b410b37d 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -2047,6 +2047,7 @@ namespace Microsoft.Dafny {
   public class LiteralExpr : Expression {

     public readonly object Value;

 

+    [Pure]

     public static bool IsTrue(Expression e) {

       Contract.Requires(e != null);

       if (e is LiteralExpr) {

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index 21bca5d2..d47b1f11 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -120,7 +120,11 @@ namespace Microsoft.Dafny {
     }

 

     IToken Tok(IToken tok) {

-      return new RefinementToken(tok, moduleUnderConstruction);

+      if (moduleUnderConstruction == null) {

+        return tok;

+      } else {

+        return new RefinementToken(tok, moduleUnderConstruction);

+      }

     }

 

     // -------------------------------------------------- Cloning ---------------------------------------------------------------

@@ -164,29 +168,10 @@ namespace Microsoft.Dafny {
         return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);

       } else if (member is Function) {

         var f = (Function)member;

-        return CloneFunction(f, f.IsGhost, null, null);

+        return CloneFunction(f, f.IsGhost, null, null, null);

       } else {

         var m = (Method)member;

-        return CloneMethod(m, CloneBlockStmt(m.Body));

-      }

-    }

-

-    Method CloneMethod(Method m, BlockStmt body) {

-      Contract.Requires(m != null);

-      Contract.Requires(body != null);

-

-      var tps = m.TypeArgs.ConvertAll(CloneTypeParam);

-      var ins = m.Ins.ConvertAll(CloneFormal);

-      var req = m.Req.ConvertAll(CloneMayBeFreeExpr);

-      var mod = CloneSpecFrameExpr(m.Mod);

-      var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);

-      var decreases = CloneSpecExpr(m.Decreases);

-      if (m is Constructor) {

-        return new Constructor(Tok(m.tok), m.Name, tps, ins,

-          req, mod, ens, decreases, body, null);

-      } else {

-        return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, null);

+        return CloneMethod(m, null, null);

       }

     }

 

@@ -517,25 +502,35 @@ namespace Microsoft.Dafny {
       return new GuardedAlternative(Tok(alt.Tok), CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt));

     }

 

-    Function CloneFunction(Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody) {

+    Function CloneFunction(Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody) {

       Contract.Requires(moreBody == null || f is Predicate);

+      Contract.Requires(moreBody == null || replacementBody == null);

 

       var tps = f.TypeArgs.ConvertAll(CloneTypeParam);

       var formals = f.Formals.ConvertAll(CloneFormal);

       var req = f.Req.ConvertAll(CloneExpr);

       var reads = f.Reads.ConvertAll(CloneFrameExpr);

+      var decreases = CloneSpecExpr(f.Decreases);

+

+      var previousModuleUnderConstruction = moduleUnderConstruction;

+      if (moreBody != null || replacementBody != null) { moduleUnderConstruction = null; }

       var ens = f.Ens.ConvertAll(CloneExpr);

+      moduleUnderConstruction = previousModuleUnderConstruction;

       if (moreEnsures != null) {

         ens.AddRange(moreEnsures);

       }

-      var decreases = CloneSpecExpr(f.Decreases);

-      var body = CloneExpr(f.Body);

-      if (moreBody != null) {

-        if (body == null) {

+

+      Expression body;

+      if (replacementBody != null) {

+        body = replacementBody;

+      } else if (moreBody != null) {

+        if (f.Body == null) {

           body = moreBody;

         } else {

-          body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, body, moreBody);

+          body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, CloneExpr(f.Body), moreBody);

         }

+      } else {

+        body = CloneExpr(f.Body);

       }

 

       if (f is Predicate) {

@@ -547,6 +542,33 @@ namespace Microsoft.Dafny {
       }

     }

 

+    Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, BlockStmt replacementBody) {

+      Contract.Requires(m != null);

+

+      var tps = m.TypeArgs.ConvertAll(CloneTypeParam);

+      var ins = m.Ins.ConvertAll(CloneFormal);

+      var req = m.Req.ConvertAll(CloneMayBeFreeExpr);

+      var mod = CloneSpecFrameExpr(m.Mod);

+      var decreases = CloneSpecExpr(m.Decreases);

+

+      var previousModuleUnderConstruction = moduleUnderConstruction;

+      if (replacementBody != null) { moduleUnderConstruction = null; }

+      var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);

+      if (replacementBody != null) { moduleUnderConstruction = previousModuleUnderConstruction; }

+      if (moreEnsures != null) {

+        ens.AddRange(moreEnsures);

+      }

+

+      var body = replacementBody ?? CloneBlockStmt(m.Body);

+      if (m is Constructor) {

+        return new Constructor(Tok(m.tok), m.Name, tps, ins,

+          req, mod, ens, decreases, body, null);

+      } else {

+        return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),

+          req, mod, ens, decreases, body, null);

+      }

+    }

+

     // -------------------------------------------------- Merging ---------------------------------------------------------------

 

     ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {

@@ -603,17 +625,17 @@ namespace Microsoft.Dafny {
               if (!TypesAreEqual(prevFunction.ResultType, f.ResultType)) {

                 reporter.Error(f, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it refines ({2})", f.Name, f.ResultType, prevFunction.ResultType);

               }

-              

-              var newBody = f.Body;

-              if (newBody != null) {

-                if (prevFunction.Body == null || isPredicate) {

-                  // cool

-                } else {

-                  reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");

-                  newBody = null;

-                }

+

+              Expression moreBody = null;

+              Expression replacementBody = null;

+              if (isPredicate) {

+                moreBody = f.Body;

+              } else if (prevFunction.Body == null) {

+                replacementBody = f.Body;

+              } else if (f.Body != null) {

+                reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");

               }

-              nw.Members[index] = CloneFunction(prevFunction, f.IsGhost, f.Ens, newBody);

+              nw.Members[index] = CloneFunction(prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody);

             }

 

           } else {

@@ -644,20 +666,16 @@ namespace Microsoft.Dafny {
               CheckAgreement_Parameters(m.tok, prevMethod.Ins, m.Ins, m.Name, "method", "in-parameter");

               CheckAgreement_Parameters(m.tok, prevMethod.Outs, m.Outs, m.Name, "method", "out-parameter");

 

-              var newBody = m.Body;

-              if (newBody != null) {

+              var replacementBody = m.Body;

+              if (replacementBody != null) {

                 if (prevMethod.Body == null) {

                   // cool

                 } else {

-                  reporter.Error(m, "body of refining method is not yet supported");  // TODO

-                  newBody = null;

+                  reporter.Error(m, "body of refining method is not yet supported");  // TODO (merge the new body into the old)

+                  replacementBody = null;

                 }

               }

-              var clone = CloneMethod(prevMethod, newBody ?? CloneBlockStmt(prevMethod.Body));

-              foreach (var e in m.Ens) {

-                clone.Ens.Add(e);

-              }

-              nw.Members[index] = clone;

+              nw.Members[index] = CloneMethod(prevMethod, m.Ens, replacementBody);

             }

           }

         }

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;
+  }
 }
 
 // ------------------------------------------------