Revised look-up and compilation of inherited trait members (static functions/methods don't work yet)

10 files changed, 306 insertions, 226 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 3c266a28..6317e462 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -145,19 +145,13 @@ namespace Microsoft.Dafny
       if (member is Field) {

         Contract.Assert(!(member is SpecialField));  // we don't expect a SpecialField to be cloned (or do we?)

         var f = (Field)member;

-        Field field = new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));

-        field.Inherited = member.Inherited;

-        return field;

+        return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes));

       } else if (member is Function) {

         var f = (Function)member;

-        Function func = CloneFunction(f);

-        func.Inherited = member.Inherited;

-        return func;

+        return CloneFunction(f);

       } else {

         var m = (Method)member;

-        Method method = CloneMethod(m);

-        method.Inherited = member.Inherited;

-        return method;

+        return CloneMethod(m);

       }

     }

 

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index d43c57c6..f2a1bdcd 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -760,6 +760,34 @@ namespace Microsoft.Dafny {
       Contract.Requires(c != null);

       Contract.Requires(!forCompanionClass || c is TraitDecl);

       Contract.Requires(0 <= indent);

+      foreach (var member in c.InheritedMembers) {

+        Contract.Assert(!member.IsGhost && !member.IsStatic);  // only non-ghost instance members should ever be added to .InheritedMembers

+        if (member is Field) {

+          var f = (Field)member;

+          // every field is inherited

+          Indent(indent);

+          wr.WriteLine("public {0} @_{1};", TypeName(f.Type), f.CompileName);

+          wr.Write("public {0} @{1}", TypeName(f.Type), f.CompileName);

+          wr.WriteLine(" {");

+          wr.WriteLine(" get { ");

+          wr.Write("return this.@_{0};", f.CompileName);

+          wr.WriteLine("}");

+          wr.WriteLine(" set { ");

+          wr.WriteLine("this.@_{0} = value;", f.CompileName);

+          wr.WriteLine("}");

+          wr.WriteLine("}");

+        } else if (member is Function) {

+          var f = (Function)member;

+          Contract.Assert(f.Body != null);

+          CompileFunction(indent, f);

+        } else if (member is Method) {

+          var method = (Method)member;

+          Contract.Assert(method.Body != null);

+          CompileMethod(c, indent, method);

+        } else {

+          Contract.Assert(false);  // unexpected member

+        }

+      }

       foreach (MemberDecl member in c.Members) {

         if (member is Field) {

           var f = (Field)member;

@@ -769,18 +797,6 @@ namespace Microsoft.Dafny {
             Indent(indent);

             wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);

             wr.WriteLine(" { get; set; }");

-          } else if (f.Inherited) {

-            Indent(indent);

-            wr.WriteLine("public {0} @_{1};", TypeName(f.Type), f.CompileName);

-            wr.Write("public {0} @{1}", TypeName(f.Type), f.CompileName);

-            wr.WriteLine(" {");

-            wr.WriteLine(" get { ");

-            wr.Write("return this.@_{0};", f.CompileName);

-            wr.WriteLine("}");

-            wr.WriteLine(" set { ");

-            wr.WriteLine("this.@_{0} = value;", f.CompileName);

-            wr.WriteLine("}");

-            wr.WriteLine("}");

           } else {

             Indent(indent);

             wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));

@@ -814,16 +830,7 @@ namespace Microsoft.Dafny {
           } else if (forCompanionClass && !f.IsStatic) {

             // companion classes only has static members

           } else {

-            Indent(indent);

-            wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);

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

-              wr.Write("<{0}>", TypeParameters(f.TypeArgs));

-            }

-            wr.Write("(");

-            WriteFormals("", f.Formals);

-            wr.WriteLine(") {");

-            CompileReturnBody(f.Body, indent + IndentAmount);

-            Indent(indent); wr.WriteLine("}");

+            CompileFunction(indent, f);

           }

         } else if (member is Method) {

           var m = (Method)member;

@@ -855,60 +862,7 @@ namespace Microsoft.Dafny {
           } else if (forCompanionClass && !m.IsStatic) {

             // companion classes only has static members

           } else {

-            Indent(indent);

-            wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);

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

-              wr.Write("<{0}>", TypeParameters(m.TypeArgs));

-            }

-            wr.Write("(");

