Dafny: added signature checking to refinement

4 files changed, 223 insertions, 42 deletions

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index 6954ee87..21bca5d2 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -164,23 +164,29 @@ 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, null, null);

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

       } else {

         var m = (Method)member;

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

-        var body = CloneBlockStmt(m.Body);

-        if (member 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, 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);

       }

     }

 

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

     }

 

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

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

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

 

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

@@ -533,10 +539,10 @@ namespace Microsoft.Dafny {
       }

 

       if (f is Predicate) {

-        return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.OpenParen, formals,

+        return new Predicate(Tok(f.tok), f.Name, f.IsStatic, isGhost, f.IsUnlimited, tps, f.OpenParen, formals,

           req, reads, ens, decreases, body, moreBody != null, null);

       } else {

-        return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, f.IsUnlimited, tps, f.OpenParen, formals, CloneType(f.ResultType),

+        return new Function(Tok(f.tok), f.Name, f.IsStatic, isGhost, f.IsUnlimited, tps, f.OpenParen, formals, CloneType(f.ResultType),

           req, reads, ens, decreases, body, null);

       }

     }

@@ -570,22 +576,44 @@ namespace Microsoft.Dafny {
             if (!(member is Function) || isPredicate && !(member is Predicate)) {

               reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", s, nwMember.Name);

             } else {

-              if (f.Decreases.Expressions.Count != 0) {

-                reporter.Error(nwMember, "decreases clause on refining {0} not supported", s);

+              var prevFunction = (Function)member;

+              if (f.Req.Count != 0) {

+                reporter.Error(f.Req[0].tok, "a refining {0} is not allowed to add preconditions", s);

               }

               if (f.Reads.Count != 0) {

-                reporter.Error(nwMember, "a refining {0} is not allowed to extend the reads clause", s);

+                reporter.Error(f.Reads[0].E.tok, "a refining {0} is not allowed to extend the reads clause", s);

               }

-              if (f.Req.Count != 0) {

-                reporter.Error(nwMember, "a refining {0} is not allowed to add preconditions", s);

+              if (f.Decreases.Expressions.Count != 0) {

+                reporter.Error(f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", s);

               }

-              // TODO: check agreement for f.TypeArgs, f.ResultType, f.Formals, and flags.  For now, they are ignored and assumed to be the same.

+

+              if (prevFunction.IsStatic != f.IsStatic) {

+                reporter.Error(f, "a function in a refining module cannot be changed from static to non-static or vice versa: {0}", f.Name);

+              }

+              if (prevFunction.IsUnlimited != f.IsUnlimited) {

+                reporter.Error(f, "a function in a refining module cannot be changed from unlimited to limited or vice versa: {0}", f.Name);

+              }

+              if (!prevFunction.IsGhost && f.IsGhost) {

+                reporter.Error(f, "a function method cannot be changed into a (ghost) function in a refining module: {0}", f.Name);

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

+                reporter.Error(f, "a function can be changed into a function method in a refining module only if the function has not yet been given a body: {0}", f.Name);

+              }

+              CheckAgreement_TypeParameters(f.tok, prevFunction.TypeArgs, f.TypeArgs, f.Name, "function");

+              CheckAgreement_Parameters(f.tok, prevFunction.Formals, f.Formals, f.Name, "function", "parameter");

+              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 && !isPredicate) {

-                reporter.Error(nwMember, "a refining function is not allowed to provided a body");

-                newBody = null;

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

+                }

               }

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

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

             }

 

           } else {

@@ -593,23 +621,42 @@ namespace Microsoft.Dafny {
             if (!(member is Method)) {

               reporter.Error(nwMember, "a method declaration ({0}) can only refine a method", nwMember.Name);

             } else {

-              var clone = (Method)CloneMember(member);

-              if (m.Decreases.Expressions.Count != 0) {

-                reporter.Error(nwMember, "decreases clause on refining method not supported");

+              var prevMethod = (Method)member;

+              if (m.Req.Count != 0) {

+                reporter.Error(m.Req[0].E.tok, "a refining method is not allowed to add preconditions");

               }

               if (m.Mod.Expressions.Count != 0) {

-                reporter.Error(nwMember, "a refining method is not allowed to extend the modifies clause");

+                reporter.Error(m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause");

               }

-              if (m.Req.Count != 0) {

-                reporter.Error(nwMember, "a refining method is not allowed to add preconditions");

+              if (m.Decreases.Expressions.Count != 0) {

+                reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported");

               }

-              // TODO: check agreement for m.TypeArgs, m.Ins, m.Outs, and flags.  For now, they are ignored and assumed to be the same.

+

+              if (prevMethod.IsStatic != m.IsStatic) {

+                reporter.Error(m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name);

+              }

+              if (prevMethod.IsGhost && !m.IsGhost) {

+                reporter.Error(m, "a method cannot be changed into a ghost method in a refining module: {0}", m.Name);

+              } else if (!prevMethod.IsGhost && m.IsGhost) {

+                reporter.Error(m, "a ghost method cannot be changed into a non-ghost method in a refining module: {0}", m.Name);

+              }

+              CheckAgreement_TypeParameters(m.tok, prevMethod.TypeArgs, m.TypeArgs, m.Name, "method");

+              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) {

+                if (prevMethod.Body == null) {

+                  // cool

+                } else {

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

+                  newBody = null;

+                }

+              }

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

               foreach (var e in m.Ens) {

                 clone.Ens.Add(e);

               }

-              if (m.Body != null) {

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

-              }

               nw.Members[index] = clone;

             }

           }

@@ -619,6 +666,57 @@ namespace Microsoft.Dafny {
       return nw;

     }

 

+    void CheckAgreement_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing) {

+      Contract.Requires(tok != null);

+      Contract.Requires(old != null);

+      Contract.Requires(nw != null);

+      Contract.Requires(name != null);

+      Contract.Requires(thing != null);

+      if (old.Count != nw.Count) {

+        reporter.Error(tok, "{0} '{1}' is declared with a different number of type parameters ({2} instead of {3}) than the corresponding {0} in the module it refines", thing, name, nw.Count, old.Count);

+      } else {

+        for (int i = 0; i < old.Count; i++) {

+          var o = old[i];

+          var n = nw[i];

+          if (o.Name != n.Name) {

+            reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being refined (expected '{1}', found '{2}')", thing, o.Name, n.Name);

+          }

+        }

+      }

+    }

+

+    void CheckAgreement_Parameters(IToken tok, List<Formal> old, List<Formal> nw, string name, string thing, string parameterKind) {

+      Contract.Requires(tok != null);

+      Contract.Requires(old != null);

+      Contract.Requires(nw != null);

+      Contract.Requires(name != null);

+      Contract.Requires(thing != null);

+      Contract.Requires(parameterKind != null);

+      if (old.Count != nw.Count) {

+        reporter.Error(tok, "{0} '{1}' is declared with a different number of {2} ({3} instead of {4}) than the corresponding {0} in the module it refines", thing, name, parameterKind, nw.Count, old.Count);

+      } else {

+        for (int i = 0; i < old.Count; i++) {

+          var o = old[i];

+          var n = nw[i];

+          if (o.Name != n.Name) {

+            reporter.Error(n.tok, "there is a difference in name of {0} {1} ('{2}' versus '{3}') of {4} {5} compared to corresponding {4} in the module it refines", parameterKind, i, n.Name, o.Name, thing, name);

+          } else if (!o.IsGhost && n.IsGhost) {

+            reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from non-ghost to ghost", parameterKind, n.Name, thing, name);

+          } else if (o.IsGhost && !n.IsGhost) {

+            reporter.Error(n.tok, "{0} '{1}' of {2} {3} cannot be changed, compared to the corresponding {2} in the module it refines, from ghost to non-ghost", parameterKind, n.Name, thing, name);

+          } else if (!TypesAreEqual(o.Type, n.Type)) {

+            reporter.Error(n.tok, "the type of {0} '{1}' is different from the type of the same {0} in the corresponding {2} in the module it refines ('{3}' instead of '{4}')", parameterKind, n.Name, thing, n.Type, o.Type);

+          }

+        }

+      }

+    }

+

+    bool TypesAreEqual(Type t, Type u) {

+      Contract.Requires(t != null);

+      Contract.Requires(u != null);

+      return t.ToString() == u.ToString();

+    }

+

     // ---------------------- additional methods -----------------------------------------------------------------------------

 

     public static bool ContainsChange(Expression expr, ModuleDecl m) {

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

 Execution trace:

     (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 15 verified, 3 errors

+Dafny program verifier finished with 29 verified, 4 errors

 

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

-RefinementErrors.dfy(13,11): Error: a refining method is not allowed to extend the modifies clause

-RefinementErrors.dfy(13,11): Error: a refining method is not allowed to add preconditions

-2 resolution/type errors detected in RefinementErrors.dfy

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

+RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause

+RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate

+RefinementErrors.dfy(32,8): Error: a field declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base

+RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F

+RefinementErrors.dfy(35,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')

+RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')

+RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')

+RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

+RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

+RefinementErrors.dfy(46,11): Error: body of refining method is not yet supported

+RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

+12 resolution/type errors detected in RefinementErrors.dfy

 

 -------------------- ReturnErrors.dfy --------------------

 ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index 2cfbf19a..96fe056f 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -63,6 +63,36 @@ module C_AnonymousClass refines B_AnonymousClass {
 }
 
 // ------------------------------------------------
+
+module BodyFree {
+  function F(x: int): int
+  method TestF() {
+    assert F(6) == F(7);  // error: no information about F so far
+  }
+  method M() returns (a: int, b: int)
+    ensures a == b;
+}
+
+module SomeBody refines BodyFree {
+  function F(x: int): int
+  { if x < 0 then 2 else 3 }
+  method TestFAgain() {
+    assert F(6) == F(7);
+  }
+  method M() returns (a: int, b: int)
+  {
+    a := b;  // good
+  }
+}
+
+module FullBodied refines BodyFree {
+//SOON:  method M() returns (a: int, b: int)
+//  {  // error: does not establish postcondition
+//    a := b + 1;
+//  }
+}
+
+// ------------------------------------------------
 /*  SOON
 module Abstract {
   class MyNumber {
diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
index b10c035e..25ba94ad 100644
--- a/Test/dafny0/RefinementErrors.dfy
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -4,6 +4,19 @@ module A {
     {
       x := 6;
     }
+
+    var abc: bool;
+    var xyz: bool;
+
+    function method F<A,B,C>(x: int, y: A, z: set<C>, b: bool): B
+
+    function G(): int  // uninterpreted for now
+    function H(): int  // uninterpreted for now
+
+    method BodyLess(y: bool, k: seq<set<object>>) returns (x: int)
+    method FullBodied(x: int) returns (y: bool, k: seq<set<object>>)
+    {
+    }
   }
 }
 
@@ -14,5 +27,32 @@ module B refines A {
       requires 0 <= y;  // error: cannot add a precondition
       modifies this;  // error: cannot add a modifies clause
       ensures 0 <= x;  // fine
+
+    predicate abc  // error: cannot replace a field with a predicate
+    var xyz: bool;  // error: ...or even with another field
+
+    function F   // error: cannot replace a "function method" with a "function"
+        <C,A,B>  // error: different list of type parameters
+        (x: int, y: A, z: seq<C>,  // error: different type of parameter z
+         k: bool)  // error: different parameter name
+        : B
+
+    function G(): int
+    { 12 }  // allowed to add a body
+
+    method BodyLess(y: bool, k: seq<set<object>>) returns (x: int)
+    {  // yes, can give it a body
+    }
+    method FullBodied(x: int) returns (y: bool, k: seq<set<object>>)
+    {  // error: not allowed to change body (not yet implemented)
+    }
+  }
+}
+
+module BB refines B {
+  class C {
+    function method G(): int  // error: allowed to make a function into a function method
+    function method H(): int  // ...unless this is where the function body is given
+    { 10 }
   }
 }