From 77143c833cbb14a20c704fb60fc28dd94edb44eb Mon Sep 17 00:00:00 2001 From: Reza Ahmadi Date: Fri, 18 Jul 2014 21:16:40 +0300 Subject: added trait feature: -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods --- Source/Dafny/Printer.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/Dafny/Printer.cs') diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1da5e7b2..6e10e7a1 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -264,7 +264,7 @@ namespace Microsoft.Dafny { public void PrintClass(ClassDecl c, int indent) { Contract.Requires(c != null); Indent(indent); - PrintClassMethodHelper("class", c.Attributes, c.Name, c.TypeArgs); + PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); if (c.Members.Count == 0) { wr.WriteLine(" { }"); } else { -- cgit v1.2.3 From 498bff41addc9ca481926f668fb6b69b17b9deda Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 5 Aug 2014 10:06:39 -0700 Subject: Resolved further merge issues --- Source/Dafny/Cloner.cs | 7 - Source/Dafny/Printer.cs | 3 + Source/Dafny/Resolver.cs | 323 ++++++++++----------- Test/dafny0/ResolutionErrors.dfy | 10 + Test/dafny0/ResolutionErrors.dfy.expect | 3 +- Test/dafny0/Trait/TraitBasix.dfy.expect | 4 +- Test/dafny0/Trait/TraitMultiModule.dfy.expect | 2 +- Test/dafny0/Trait/TraitOverride0.dfy.expect | 2 +- Test/dafny0/Trait/TraitOverride1.dfy.expect | 2 +- .../Trait/TraitUsingParentMembers.dfy.expect | 2 +- 10 files changed, 175 insertions(+), 183 deletions(-) (limited to 'Source/Dafny/Printer.cs') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index cbd27f74..203dbef4 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -136,19 +136,14 @@ namespace Microsoft.Dafny 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; //we do need this information in ResolveClassMemberTypes method return field; } else if (member is Function) { var f = (Function)member; - f.Inherited = member.Inherited; Function func = CloneFunction(f); - func.Inherited = member.Inherited; return func; } else { var m = (Method)member; - m.Inherited = member.Inherited; Method method = CloneMethod(m); - method.Inherited = member.Inherited; return method; } } @@ -190,8 +185,6 @@ namespace Microsoft.Dafny public Formal CloneFormal(Formal formal) { Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost); - if (f.Type is UserDefinedType && formal.Type is UserDefinedType) - ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(formal.Type)).ResolvedClass; return f; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 6e10e7a1..a96efb8b 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -265,6 +265,9 @@ namespace Microsoft.Dafny { Contract.Requires(c != null); Indent(indent); PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs); + if (c.TraitId != null) { + wr.Write(" extends {0}", c.TraitId.val); + } if (c.Members.Count == 0) { wr.WriteLine(" { }"); } else { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d1ae1627..d391ab4e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -136,12 +136,12 @@ namespace Microsoft.Dafny return nm; } } - //Dictionary> allDatatypeCtors; + //Dictionary> allDatatypeCtors; - readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>(); - readonly Dictionary/*!*/>/*!*/ datatypeMembers = new Dictionary/*!*/>(); - readonly Dictionary/*!*/>/*!*/ datatypeCtors = new Dictionary/*!*/>(); - readonly Graph/*!*/ dependencies = new Graph(); + readonly Dictionary> classMembers = new Dictionary>(); + readonly Dictionary> datatypeMembers = new Dictionary>(); + readonly Dictionary> datatypeCtors = new Dictionary>(); + readonly Graph dependencies = new Graph(); private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; private RefinementTransformer refinementTransformer = null; @@ -1457,6 +1457,14 @@ namespace Microsoft.Dafny allTypeParameters.PopMarker(); } + // Now that all traits have been resolved, let classes inherit the trait members + foreach (var d in declarations) { + var cl = d as ClassDecl; + if (cl != null) { + InheritTraitMembers(cl); + } + } + // perform acyclicity test on type synonyms var cycle = typeSynonymDependencies.TryFindCycle(); if (cycle != null) { @@ -1478,7 +1486,7 @@ namespace Microsoft.Dafny Contract.Assert(d != null); if (d is TraitDecl && d.TypeArgs != null && d.TypeArgs.Count > 0) { - Error(d, "a trait can not declare type parameters"); + Error(d, "a trait cannot declare type parameters"); } allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, false, d); @@ -2763,13 +2771,33 @@ namespace Microsoft.Dafny /// /// Assumes type parameters have already been pushed /// - void ResolveClassMemberTypes(ClassDecl/*!*/ cl) { + void ResolveClassMemberTypes(ClassDecl cl) { Contract.Requires(cl != null); Contract.Requires(currentClass == null); Contract.Ensures(currentClass == null); currentClass = cl; - RefinementCloner cloner = new RefinementCloner(cl.Module); + + // Resolve names of traits extended + if (cl.TraitId != null) { + var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val); + if (trait == null) { + Error(cl.TraitId, "unresolved identifier: {0}", cl.TraitId.val); + } else if (!(trait is TraitDecl)) { + Error(cl.TraitId, "identifier '{0}' does not denote a trait", cl.TraitId.val); + } else { + //disallowing inheritance in multi module case + string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty); + string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty); + if (clModName != traitModName) { + Error(cl.TraitId, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module", + cl.FullName, trait.FullName)); + } else { + cl.Trait = (TraitDecl)trait; + } + } + } + foreach (MemberDecl member in cl.Members) { member.EnclosingClass = cl; if (member is Field) { @@ -2814,165 +2842,126 @@ namespace Microsoft.Dafny } } + currentClass = null; + } + + void InheritTraitMembers(ClassDecl cl) { + Contract.Requires(cl != null); + //merging class members with parent members if any - if (cl.TraitId != null) - { - //resolving trait: making sure if the given qualifed name is a Trait - var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val); - if (trait != null && trait is TraitDecl) - { - //disallowing inheritance in multi module case - string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty); - string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty); - if (clModName != traitModName) - { - Error(cl, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module", - cl.FullName, trait.FullName)); + if (cl.Trait != null) { + var clMembers = classMembers[cl]; + var traitMembers = classMembers[cl.Trait]; + //merging current class members with the inheriting trait + foreach (KeyValuePair 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); + + //checking specifications + //class method must provide its own specifications in case the overriden method has provided any + if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req + { + Error(classMethod, "Method must provide its own Requires clauses anew"); + } + if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens + { + Error(classMethod, "Method must provide its own Ensures clauses anew"); + } + if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod + { + Error(classMethod, "Method must provide its own Modifies clauses anew"); + } + if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases + { + Error(classMethod, "Method must provide its own Decreases clauses anew"); + } } - else - { - cl.Trait = (TraitDecl)trait; - var traitMembers = classMembers[trait]; - //merging current class members with the inheriting trait - foreach (KeyValuePair traitMem in traitMembers) - { - object clMember = cl.Members.FirstOrDefault(clMem => clMem.CompileName == traitMem.Key); - if (clMember != null) - { - //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; - Method classMethod = (Method)clMember; - //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod); - if (traitMethod.Body != null && !classMembers[cl][classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent - Error(classMethod, "a class can not 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); - - //checking specifications - //class method must provide its own specifications in case the overriden method has provided any - if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req - { - Error(classMethod, "Method must provide its own Requires clauses anew"); - } - if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens - { - Error(classMethod, "Method must provide its own Ensures clauses anew"); - } - if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod - { - Error(classMethod, "Method must provide its own Modifies clauses anew"); - } - if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases - { - Error(classMethod, "Method must provide its own Decreases clauses anew"); - } - } - } - 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 can not override implemented functions"); - else - { - classFunction.OverriddenFunction = traitFunction; - //adding a call graph edge from the trait method to that of class - cl.Module.CallGraph.AddEdge(traitFunction, classFunction); - - //checking specifications - //class function must provide its own specifications in case the overriden function has provided any - if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req - { - Error(classFunction, "Function must provide its own Requires clauses anew"); - } - if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens - { - Error(classFunction, "Function must provide its own Ensures clauses anew"); - } - if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod - { - Error(classFunction, "Function must provide its own Reads clauses anew"); - } - if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases - { - Error(classFunction, "Function must provide its own Decreases clauses anew"); - } - } - } - else if (traitMem.Value is Field) - { - Field traitField = (Field)traitMem.Value; - Field classField = (Field)clMember; - if (!classMembers[cl][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 - { - MemberDecl classNewMember = cloner.CloneMember(traitMem.Value); - if (classNewMember is Field) - { - Field f = (Field)classNewMember; - if (f.Type is UserDefinedType) - ((UserDefinedType)f.Type).ResolvedClass = ((UserDefinedType)(((Field)(traitMem.Value)).Type)).ResolvedClass; - } - 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 (MemberDecl traitMember in trait.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 + } 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 method to that of class + cl.Module.CallGraph.AddEdge(traitFunction, classFunction); + + //checking specifications + //class function must provide its own specifications in case the overriden function has provided any + if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req + { + Error(classFunction, "Function must provide its own Requires clauses anew"); + } + if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens + { + Error(classFunction, "Function must provide its own Ensures clauses anew"); + } + if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod + { + Error(classFunction, "Function must provide its own Reads clauses anew"); + } + if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases + { + Error(classFunction, "Function must provide its own Decreases clauses anew"); + } + } + } 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 + clMembers.Add(traitMem.Key, traitMem.Value); + } + }//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 (MemberDecl traitMember in cl.Trait.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 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); - } - if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null) - Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName); - } - } - } + 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); } + if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null) + Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName); + } } - else - Error(cl, string.Format("unresolved identifier: {0}", cl.TraitId.val)); + } } - - currentClass = null; } /// @@ -5886,17 +5875,13 @@ namespace Microsoft.Dafny // ---------- new C Contract.Assert(rr.ArrayDimensions == null && rr.OptionalNameComponent == null && rr.InitCall == null); } - if (rr.EType is UserDefinedType) - { - if (((UserDefinedType)rr.EType).ResolvedClass is TraitDecl) - { - Error(stmt, "new can not be applied to a trait"); - } - } - if (!callsConstructor && rr.EType.NormalizeExpand() is UserDefinedType) { + if (rr.EType.NormalizeExpand() is UserDefinedType) { var udt = (UserDefinedType)rr.EType.NormalizeExpand(); var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test - if (cl.HasConstructor) { + if (cl is TraitDecl) { + Error(stmt, "new cannot be applied to a trait"); + } + if (!callsConstructor && cl.HasConstructor) { Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name); } } diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index aaf1291c..9f6c948a 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1090,3 +1090,13 @@ module OpaqueTypes1 { assert p != q; // error: types must be the same in order to do compare } } + +// ----- new trait ------------------------------------------- + + +trait J { } +type JJ = J +method TraitSynonym() +{ + var x := new JJ; // error: new cannot be applied to a trait +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index d5d12eb9..b11fa9f8 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -172,4 +172,5 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real) ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int) ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat) -174 resolution/type errors detected in ResolutionErrors.dfy +ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait +175 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect index 1d44d0f6..4a908ee7 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy.expect +++ b/Test/dafny0/Trait/TraitBasix.dfy.expect @@ -1,7 +1,7 @@ +TraitBasix.dfy(91,23): Error: unresolved identifier: IX TraitBasix.dfy(77,13): Error: member in the class has been already inherited from its parent trait TraitBasix.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable TraitBasix.dfy(80,7): Error: class: I0Child2 does not implement trait member: F -TraitBasix.dfy(91,7): Error: unresolved identifier: IX TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor -TraitBasix.dfy(117,10): Error: new can not be applied to a trait +TraitBasix.dfy(117,10): Error: new cannot be applied to a trait 6 resolution/type errors detected in TraitBasix.dfy diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect index 589fba07..b9031dac 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -1,2 +1,2 @@ -TraitMultiModule.dfy(21,9): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module +TraitMultiModule.dfy(21,20): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module 1 resolution/type errors detected in TraitMultiModule.dfy diff --git a/Test/dafny0/Trait/TraitOverride0.dfy.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect index 4020b880..1e7bface 100644 --- a/Test/dafny0/Trait/TraitOverride0.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect @@ -1,4 +1,4 @@ -TraitOverride0.dfy(53,20): Error: a class can not override implemented functions +TraitOverride0.dfy(53,20): Error: a class cannot override implemented functions 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 diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect index 0f7b49e3..c90560b0 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 62 verified, 0 errors +Dafny program verifier finished with 52 verified, 0 errors diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect index 6849499c..b59d7b80 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 -- cgit v1.2.3