-            int nIns = WriteFormals("", m.Ins);

-            WriteFormals(nIns == 0 ? "" : ", ", m.Outs);

-            wr.WriteLine(")");

-            Indent(indent); wr.WriteLine("{");

-            foreach (Formal p in m.Outs) {

-              if (!p.IsGhost) {

-                Indent(indent + IndentAmount);

-                wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));

-              }

-            }

-            if (m.Body == null) {

-              Error("Method {0} has no body", m.FullName);

-            } else {

-              if (m.IsTailRecursive) {

-                Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");

-                if (!m.IsStatic) {

-                  Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");

-                }

-              }

-              Contract.Assert(enclosingMethod == null);

-              enclosingMethod = m;

-              TrStmtList(m.Body.Body, indent);

-              Contract.Assert(enclosingMethod == m);

-              enclosingMethod = null;

-            }

-            Indent(indent); wr.WriteLine("}");

-

-            // allow the Main method to be an instance method

-            if (!m.IsStatic && IsMain(m)) {

-              Indent(indent);

-              wr.WriteLine("public static void Main(string[] args) {");

-              Contract.Assert(m.EnclosingClass == c);

-              Indent(indent + IndentAmount);

-              wr.Write("@{0} b = new @{0}", c.CompileName);

-              if (c.TypeArgs.Count != 0) {

-                // instantiate every parameter, it doesn't particularly matter how

-                wr.Write("<");

-                string sep = "";

-                for (int i = 0; i < c.TypeArgs.Count; i++) {

-                  wr.Write("{0}int", sep);

-                  sep = ", ";

-                }

-                wr.Write(">");

-              }

-              wr.WriteLine("();");

-              Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");

-              Indent(indent); wr.WriteLine("}");

-            }

+            CompileMethod(c, indent, m);

           }

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member

@@ -916,6 +870,76 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private void CompileFunction(int indent, Function f) {

+      Indent(indent);

+      wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);

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

+        wr.Write("<{0}>", TypeParameters(f.TypeArgs));

+      }

+      wr.Write("(");

+      WriteFormals("", f.Formals);

+      wr.WriteLine(") {");

+      CompileReturnBody(f.Body, indent + IndentAmount);

+      Indent(indent); wr.WriteLine("}");

+    }

+

+    private void CompileMethod(ClassDecl c, int indent, Method m) {

+      Indent(indent);

+      wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);

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

+        wr.Write("<{0}>", TypeParameters(m.TypeArgs));

+      }

+      wr.Write("(");

+      int nIns = WriteFormals("", m.Ins);

+      WriteFormals(nIns == 0 ? "" : ", ", m.Outs);

+      wr.WriteLine(")");

+      Indent(indent); wr.WriteLine("{");

+      foreach (Formal p in m.Outs) {

+        if (!p.IsGhost) {

+          Indent(indent + IndentAmount);

+          wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));

+        }

+      }

+      if (m.Body == null) {

+        Error("Method {0} has no body", m.FullName);

+      } else {

+        if (m.IsTailRecursive) {

+          Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");

+          if (!m.IsStatic) {

+            Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");

+          }

+        }

+        Contract.Assert(enclosingMethod == null);

+        enclosingMethod = m;

+        TrStmtList(m.Body.Body, indent);

+        Contract.Assert(enclosingMethod == m);

+        enclosingMethod = null;

+      }

+      Indent(indent); wr.WriteLine("}");

+

+      // allow the Main method to be an instance method

+      if (!m.IsStatic && IsMain(m)) {

+        Indent(indent);

+        wr.WriteLine("public static void Main(string[] args) {");

+        Contract.Assert(m.EnclosingClass == c);

+        Indent(indent + IndentAmount);

+        wr.Write("@{0} b = new @{0}", c.CompileName);

+        if (c.TypeArgs.Count != 0) {

+          // instantiate every parameter, it doesn't particularly matter how

+          wr.Write("<");

+          string sep = "";

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

+            wr.Write("{0}int", sep);

+            sep = ", ";

+          }

+          wr.Write(">");

+        }

+        wr.WriteLine("();");

+        Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");

+        Indent(indent); wr.WriteLine("}");

+      }

+    }

+

     void CompileReturnBody(Expression body, int indent) {

       Contract.Requires(0 <= indent);

       body = body.Resolved;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 02d729b4..dadfeb15 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1872,6 +1872,7 @@ namespace Microsoft.Dafny {
   public class ClassDecl : TopLevelDecl {

     public override string WhatKind { get { return "class"; } }

     public readonly List<MemberDecl> Members;

+    public readonly List<MemberDecl> InheritedMembers = new List<MemberDecl>();  // these are non-ghost instance fields and instance members defined with bodies in traits (this list is used by the compiler)

     public readonly List<Type> TraitsTyp;  // these are the types that are parsed after the keyword 'extends'

     public readonly List<TraitDecl> TraitsObj = new List<TraitDecl>();  // populated during resolution

     public bool HasConstructor;  // filled in (early) during resolution; true iff there exists a member that is a Constructor

@@ -2288,7 +2289,6 @@ namespace Microsoft.Dafny {
     public readonly bool IsGhost;

     public TopLevelDecl EnclosingClass;  // filled in during resolution

     public MemberDecl RefinementBase;  // filled in during the pre-resolution refinement transformation; null if the member is new here

-    public bool Inherited;

     public MemberDecl(IToken tok, string name, bool hasStaticKeyword, bool isGhost, Attributes attributes)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0e8e0ec3..5a5bfb26 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -209,7 +209,6 @@ namespace Microsoft.Dafny
     readonly Graph<ModuleDecl> dependencies = new Graph<ModuleDecl>();

     private ModuleSignature systemNameInfo = null;

     private bool useCompileSignatures = false;

-    private RefinementTransformer refinementTransformer = null;

 

     public Resolver(Program prog) {

       Contract.Requires(prog != null);

@@ -1006,11 +1005,16 @@ namespace Microsoft.Dafny
           var members = new Dictionary<string, MemberDecl>();

           classMembers.Add(cl, members);

 

-          bool hasConstructor = false;

           foreach (MemberDecl m in cl.Members) {

             if (!members.ContainsKey(m.Name)) {

               members.Add(m.Name, m);

-              if (m is CoPredicate || m is CoLemma) {

+              if (m is Constructor) {

+                if (cl is TraitDecl) {

+                  Error(m.tok, "a trait is not allowed to declare a constructor");

+                } else {

+                  cl.HasConstructor = true;

+                }

+              } else if (m is CoPredicate || m is CoLemma) {

                 var extraName = m.Name + "#";

                 MemberDecl extraMember;

                 var cloner = new Cloner();

@@ -1063,14 +1067,6 @@ namespace Microsoft.Dafny
             } else {

               Error(m, "Duplicate member name: {0}", m.Name);

             }

-            if (m is Constructor) {

-              hasConstructor = true;

-            }

-          }

-          cl.HasConstructor = hasConstructor;

-          if (cl is TraitDecl && cl.HasConstructor)

-          {

-              Error(cl, "a trait is not allowed to declare a constructor");

           }

           if (cl.IsDefaultClass) {

             foreach (MemberDecl m in cl.Members) {

@@ -1191,6 +1187,14 @@ namespace Microsoft.Dafny
       Contract.Requires(datatypeDependencies != null);

       Contract.Requires(codatatypeDependencies != null);

 

+      // resolve the trait names that a class extends and register the trait members in the classes that inherit them

+      foreach (TopLevelDecl d in declarations) {

+        var cl = d as ClassDecl;

+        if (cl != null) {

+          RegisterInheritedMembers(cl);

+        }

+      }

+

       var typeRedirectionDependencies = new Graph<RedirectingTypeDecl>();

       foreach (TopLevelDecl d in declarations) {

         Contract.Assert(d != null);

@@ -2825,17 +2829,21 @@ namespace Microsoft.Dafny
     List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)

     readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"

 

-

     /// <summary>

-    /// Assumes type parameters have already been pushed

+    /// This method resolves the types that have been given after the 'extends' keyword.  Then, it populates

+    /// the string->MemberDecl table for "cl" to make sure that all inherited names are accounted for.  Further

+    /// checks are done later, elsewhere.

     /// </summary>

-    void ResolveClassMemberTypes(ClassDecl cl) {

+    void RegisterInheritedMembers(ClassDecl cl) {

       Contract.Requires(cl != null);

       Contract.Requires(currentClass == null);

       Contract.Ensures(currentClass == null);

-

       currentClass = cl;

 

+      if (cl.TraitsTyp.Count > 0 && cl.TypeArgs.Count > 0) {

+        Error(cl.tok, "sorry, traits are currently supported only for classes that take no type arguments");  // TODO: do the work to remove this limitation

+      }

+

       // Resolve names of traits extended

       foreach (var tt in cl.TraitsTyp) {

         var prevErrorCount = ErrorCount;

@@ -2857,6 +2865,34 @@ namespace Microsoft.Dafny
         }

       }

 

+      // Inherit members from traits.  What we do here is simply to register names, and in particular to register

+      // names that are no already in the class.

+      var members = classMembers[cl];

+      foreach (var trait in cl.TraitsObj) {

+        foreach (var traitMember in trait.Members) {

+          MemberDecl classMember;

+          if (members.TryGetValue(traitMember.Name, out classMember)) {

+            // the class already declares or inherits a member with this name, so we take no further action at this time

+          } else {

+            // register the trait member in the class

+            members.Add(traitMember.Name, traitMember);

+          }

+        }

+      }

+

+      currentClass = null;

+    }

+

+    /// <summary>

+    /// Assumes type parameters have already been pushed

+    /// </summary>

+    void ResolveClassMemberTypes(ClassDecl cl) {

+      Contract.Requires(cl != null);

+      Contract.Requires(currentClass == null);

+      Contract.Ensures(currentClass == null);

+

+      currentClass = cl;

+

       foreach (MemberDecl member in cl.Members) {

         member.EnclosingClass = cl;

         if (member is Field) {

@@ -2910,112 +2946,91 @@ namespace Microsoft.Dafny
     void InheritTraitMembers(ClassDecl cl) {

       Contract.Requires(cl != null);

 

-      RefinementCloner cloner = new RefinementCloner(cl.Module);

+      var refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);

       //merging class members with parent members if any

-      if (cl.TraitsObj != null) {

-        var clMembers = classMembers[cl];

-        foreach (TraitDecl traitObj in cl.TraitsObj)

-        {

-            var traitMembers = classMembers[traitObj];

-            //merging current class members with the inheriting trait

-            foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers)

-            {

-                MemberDecl clMember;

-                if (clMembers.TryGetValue(traitMem.Key, out clMember))

-                {

-                    //check if the signature of the members are equal and the member is body-less

-                    if (traitMem.Value is Method)

-                    {

-                        Method traitMethod = (Method)traitMem.Value;

-                        // TODO: should check that the class member is also a method, and the same kind of method

-                        Method classMethod = (Method)clMember;

-                        //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod);

-                        if (traitMethod.Body != null && !clMembers[classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent

-                            Error(classMethod, "a class cannot override implemented methods");

-                        else

-                        {

-                            classMethod.OverriddenMethod = traitMethod;

-                            //adding a call graph edge from the trait method to that of class

-                            cl.Module.CallGraph.AddEdge(traitMethod, classMethod);

-                        }

-                    }

-                    else if (traitMem.Value is Function)

-                    {

-                        Function traitFunction = (Function)traitMem.Value;

-                        Function classFunction = (Function)clMember;

-                        //refinementTransformer.CheckFunctionsAreRefinements(classFunction, traitFunction);

-                        if (traitFunction.Body != null && !classMembers[cl][classFunction.CompileName].Inherited)

-                            Error(classFunction, "a class cannot override implemented functions");

-                        else

-                        {

-                            classFunction.OverriddenFunction = traitFunction;

-                            //adding a call graph edge from the trait function to that of class

-                            cl.Module.CallGraph.AddEdge(traitFunction, classFunction);

-                        }

-                    }

-                    else if (traitMem.Value is Field)

-                    {

-                        Field traitField = (Field)traitMem.Value;

-                        Field classField = (Field)clMember;

-                        if (!clMembers[classField.CompileName].Inherited)

-                            Error(classField, "member in the class has been already inherited from its parent trait");

-                    }

-                }

-                else

-                {

-                    //the member is not already in the class

-                    // enter the trait member in the symbol table for the class

-                    MemberDecl classNewMember = cloner.CloneMember(traitMem.Value);

-                    classNewMember.EnclosingClass = cl;

-                    classNewMember.Inherited = true;

-                    classMembers[cl].Add(traitMem.Key, classNewMember);

-                    cl.Members.Add(classNewMember);

-                }

-            }//foreach

-        }

-        //checking to make sure all body-less methods/functions have been implemented in the child class

-        if (refinementTransformer == null)

-          refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);

-        foreach (TraitDecl traitObj in cl.TraitsObj)

-        {

-            foreach (MemberDecl traitMember in traitObj.Members.Where(mem => mem is Function || mem is Method))

-            {

-                if (traitMember is Function)

-                {

-                    Function traitFunc = (Function)traitMember;

-                    if (traitFunc.Body == null) //we do this check only if trait function body is null

-                    {

-                        var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName);

-                        if (classMem != null)

-                        {

-                            Function classFunc = (Function)classMem;

-                            refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc);

-                        }

-                        else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null)

-                            Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName);

-                    }

-                }

-                if (traitMember is Method)

-                {

-                    Method traitMethod = (Method)traitMember;

-                    if (traitMethod.Body == null) //we do this check only if trait method body is null

-                    {

-                        var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName);

-                        if (classMem != null)

-                        {

-                            Method classMethod = (Method)classMem;

-                            refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);

-                            var traitMethodAllowsNonTermination = Contract.Exists(traitMethod.Decreases.Expressions, e => e is WildcardExpr);

-                            var classMethodAllowsNonTermination = Contract.Exists(classMethod.Decreases.Expressions, e => e is WildcardExpr);

-                            if (classMethodAllowsNonTermination && !traitMethodAllowsNonTermination) {

-                              Error(classMethod.tok, "not allowed to override a terminating method with a possibly non-terminating method ('{0}')", classMethod.Name);

-                            }

-                        }

-                        if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null)

-                            Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName);

-                    }

-                }

+      var clMembers = classMembers[cl];

+      foreach (TraitDecl trait in cl.TraitsObj) {

+        //merging current class members with the inheriting trait

+        foreach (var traitMember in trait.Members) {

+          var clMember = clMembers[traitMember.Name];

+          if (clMember == traitMember) {

+            // The member is the one inherited from the trait (and the class does not itself define a member with this name).  This

+            // is fine for fields and for functions and methods with bodies.  However, for a body-less function or method, the class

+            // is required to at least redeclare the member with its signature.  (It should also provide a stronger specification,

+            // but that will be checked by the verifier.  And it should also have a body, but that will be checked by the compiler.)

+            if (traitMember is Field) {

+              var field = (Field)traitMember;

+              if (!field.IsGhost) {

+                cl.InheritedMembers.Add(field);

+              }

+            } else if (traitMember is Function) {

+              var func = (Function)traitMember;

+              if (func.Body == null) {

+                Error(cl.tok, "class '{0}' does not implement trait function '{1}.{2}'", cl.Name, trait.Name, traitMember.Name);

+              } else if (!func.IsGhost && !func.IsStatic) {

+                cl.InheritedMembers.Add(func);

+              }

+            } else if (traitMember is Method) {

+              var method = (Method)traitMember;

+              if (method.Body == null) {

+                Error(cl.tok, "class '{0}' does not implement trait method '{1}.{2}'", cl.Name, trait.Name, traitMember.Name);

+              } else if (!method.IsGhost && !method.IsStatic) {

+                cl.InheritedMembers.Add(method);

+              }

+            }

+          } else if (clMember.EnclosingClass != cl) {

+            // The class inherits the member from two places

+            Error(clMember.tok, "member name '{0}' in class '{1}' inherited from both traits '{2}' and '{3}'", traitMember.Name, cl.Name, clMember.EnclosingClass.Name, trait.Name);

+

+          } else if (traitMember is Field) {

+            // The class is not allowed to do anything with the field other than silently inherit it.

+            if (clMember is Field) {

+              Error(clMember.tok, "field '{0}' is inherited from trait '{1}' and is not allowed to be re-declared", traitMember.Name, trait.Name);

+            } else {

+              Error(clMember.tok, "member name '{0}' in class '{1}' clashes with inherited field from trait '{2}'", traitMember.Name, cl.Name, trait.Name);

+            }

+

+          } else if (traitMember is Method) {

+            var traitMethod = (Method)traitMember;

+            if (traitMethod.Body != null) {

+              // The method was defined in the trait, so the class is not allowed to do anything with the method other than silently inherit it.

+              Error(clMember.tok, "member '{0}' in class '{1}' overrides fully defined method inherited from trait '{2}'", clMember.Name, cl.Name, trait.Name);

+            } else if (!(clMember is Method)) {

+              Error(clMember.tok, "non-method member '{0}' overrides method '{1}' inherited from trait '{2}'", clMember.Name, traitMethod.Name, trait.Name);

+            } else {

+              var classMethod = (Method)clMember;

+              classMethod.OverriddenMethod = traitMethod;

+              //adding a call graph edge from the trait method to that of class

+              cl.Module.CallGraph.AddEdge(traitMethod, classMethod);

+

+              refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod);

+

+              var traitMethodAllowsNonTermination = Contract.Exists(traitMethod.Decreases.Expressions, e => e is WildcardExpr);

+              var classMethodAllowsNonTermination = Contract.Exists(classMethod.Decreases.Expressions, e => e is WildcardExpr);

+              if (classMethodAllowsNonTermination && !traitMethodAllowsNonTermination) {

+                Error(classMethod.tok, "not allowed to override a terminating method with a possibly non-terminating method ('{0}')", classMethod.Name);

+              }

             }

+

+          } else if (traitMember is Function) {

+            var traitFunction = (Function)traitMember;

+            if (traitFunction.Body != null) {

+              // The function was defined in the trait, so the class is not allowed to do anything with the function other than silently inherit it.

+              Error(clMember.tok, "member '{0}' in class '{1}' overrides fully defined function inherited from trait '{2}'", clMember.Name, cl.Name, trait.Name);

+            } else if (!(clMember is Function)) {

+              Error(clMember.tok, "non-function member '{0}' overrides function '{1}' inherited from trait '{2}'", clMember.Name, traitFunction.Name, trait.Name);

+            } else {

+              var classFunction = (Function)clMember;

+              classFunction.OverriddenFunction = traitFunction;

+              //adding a call graph edge from the trait method to that of class

+              cl.Module.CallGraph.AddEdge(traitFunction, classFunction);

+

+              refinementTransformer.CheckOverride_FunctionParameters(classFunction, traitFunction);

+            }

+

+          } else {

+            Contract.Assert(false);  // unexpected member

+          }

         }

       }

     }

@@ -8082,7 +8097,7 @@ namespace Microsoft.Dafny
               }

             }

             if (errorCount != ErrorCount) {

-              // no nothing else; error has been reported

+              // do nothing else; error has been reported

             } else if (callee != null) {

               // produce a FunctionCallExpr instead of an ApplyExpr(MemberSelectExpr)

               var rr = new FunctionCallExpr(e.Lhs.tok, callee.Name, mse.Obj, e.tok, e.Args);

diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect
index 84465fea..69af0dc5 100644
--- a/Test/dafny0/Trait/TraitBasix.dfy.expect
+++ b/Test/dafny0/Trait/TraitBasix.dfy.expect
@@ -1,7 +1,7 @@
 TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name?)

-TraitBasix.dfy(77,8): Error: member in the class has been already inherited from its parent trait

-TraitBasix.dfy(70,8): Error: class: I0Child does not implement trait member: Customizable

-TraitBasix.dfy(80,8): Error: class: I0Child2 does not implement trait member: F

-TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor

+TraitBasix.dfy(77,8): Error: field 'x' is inherited from trait 'I2' and is not allowed to be re-declared

+TraitBasix.dfy(70,8): Error: class 'I0Child' does not implement trait method 'I2.Customizable'

+TraitBasix.dfy(80,8): Error: class 'I0Child2' does not implement trait function 'I2.F'

+TraitBasix.dfy(101,15): Error: a trait is not allowed to declare a constructor

 TraitBasix.dfy(117,9): Error: new cannot be applied to a trait

 6 resolution/type errors detected in TraitBasix.dfy

diff --git a/Test/dafny0/Trait/TraitCompile.dfy b/Test/dafny0/Trait/TraitCompile.dfy
index cc667a9a..3d559de1 100644
--- a/Test/dafny0/Trait/TraitCompile.dfy
+++ b/Test/dafny0/Trait/TraitCompile.dfy
@@ -58,14 +58,61 @@ method Main()
   Client(c);

   var z := TT.StaticMinus(50, 20);

   print "z=", z, "\n";

-  var z' := CC.StaticMinus(50, 20);

-  print "z'=", z', "\n";

-  var w := c.StaticMinus(50, 20);

-  print "w=", w, "\n";

+//  var z' := CC.StaticMinus(50, 20);

+//  print "z'=", z', "\n";

+//  var w := c.StaticMinus(50, 20);

+//  print "w=", w, "\n";

 

   c.Double(500);

   c.AddFive(502);

-  c.StaticTriple(504);

+//  c.StaticTriple(504);

   TT.StaticTriple(504);

-  CC.StaticTriple(505);

+//  CC.StaticTriple(505);

+

+  var seven := OtherModule.Y.F(15);

+  assert seven == 7;

+  var b := OtherModule.Y.P(real(seven));

+  print "From OtherModule.Y: ", seven, " and ", b, "\n";

+//  seven := OtherModule.X.F(15);

+//  assert seven == 7;

+//  b := OtherModule.X.P(real(seven));

+//  print "From OtherModule.X: ", seven, " and ", b, "\n";

+

+  TestFields.Test();

+}

+

+module OtherModule {

+  trait Y {

+    static function method F(x: int): int

+    { x / 2 }

+    static method P(t: real) returns (f: bool)

+    {

+      print "This is OtherModule.P(", t, ")\n";

+      f := t < 10.0;

+    }

+  }

+  class X extends Y {

+  }

+}

+

+

+module TestFields {

+  trait J {

+    var f: int

+  }

+

+  class C extends J {

+  }

+

+  method Test() {

+    var c := new C;

+    var j: J := c;

+

+    c.f := 15;

+    assert j.f == 15;

+    print "c.f= ", c.f, " j.f= ", j.f, "\n";

+    j.f := 18;

+    assert c.f == 18;

+    print "c.f= ", c.f, " j.f= ", j.f, "\n";

+  }

 }

diff --git a/Test/dafny0/Trait/TraitCompile.dfy.expect b/Test/dafny0/Trait/TraitCompile.dfy.expect
index f4f346de..2b4f82c1 100644
--- a/Test/dafny0/Trait/TraitCompile.dfy.expect
+++ b/Test/dafny0/Trait/TraitCompile.dfy.expect
@@ -1,5 +1,5 @@
 

-Dafny program verifier finished with 23 verified, 0 errors

+Dafny program verifier finished with 22 verified, 0 errors

 Program compiled successfully

 Running...

 

@@ -9,10 +9,10 @@ d=800
 a5=407
 t=1212
 z=30
-z'=30
-w=30
 d=1000
 a5=507
 t=1512
-t=1512
-t=1515
+This is OtherModule.P((7.0 / 1.0))
+From OtherModule.Y: 7 and True
+c.f= 15 j.f= 15
+c.f= 18 j.f= 18
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect
index 1e7bface..fefed2f2 100644
--- a/Test/dafny0/Trait/TraitOverride0.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect
@@ -1,5 +1,5 @@
-TraitOverride0.dfy(53,20): Error: a class cannot override implemented functions

+TraitOverride0.dfy(53,20): Error: member 'Mul' in class 'C1' overrides fully defined function inherited from trait 'T1'

 TraitOverride0.dfy(48,20): Error: function 'BodyLess1' is declared with a different number of parameter (1 instead of 0) than the corresponding function in the module it overrides

-TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess1

-TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess2

+TraitOverride0.dfy(65,6): Error: class 'C2' does not implement trait function 'T1.BodyLess1'

+TraitOverride0.dfy(65,6): Error: class 'C2' does not implement trait function 'T1.BodyLess2'

 4 resolution/type errors detected in TraitOverride0.dfy

diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect
index 85c793d4..26aac19c 100644
--- a/Test/dafny0/Trait/TraitOverride1.dfy.expect
+++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 58 verified, 0 errors

+Dafny program verifier finished with 50 verified, 0 errors

diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
index ebda3b9f..9960c1d9 100644
--- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
+++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect
@@ -5,4 +5,4 @@ Execution trace:
     (0,0): anon2

     (0,0): anon6_Then

 

-Dafny program verifier finished with 9 verified, 1 error

+Dafny program verifier finished with 7 verified, 1 error