diff options
| author |  qunyanm <unknown> | 2015-04-06 10:35:55 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-06 10:35:55 -0700 |
| commit | 8cac7f02bde3364c92763c26b0f75c1b5feef944 (patch) | |
| tree | 6dad47174675c2209aae74cbbc92af43d928eed5 | |
| parent | ce0649d4207ab1edeea2b26141ad45af7a5ee796 (diff) | |
| parent | 0aeab928abc85e646dc58c4dc4670a03a36cbc2f (diff) | |
Merge
25 files changed, 1007 insertions, 869 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 4972517b..74bdb63e 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -101,6 +101,13 @@ type ref; const null: ref;
// ---------------------------------------------------------------
+// -- Traits -----------------------------------------------------
+// ---------------------------------------------------------------
+
+const unique NoTraitAtAll: ClassName;
+function TraitParent(ClassName): ClassName;
+
+// ---------------------------------------------------------------
// -- Boxing and unboxing ----------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 8552e480..3c266a28 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -105,7 +105,7 @@ namespace Microsoft.Dafny if (d is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
} else {
- return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp);
+ return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType));
}
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index e557e509..7b63f65b 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -215,7 +215,7 @@ namespace Microsoft.Dafny { Indent(indent);
wr.Write("public interface @{0}", trait.CompileName);
wr.WriteLine(" {");
- CompileClassMembers(trait, indent + IndentAmount);
+ CompileClassMembers(trait, false, indent + IndentAmount);
Indent(indent); wr.WriteLine("}");
//writing the _Companion class
@@ -236,27 +236,26 @@ namespace Microsoft.Dafny { }
}
}
- var cl = new ClassDecl(d.tok, d.Name, d.Module, d.TypeArgs, members, d.Attributes, null);
Indent(indent);
- wr.Write("public class @_Companion_{0}", cl.CompileName);
+ wr.Write("public class @_Companion_{0}", trait.CompileName);
wr.WriteLine(" {");
- CompileClassMembers(cl, indent + IndentAmount);
+ CompileClassMembers(trait, true, indent + IndentAmount);
Indent(indent); wr.WriteLine("}");
}
else if (d is ClassDecl) {
var cl = (ClassDecl)d;
Indent(indent);
- if (cl.TraitsObj != null && cl.TraitsObj.Count > 0)
- {
- wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitsStr);
- }
- else
- wr.Write("public class @{0}", cl.CompileName);
+ wr.Write("public class @{0}", cl.CompileName);
if (cl.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(cl.TypeArgs));
}
+ string sep = " : ";
+ foreach (var trait in cl.TraitsTyp) {
+ wr.Write("{0}{1}", sep, TypeName(trait));
+ sep = ", ";
+ }
wr.WriteLine(" {");
- CompileClassMembers(cl, indent+IndentAmount);
+ CompileClassMembers(cl, false, indent+IndentAmount);
Indent(indent); wr.WriteLine("}");
} else if (d is ModuleDecl) {
// nop
@@ -757,193 +756,151 @@ namespace Microsoft.Dafny { }
}
-
- void CompileClassMembers(ClassDecl c, int indent)
- {
+ void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent) {
Contract.Requires(c != null);
+ Contract.Requires(!forCompanionClass || c is TraitDecl);
+ Contract.Requires(0 <= indent);
foreach (MemberDecl member in c.Members) {
if (member is Field) {
- Field f = (Field)member;
- if (!f.IsGhost) {
- if (c is TraitDecl)
- {
- {
- Indent(indent);
- wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);
- wr.Write(" {");
- wr.Write(" get; set; ");
- wr.WriteLine("}");
- }
- }
- 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));
- }
- }
+ var f = (Field)member;
+ if (f.IsGhost || forCompanionClass) {
+ // emit nothing
+ } else if (c is TraitDecl) {
+ 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));
}
} else if (member is Function) {
- Function f = (Function)member;
- if (c is TraitDecl)
- {
- if (member.IsStatic && f.Body == null)
- {
- Error("Function {0} has no body", f.FullName);
- }
- else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait
- {
- Indent(indent);
- wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);
- wr.Write("(");
- WriteFormals("", f.Formals);
- wr.WriteLine(");");
- }
- }
- else
- {
- if (f.Body == null)
- {
- if (!Attributes.Contains(f.Attributes, "axiom"))
- {
- Error("Function {0} has no body", f.FullName);
- }
- }
- else if (f.IsGhost)
- {
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(f.Body);
- }
- 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("}");
- }
+ var f = (Function)member;
+ if (f.Body == null && !(c is TraitDecl && !f.IsStatic)) {
+ // A (ghost or non-ghost) function must always have a body, except if it's an instance function in a trait.
+ if (forCompanionClass || Attributes.Contains(f.Attributes, "axiom")) {
+ // suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)
+ } else {
+ Error("Function {0} has no body", f.FullName);
+ }
+ } else if (f.IsGhost) {
+ // nothing to compile, but we do check for assumes
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(f.Body);
+ } else if (c is TraitDecl && !forCompanionClass) {
+ // include it, unless it's static
+ if (!f.IsStatic) {
+ Indent(indent);
+ wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);
+ wr.Write("(");
+ WriteFormals("", f.Formals);
+ wr.WriteLine(");");
+ }
+ } 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("}");
}
} else if (member is Method) {
- Method m = (Method)member;
- if (c is TraitDecl)
- {
- if (member.IsStatic && m.Body == null)
- {
- Error("Method {0} has no body", m.FullName);
- }
- else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait
- {
- Indent(indent);
- wr.Write("void @{0}", m.CompileName);
- wr.Write("(");
- int nIns = WriteFormals("", m.Ins);
- WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
- wr.WriteLine(");");
- }
- }
- else
- {
- if (m.Body == null)
- {
- if (!Attributes.Contains(m.Attributes, "axiom"))
- {
- Error("Method {0} has no body", m.FullName);
- }
+ var m = (Method)member;
+ if (m.Body == null && !(c is TraitDecl && !m.IsStatic)) {
+ // A (ghost or non-ghost) method must always have a body, except if it's an instance method in a trait.
+ if (forCompanionClass || Attributes.Contains(m.Attributes, "axiom")) {
+ // suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)
+ } else {
+ Error("Method {0} has no body", m.FullName);
+ }
+ } else if (m.IsGhost) {
+ // nothing to compile, but we do check for assumes
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(m.Body);
+ } else if (c is TraitDecl && !forCompanionClass) {
+ // include it, unless it's static
+ if (!m.IsStatic) {
+ Indent(indent);
+ wr.Write("void @{0}", m.CompileName);
+ wr.Write("(");
+ int nIns = WriteFormals("", m.Ins);
+ WriteFormals(nIns == 0 ? "" : ", ", m.Outs);
+ wr.WriteLine(");");
+ }
+ } 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));
}
- else if (m.IsGhost)
- {
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(m.Body);
+ }
+ 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;");
+ }
}
- 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("}");
- }
+ 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("}");
+ }
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member
@@ -975,6 +932,22 @@ namespace Microsoft.Dafny { return null;
}
+ string TypeName_Companion(Type type) {
+ Contract.Requires(type != null);
+ var udt = type as UserDefinedType;
+ if (udt != null && udt.ResolvedClass is TraitDecl) {
+ string s = udt.FullCompanionCompileName;
+ if (udt.TypeArgs.Count != 0) {
+ if (udt.TypeArgs.Exists(argType => argType is ObjectType)) {
+ Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");
+ }
+ s += "<" + TypeNames(udt.TypeArgs) + ">";
+ }
+ return s;
+ } else {
+ return TypeName(type);
+ }
+ }
string TypeName(Type type)
{
Contract.Requires(type != null);
@@ -1882,14 +1855,7 @@ namespace Microsoft.Dafny { wr.Write("@" + receiverReplacement);
} else if (s.Method.IsStatic) {
Indent(indent);
- if (s.Receiver.Type is UserDefinedType && ((UserDefinedType)s.Receiver.Type).ResolvedClass is TraitDecl)
- {
- wr.Write("@_Companion_{0}", TypeName(cce.NonNull(s.Receiver.Type)).Replace("@", string.Empty));
- }
- else
- {
- wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
- }
+ wr.Write(TypeName_Companion(s.Receiver.Type));
} else {
Indent(indent);
TrParenExpr(s.Receiver);
@@ -2957,7 +2923,7 @@ namespace Microsoft.Dafny { void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, FCE_Arg_Translator tr) {
Function f = cce.NonNull(e.Function);
if (f.IsStatic) {
- twr.Write(TypeName(cce.NonNull(e.Receiver.Type)));
+ twr.Write(TypeName_Companion(e.Receiver.Type));
} else {
twr.Write("(");
tr(e.Receiver);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ed089f10..02d729b4 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -994,6 +994,13 @@ namespace Microsoft.Dafny { }
}
}
+ public string FullCompanionCompileName {
+ get {
+ Contract.Requires(ResolvedClass is TraitDecl);
+ var s = ResolvedClass.Module.IsDefaultModule ? "" : ResolvedClass.Module.CompileName + ".";
+ return s + "@_Companion_" + CompileName;
+ }
+ }
public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype/iterator and TypeArgs match the type parameters of that class/datatype/iterator
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
@@ -1865,12 +1872,14 @@ namespace Microsoft.Dafny { public class ClassDecl : TopLevelDecl {
public override string WhatKind { get { return "class"; } }
public readonly List<MemberDecl> Members;
- public List<TraitDecl> TraitsObj;
- public readonly List<Type> TraitsTyp;
+ 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
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Members));
+ Contract.Invariant(TraitsTyp != null);
+ Contract.Invariant(TraitsObj != null);
}
public ClassDecl(IToken tok, string name, ModuleDefinition module,
@@ -1882,42 +1891,18 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(members));
Members = members;
- //if (traits != null)
- TraitsTyp = traits;
+ TraitsTyp = traits ?? new List<Type>();
}
public virtual bool IsDefaultClass {
get {
return false;
}
}
-
- public string TraitsStr
- {
- get
- {
- if (TraitsTyp == null || TraitsTyp.Count == 0)
- return string.Empty;
- StringBuilder sb = new StringBuilder();
- foreach (Type ty in TraitsTyp)
- {
- if (ty is UserDefinedType)
- {
- sb.Append(((UserDefinedType)(ty)).Name);
- sb.Append(",");
- }
- }
- if (sb.Length > 0)
- {
- sb.Remove(sb.Length - 1, 1);
- }
- return sb.ToString();
- }
- }
}
public class DefaultClassDecl : ClassDecl {
public DefaultClassDecl(ModuleDefinition module, [Captured] List<MemberDecl> members)
- : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null,null) {
+ : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null, null) {
Contract.Requires(module != null);
Contract.Requires(cce.NonNullElements(members));
}
@@ -1934,7 +1919,7 @@ namespace Microsoft.Dafny { public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)
: base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,
new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),
- new List<MemberDecl>(), attrs,null)
+ new List<MemberDecl>(), attrs, null)
{
Contract.Requires(1 <= dims);
Contract.Requires(module != null);
@@ -2218,7 +2203,7 @@ namespace Microsoft.Dafny { List<MaybeFreeExpression> yieldRequires,
List<MaybeFreeExpression> yieldEnsures,
BlockStmt body, Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes,null)
+ : base(tok, name, module, typeArgs, new List<MemberDecl>(), attributes, null)
{
Contract.Requires(tok != null);
Contract.Requires(name != null);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index b8c99b00..5fa232f1 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -319,8 +319,11 @@ namespace Microsoft.Dafny { Contract.Requires(c != null);
Indent(indent);
PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
- if (c.TraitsStr!=string.Empty) {
- wr.Write(" extends {0}", c.TraitsStr);
+ string sep = " extends ";
+ foreach (var trait in c.TraitsTyp) {
+ wr.Write(sep);
+ PrintType(trait);
+ sep = ", ";
}
if (c.Members.Count == 0) {
wr.WriteLine(" { }");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bf417de7..0e8e0ec3 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2837,39 +2837,24 @@ namespace Microsoft.Dafny currentClass = cl;
// Resolve names of traits extended
- if (cl.TraitsTyp != null)
- {
- cl.TraitsObj = new List<TraitDecl>();
- foreach (Type traitTyp in cl.TraitsTyp)
- {
- if (traitTyp is UserDefinedType)
- {
- var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == ((UserDefinedType)(traitTyp)).FullCompileName);
- if (trait == null)
- {
- Error(((UserDefinedType)(traitTyp)).tok, "unresolved identifier: {0}", ((UserDefinedType)(traitTyp)).tok.val);
- }
- else if (!(trait is TraitDecl))
- {
- Error(((UserDefinedType)(traitTyp)).tok, "identifier '{0}' does not denote a trait", ((UserDefinedType)(traitTyp)).tok.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(((UserDefinedType)(traitTyp)).tok, 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.TraitsObj.Add((TraitDecl)trait);
- }
- }
- }
+ foreach (var tt in cl.TraitsTyp) {
+ var prevErrorCount = ErrorCount;
+ ResolveType(cl.tok, tt, new NoContext(cl.Module), ResolveTypeOptionEnum.DontInfer, null);
+ if (ErrorCount == prevErrorCount) {
+ var udt = tt as UserDefinedType;
+ if (udt != null && udt.ResolvedClass is TraitDecl) {
+ var trait = (TraitDecl)udt.ResolvedClass;
+ //disallowing inheritance in multi module case
+ if (cl.Module != trait.Module) {
+ Error(udt.tok, "class '{0}' is in a different module than trait '{1}'. A class may only extend a trait in the same module.", cl.Name, trait.FullName);
+ } else {
+ // all is good
+ cl.TraitsObj.Add(trait);
+ }
+ } else {
+ Error(udt != null ? udt.tok : cl.tok, "a class can only extend traits (found '{0}')", tt);
}
+ }
}
foreach (MemberDecl member in cl.Members) {
@@ -2952,25 +2937,6 @@ namespace Microsoft.Dafny 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)
@@ -2985,25 +2951,6 @@ namespace Microsoft.Dafny classFunction.OverriddenFunction = traitFunction;
//adding a call graph edge from the trait function 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)
@@ -3058,6 +3005,11 @@ namespace Microsoft.Dafny {
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);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9160248c..2672258d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -155,6 +155,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type Ty;
public readonly Bpl.Type TyTag;
public readonly Bpl.Expr Null;
+ public readonly Bpl.Expr NoTraitAtAll;
private readonly Bpl.Constant allocField;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -178,6 +179,7 @@ namespace Microsoft.Dafny { Contract.Invariant(Ty != null);
Contract.Invariant(TyTag != null);
Contract.Invariant(Null != null);
+ Contract.Invariant(NoTraitAtAll != null);
Contract.Invariant(allocField != null);
}
@@ -282,6 +284,7 @@ namespace Microsoft.Dafny { this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new List<Bpl.Type>());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
+ this.NoTraitAtAll = new Bpl.IdentifierExpr(Token.NoToken, "NoTraitAtAll", ClassNameType);
}
}
@@ -537,8 +540,7 @@ namespace Microsoft.Dafny { }
}
- //adding TraitParent function and axioms
- AddTraitParentFuncAndAxioms();
+ AddTraitParentAxioms();
if (InsertChecksums)
{
@@ -561,35 +563,24 @@ namespace Microsoft.Dafny { return sink;
}
- //adding TraitParent function and axioms
- //if a class A extends trait J and B does not extned anything, then this method adds the followings to the sink:
- // const unique NoTraitAtAll: ClassName;
- // function TraitParent(ClassName): ClassName;
- // axiom TraitParent(class.A) == class.J;
- // axiom TraitParent(class.B) == NoTraitAtAll;
- private void AddTraitParentFuncAndAxioms()
+ /// <summary>
+ /// adding TraitParent axioms
+ /// if a class A extends trait J and B does not extend anything, then this method adds the followings to the sink:
+ /// axiom TraitParent(class.A) == class.J;
+ /// axiom TraitParent(class.B) == NoTraitAtAll;
+ /// </summary>
+ private void AddTraitParentAxioms()
{
foreach (ModuleDefinition m in program.Modules)
{
- if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj != null && ((ClassDecl)d).TraitsObj.Count > 0) || (d is TraitDecl)))
+ if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitsObj.Count > 0) || (d is TraitDecl)))
{
- //adding const unique NoTraitAtAll: ClassName;
- Token tNoTrait = new Token();
- Token tTraitParent = new Token();
- Bpl.Constant cNoTrait = new Bpl.Constant(tNoTrait, new Bpl.TypedIdent(tNoTrait, "NoTraitAtAll", predef.ClassNameType), true);
- sink.AddTopLevelDeclaration(cNoTrait);
- //adding function TraitParent(ClassName): ClassName;
- var arg_ref = new Bpl.Formal(tTraitParent, new Bpl.TypedIdent(tTraitParent, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var res = new Bpl.Formal(tTraitParent, new Bpl.TypedIdent(tTraitParent, Bpl.TypedIdent.NoName, predef.ClassNameType), false);
- var fTraitParent = new Bpl.Function(tTraitParent, "TraitParent", new List<Variable> { arg_ref }, res);
- sink.AddTopLevelDeclaration(fTraitParent);
-
foreach (TopLevelDecl d in m.TopLevelDecls)
{
if (d is ClassDecl)
{
var c = (ClassDecl)d;
- if (c is ClassDecl && c.TraitsObj != null && c.TraitsObj.Count > 0)
+ if (c.TraitsObj.Count > 0)
{
foreach (TraitDecl traitObj in c.TraitsObj)
{
@@ -598,27 +589,18 @@ namespace Microsoft.Dafny { Bpl.Constant trait = new Bpl.Constant(traitObj.tok, trait_id, true);
Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(traitObj.tok, trait);
- var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);
- var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "TraitParent", new List<Variable> { args }, ret_value));
- var funCallExpr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
+ var id = new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType);
+ var funCallExpr = FunctionCall(c.tok, BuiltinFunction.TraitParent, null, id);
var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, traitId_expr));
sink.AddTopLevelDeclaration(traitParentAxiom);
}
}
- else if (c is ClassDecl && (c.TraitsObj == null || c.TraitsObj.Count == 0))
+ else
{
- //this adds: axiom TraitParent(class.B) == NoTraitAtAll; Where B does not extend any traits
- Bpl.TypedIdent noTraitAtAll_id = new Bpl.TypedIdent(c.tok, "NoTraitAtAll", predef.ClassNameType);
- Bpl.Constant noTraitAtAll = new Bpl.Constant(c.tok, noTraitAtAll_id, true);
- Bpl.Expr noTraitAtAll_expr = new Bpl.IdentifierExpr(c.tok, noTraitAtAll);
-
- var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);
- var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "TraitParent", new List<Variable> { args }, ret_value));
- var funCallExpr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
- var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, noTraitAtAll_expr));
+ var id = new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType);
+ var funCallExpr = FunctionCall(c.tok, BuiltinFunction.TraitParent, null, id);
+ var traitParentAxiom = new Bpl.Axiom(c.tok, Bpl.Expr.Eq(funCallExpr, predef.NoTraitAtAll));
sink.AddTopLevelDeclaration(traitParentAxiom);
}
@@ -1365,7 +1347,7 @@ namespace Microsoft.Dafny { {
var t = (TraitDecl)c;
var dtypeFunc = FunctionCall(o.tok, BuiltinFunction.DynamicType, null, o);
- Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
+ Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.FullSanitizedName, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
rhs = BplOr(o_null, implementsFunc);
}
else
@@ -1380,34 +1362,20 @@ namespace Microsoft.Dafny { });
}
- //this adds: function implements$J(ClassName): bool;
- if (c is TraitDecl)
- {
- var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- var implement_intr = new Bpl.Function(c.tok, "implements$" + c.Name, new List<Variable> { arg_ref }, res);
- sink.AddTopLevelDeclaration(implement_intr);
- }
- //this adds: axiom implements$J(class.C);
- else if (c is ClassDecl)
- {
- if (c.TraitsObj != null && c.TraitsObj.Count > 0)
- {
- //var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);
- //Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
- foreach (Type traitType in c.TraitsTyp)
- {
- if (traitType is UserDefinedType)
- {
- var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
- var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + ((UserDefinedType)(traitType)).tok, new List<Variable> { args }, ret_value));
- var expr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
- var implements_axiom = new Bpl.Axiom(c.tok, expr);
- sink.AddTopLevelDeclaration(implements_axiom);
- }
- }
- }
+ if (c is TraitDecl) {
+ //this adds: function implements$J(Ty): bool;
+ var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.Ty), true);
+ var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
+ var implement_intr = new Bpl.Function(c.tok, "implements$" + c.FullSanitizedName, new List<Variable> { arg_ref }, res);
+ sink.AddTopLevelDeclaration(implement_intr);
+ } else if (c is ClassDecl) {
+ //this adds: axiom implements$J(class.C);
+ foreach (var trait in c.TraitsObj) {
+ var arg = ClassTyCon(c, new List<Expr>()); // TODO: this needs more work if overridingClass has type parameters
+ var expr = FunctionCall(c.tok, "implements$" + trait.FullSanitizedName, Bpl.Type.Bool, arg);
+ var implements_axiom = new Bpl.Axiom(c.tok, expr);
+ sink.AddTopLevelDeclaration(implements_axiom);
+ }
}
foreach (MemberDecl member in c.Members) {
@@ -1514,7 +1482,7 @@ namespace Microsoft.Dafny { AddFrameAxiom(f);
// add consequence axiom
sink.AddTopLevelDeclaration(FunctionConsequenceAxiom(f, f.Ens));
- // add definition axioms, suitably specialized for "match" cases and for literals
+ // add definition axioms, suitably specialized for literals
if (f.Body != null && !IsOpaqueFunction(f)) {
AddFunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, f.Body.Resolved);
AddFunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, f.Body.Resolved);
@@ -2097,10 +2065,11 @@ namespace Microsoft.Dafny { }
}
- Bpl.Axiom FunctionAxiom(Function f, FunctionAxiomVisibility visibility, Expression body, ICollection<Formal> lits) {
+ Bpl.Axiom FunctionAxiom(Function f, FunctionAxiomVisibility visibility, Expression body, ICollection<Formal> lits, TopLevelDecl overridingClass = null) {
Contract.Requires(f != null);
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
+ Contract.Requires(!f.IsStatic || overridingClass == null);
// only if body is null, we will return null:
Contract.Ensures((Contract.Result<Bpl.Axiom>() == null) == (body == null));
@@ -2114,7 +2083,8 @@ namespace Microsoft.Dafny { // ==>
// (forall s, $Heap, formals :: // let args := $Heap,formals
// { f(Succ(s), args) } // (*)
- // f#canCall(args) || USE_VIA_CONTEXT
+ // (f#canCall(args) || USE_VIA_CONTEXT) &&
+ // dtype(this) == overridingClass // if "overridingClass" != null
// ==>
// BODY-can-make-its-calls &&
// f(Succ(s), args) == BODY); // (*)
@@ -2178,6 +2148,7 @@ namespace Microsoft.Dafny { // ante: $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
+ Bpl.Expr additionalAntecedent = null;
if (!f.IsStatic) {
var bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, etran.This, predef.RefType));
formals.Add(bvThis);
@@ -2189,6 +2160,10 @@ namespace Microsoft.Dafny { Bpl.Expr.Neq(bvThisIdExpr, predef.Null),
etran.GoodRef(f.tok, bvThisIdExpr, thisType));
ante = Bpl.Expr.And(ante, wh);
+ if (overridingClass != null) {
+ // additionalAntecednet := dtype(this) == overridingClass
+ additionalAntecedent = DType(bvThisIdExpr, ClassTyCon(overridingClass, new List<Expr>())); // TODO: this needs more work if overridingClass has type parameters
+ }
}
var substMap = new Dictionary<IVariable, Expression>();
@@ -2225,11 +2200,13 @@ namespace Microsoft.Dafny { // Add the precondition function and its axiom (which is equivalent to the ante)
if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) {
- var precondF = new Bpl.Function(f.tok,
- RequiresName(f), new List<Bpl.TypeVariable>(),
- formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),
- BplFormalVar(null, Bpl.Type.Bool, false));
- sink.AddTopLevelDeclaration(precondF);
+ if (overridingClass == null) {
+ var precondF = new Bpl.Function(f.tok,
+ RequiresName(f), new List<Bpl.TypeVariable>(),
+ formals.ConvertAll(v => (Bpl.Variable)BplFormalVar(null, v.TypedIdent.Type, true)),
+ BplFormalVar(null, Bpl.Type.Bool, false));
+ sink.AddTopLevelDeclaration(precondF);
+ }
var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool,
formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x))));
sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante))));
@@ -2246,6 +2223,9 @@ namespace Microsoft.Dafny { // ante := useViaCanCall || (useViaContext && typeAnte && pre)
ante = Bpl.Expr.Or(useViaCanCall, ante);
+ if (additionalAntecedent != null) {
+ ante = Bpl.Expr.And(ante, additionalAntecedent);
+ }
Bpl.Expr funcAppl;
{
@@ -2287,7 +2267,11 @@ namespace Microsoft.Dafny { Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, kv, tr, Bpl.Expr.Imp(ante, meat));
var activate = AxiomActivation(f, visibility == FunctionAxiomVisibility.ForeignModuleOnly, visibility == FunctionAxiomVisibility.IntraModuleOnly, etran);
string comment;
- comment = "definition axiom for " + f.FullSanitizedName;
+ if (overridingClass == null) {
+ comment = "definition axiom for " + f.FullSanitizedName;
+ } else {
+ comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingClass.FullSanitizedName;
+ }
if (lits != null) {
if (lits.Count == f.Formals.Count) {
comment += " for all literals";
@@ -3056,67 +3040,32 @@ namespace Microsoft.Dafny { private void AddFunctionOverrideAxiom(Function f)
{
- Contract.Requires(f != null);
- Contract.Requires(sink != null && predef != null);
- // function override axiom
- // axiom (forall $heap: HeapType, this: ref, x#0: int ::
- // { J.F($heap, this, x#0) }
- // this != null && dtype(this) == class.C
- // ==>
- // J.F($heap, this, x#0) == C.F($heap, this, x#0));
-
- var formals = new List<Variable>();
- var argsC = new List<Bpl.Expr>();
- var argsT = new List<Bpl.Expr>();
-
- var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType));
- var s = new Bpl.IdentifierExpr(f.tok, bv);
- if (f.IsRecursive)
- {
- formals.Add(bv);
- argsC.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));
- argsT.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s));
- }
-
- bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.tok, bv);
- argsC.Add(s);
- argsT.Add(s);
-
- if (!f.IsStatic)
- {
- bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.tok, bv);
- argsC.Add(s);
- argsT.Add(s);
- }
- foreach (var p in f.Formals)
- {
- bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.FullSanitizedName + "_" + p.AssignUniqueName(f.IdGenerator), TrType(p.Type)));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.tok, bv);
- argsC.Add(s);
- }
- foreach (var p in f.OverriddenFunction.Formals)
- {
- bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, f.OverriddenFunction.FullSanitizedName + "_" + p.AssignUniqueName(f.OverriddenFunction.IdGenerator), TrType(p.Type)));
- formals.Add(bv);
- s = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, bv);
- argsT.Add(s);
- }
-
- var funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
- var funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType)));
- var funcApplC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
- var funcApplT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT);
-
- var typeParams = TrTypeParamDecls(f.TypeArgs);
+ Contract.Requires(f != null);
+ Contract.Requires(!f.IsStatic); // only instance functions can be overridden
+ Contract.Requires(sink != null && predef != null);
- Bpl.Trigger tr = new Bpl.Trigger(f.OverriddenFunction.tok, true, new List<Bpl.Expr> { funcApplT, funcApplC });
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(funcApplC, funcApplT));
- sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax, "function override axiom"));
+ // Essentially, the function override axiom looks like:
+ // axiom (forall $heap: HeapType, this: ref, x#0: int ::
+ // { J.F($heap, this, x#0) }
+ // this != null && dtype(this) == class.C
+ // ==>
+ // J.F($heap, this, x#0) == C.F($heap, this, x#0));
+ // but it also has the various usual antecedents. Essentially, the override gives a part of the body of the
+ // trait's function, so we call FunctionAxiom to generate a conditional axiom (that is, we pass in the "overridingClass"
+ // parameter to FunctionAxiom, which will add 'dtype(this) == class.C' as an additional antecedent) for a
+ // body of 'C.F(this, x#0)'.
+ // TODO: More work needs to be done to support any type parameters that class C might have. These would
+ // need to be quantified (existentially?) in the axiom.
+ var receiver = new ThisExpr(f.tok);
+ receiver.Type = Resolver.GetReceiverType(f.tok, f);
+ var args = f.OverriddenFunction.Formals.ConvertAll(p => (Expression)new IdentifierExpr(p.tok, p.Name) { Var = p, Type = p.Type });
+ var pseudoBody = new FunctionCallExpr(f.tok, f.Name, new ThisExpr(f.tok), f.tok, args);
+ pseudoBody.Function = f; // resolve here
+ // TODO: the following two lines (incorrectly) assume there are no type parameters
+ pseudoBody.Type = f.ResultType; // resolve here
+ pseudoBody.TypeArgumentSubstitutions = new Dictionary<TypeParameter,Type>(); // resolve here
+ sink.AddTopLevelDeclaration(FunctionAxiom(f.OverriddenFunction, FunctionAxiomVisibility.IntraModuleOnly, pseudoBody, null, f.EnclosingClass));
+ sink.AddTopLevelDeclaration(FunctionAxiom(f.OverriddenFunction, FunctionAxiomVisibility.ForeignModuleOnly, pseudoBody, null, f.EnclosingClass));
}
private void AddFunctionOverrideEnsChk(Function f, StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap, List<Variable> implInParams)
@@ -3405,33 +3354,68 @@ namespace Microsoft.Dafny { }
}
- private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap)
- {
- var decrToks = new List<IToken>();
- var decrTypes1 = new List<Type>();
- var decrTypes2 = new List<Type>();
- var decrClass = new List<Expr>();
- var decrTrait = new List<Expr>();
- if (m.Decreases != null)
- {
- foreach (var decC in m.Decreases.Expressions)
- {
- decrToks.Add(decC.tok);
- decrTypes1.Add(decC.Type);
- decrClass.Add(etran.TrExpr(decC));
- }
- }
- if (m.OverriddenMethod.Decreases != null)
- {
- foreach (var decT in m.OverriddenMethod.Decreases.Expressions)
- {
- var decCNew = Substitute(decT, null, substMap);
- decrTypes2.Add(decCNew.Type);
- decrTrait.Add(etran.TrExpr(decCNew));
- }
+ private void AddMethodOverrideTerminationChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Dictionary<IVariable, Expression> substMap) {
+ Contract.Requires(m != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(etran != null);
+ Contract.Requires(substMap != null);
+ // Note, it is as if the trait's method is calling the class's method.
+ var contextDecreases = m.OverriddenMethod.Decreases.Expressions;
+ var calleeDecreases = m.Decreases.Expressions;
+ // We want to check: calleeDecreases <= contextDecreases (note, we can allow equality, since there is a bounded, namely 1, number of dynamic dispatches)
+ if (Contract.Exists(contextDecreases, e => e is WildcardExpr)) {
+ // no check needed
+ return;
+ }
+
+ int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);
+ var toks = new List<IToken>();
+ var types0 = new List<Type>();
+ var types1 = new List<Type>();
+ var callee = new List<Expr>();
+ var caller = new List<Expr>();
+
+ for (int i = 0; i < N; i++) {
+ Expression e0 = calleeDecreases[i];
+ Expression e1 = Substitute(contextDecreases[i], null, substMap);
+ if (!CompatibleDecreasesTypes(e0.Type, e1.Type)) {
+ N = i;
+ break;
}
- var decrChk = DecreasesCheck(decrToks, decrTypes1, decrTypes2, decrClass, decrTrait, null, null, true, false);
- builder.Add(new Bpl.AssertCmd(m.tok, decrChk));
+ toks.Add(new NestedToken(m.tok, e1.tok));
+ types0.Add(e0.Type.NormalizeExpand());
+ types1.Add(e1.Type.NormalizeExpand());
+ callee.Add(etran.TrExpr(e0));
+ caller.Add(etran.TrExpr(e1));
+ }
+
+ var decrCountT = contextDecreases.Count;
+ var decrCountC = calleeDecreases.Count;
+ // Generally, we want to produce a check "decrClass <= decrTrait", allowing (the common case where) they are equal.
+ // * If N < decrCountC && N < decrCountT, then "decrClass <= decrTrait" if the comparison ever gets beyond the
+ // parts that survived truncation. Thus, we compare with "allowNoChange" set to "false".
+ // Otherwise:
+ // * If decrCountC == decrCountT, then the truncation we did above had no effect and we pass in "allowNoChange" as "true".
+ // * If decrCountC > decrCountT, then we will have truncated decrClass above. Let x,y and x' denote decrClass and
+ // decrTrait, respectively, where x and x' have the same length. Considering how Dafny in effect pads the end of
+ // decreases tuples with a \top, we were supposed to evaluate (x,(y,\top)) <= (x',\top), which by lexicographic pairs
+ // we can expand to:
+ // x <= x' && (x == x' ==> (y,\top) <= \top)
+ // which is equivalent to just x <= x'. Thus, we called DecreasesCheck to compare x and x' and we pass in "allowNoChange"
+ // as "true".
+ // * If decrCountC < decrCountT, then we will have truncated decrTrait above. Let x and x',y' denote decrClass and
+ // decrTrait, respectively, where x and x' have the same length. We then want to check (x,\top) <= (x',(y',\top)), which
+ // expands to:
+ // x <= x' && (x == x' ==> \top <= (y',\top))
+ // = { \top is strictly larger than a pair }
+ // x <= x' && (x == x' ==> false)
+ // =
+ // x < x'
+ // So we perform our desired check by calling DecreasesCheck to strictly compare x and x', so we pass in "allowNoChange"
+ // as "false".
+ bool allowNoChange = N == decrCountT && decrCountT <= decrCountC;
+ var decrChk = DecreasesCheck(toks, types0, types1, callee, caller, null, null, allowNoChange, false);
+ builder.Add(Assert(m.tok, decrChk, "method's decreases clause must be below or equal to that in the trait"));
}
private void AddMethodOverrideSubsetChk(Method m, Bpl.StmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables, Dictionary<IVariable, Expression> substMap)
@@ -11683,6 +11667,8 @@ namespace Microsoft.Dafny { Is, IsBox,
IsAlloc, IsAllocBox,
+ TraitParent,
+
SetCard,
SetEmpty,
SetUnionOne,
@@ -11860,6 +11846,11 @@ namespace Microsoft.Dafny { Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$IsAllocBox", Bpl.Type.Bool, args);
+ case BuiltinFunction.TraitParent:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "TraitParent", predef.ClassNameType, args);
+
case BuiltinFunction.SetCard:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
diff --git a/Test/dafny0/Trait/TraitBasix.dfy b/Test/dafny0/Trait/TraitBasix.dfy index e16e8fc4..eaf4ba4b 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy +++ b/Test/dafny0/Trait/TraitBasix.dfy @@ -3,95 +3,95 @@ module m1
{
- trait I1
- {
- function M1(x:int,y:int) :int
- {
- x*y
- }
- }
-
-
- trait I2 //all is fine in this trait
- {
- var x: int;
-
- function method Twice(): int
- reads this;
- {
- x + x
- }
-
- function method F(z: int): int
- reads this;
-
-
- method Compute(s: bool) returns (t: int, u: int)
- modifies this;
- {
- if s {
- t, u := F(F(15)), Twice();
- } else {
- t := Twice();
- x := F(45);
- u := Twice();
- var p := Customizable(u);
- return t+p, u;
- }
- }
-
- method Customizable(w: int) returns (p: int)
- modifies this;
-
-
- static method StaticM(a: int) returns (b: int)
- {
- b := a;
- }
-
- static method SS(a: int) returns (b:int)
- {
- b:=a*2;
- }
- }
-
- method I2Client(j: I2) returns (p: int) //all is fine in this client method
- requires j != null;
- modifies j;
- {
- j.x := 100;
- var h := j.Twice() + j.F(j.Twice());
- var a, b := j.Compute(h < 33);
- var c, d := j.Compute(33 <= h);
- p := j.Customizable(a + b + c + d);
- p := I2.StaticM(p);
- }
-
- class I0Child extends I2 //errors, body-less methods/functions in the parent have not implemented here
- {
- function method F(z: int): int
- reads this;
- {
- z
- }
- var x: int; //error, x has been declared in the parent trait
- }
-
- class I0Child2 extends I2
- {
- method Customizable(w: int) returns (p: int)
- modifies this;
- {
- w:=w+1;
- }
-
- var c1: I0Child;
- }
-
- class IXChild extends IX //error, IX trait is undefined
- {
-
- }
+ trait I1
+ {
+ function M1(x:int,y:int) :int
+ {
+ x*y
+ }
+ }
+
+
+ trait I2 //all is fine in this trait
+ {
+ var x: int;
+
+ function method Twice(): int
+ reads this;
+ {
+ x + x
+ }
+
+ function method F(z: int): int
+ reads this;
+
+
+ method Compute(s: bool) returns (t: int, u: int)
+ modifies this;
+ {
+ if s {
+ t, u := F(F(15)), Twice();
+ } else {
+ t := Twice();
+ x := F(45);
+ u := Twice();
+ var p := Customizable(u);
+ return t+p, u;
+ }
+ }
+
+ method Customizable(w: int) returns (p: int)
+ modifies this;
+
+
+ static method StaticM(a: int) returns (b: int)
+ {
+ b := a;
+ }
+
+ static method SS(a: int) returns (b:int)
+ {
+ b:=a*2;
+ }
+ }
+
+ method I2Client(j: I2) returns (p: int) //all is fine in this client method
+ requires j != null;
+ modifies j;
+ {
+ j.x := 100;
+ var h := j.Twice() + j.F(j.Twice());
+ var a, b := j.Compute(h < 33);
+ var c, d := j.Compute(33 <= h);
+ p := j.Customizable(a + b + c + d);
+ p := I2.StaticM(p);
+ }
+
+ class I0Child extends I2 //errors, body-less methods/functions in the parent have not implemented here
+ {
+ function method F(z: int): int
+ reads this;
+ {
+ z
+ }
+ var x: int; //error, x has been declared in the parent trait
+ }
+
+ class I0Child2 extends I2
+ {
+ method Customizable(w: int) returns (p: int)
+ modifies this;
+ {
+ w:=w+1;
+ }
+
+ var c1: I0Child;
+ }
+
+ class IXChild extends IX //error, IX trait is undefined
+ {
+
+ }
}
@@ -100,7 +100,7 @@ trait I0 var x: int;
constructor I0(x0: int) // error: constructor is not allowed in a trait
{
- x:=x0;
+ x:=x0;
}
}
@@ -108,66 +108,66 @@ trait I1 {
function M1(x:int,y:int) :int
{
- x*y
+ x*y
}
}
method TestI1()
{
- var i1 := new I1; //error: new is not allowed in a trait
+ var i1 := new I1; //error: new is not allowed in a trait
}
-trait I2 //all is fine in this trait
+trait I2 //all is fine in this trait
{
- var x: int;
-
- function method Twice(): int
- reads this;
- {
- x + x
- }
-
- function method F(z: int): int
- reads this;
-
-
- method Compute(s: bool) returns (t: int, u: int)
- modifies this;
- {
- if s {
- t, u := F(F(15)), Twice();
- } else {
- t := Twice();
- x := F(45);
- u := Twice();
- var p := Customizable(u);
- return t+p, u;
- }
- }
-
- method Customizable(w: int) returns (p: int)
- modifies this;
-
-
- static method StaticM(a: int) returns (b: int)
- {
- b := a;
- }
-
- static method SS(a: int) returns (b:int)
- {
- b:=a*2;
- }
+ var x: int;
+
+ function method Twice(): int
+ reads this;
+ {
+ x + x
+ }
+
+ function method F(z: int): int
+ reads this;
+
+
+ method Compute(s: bool) returns (t: int, u: int)
+ modifies this;
+ {
+ if s {
+ t, u := F(F(15)), Twice();
+ } else {
+ t := Twice();
+ x := F(45);
+ u := Twice();
+ var p := Customizable(u);
+ return t+p, u;
+ }
+ }
+
+ method Customizable(w: int) returns (p: int)
+ modifies this;
+
+
+ static method StaticM(a: int) returns (b: int)
+ {
+ b := a;
+ }
+
+ static method SS(a: int) returns (b:int)
+ {
+ b:=a*2;
+ }
}
method I2Client(j: I2) returns (p: int) //all is fine in this client method
- requires j != null;
- modifies j;
+ requires j != null;
+ modifies j;
{
- j.x := 100;
- var h := j.Twice() + j.F(j.Twice());
- var a, b := j.Compute(h < 33);
- var c, d := j.Compute(33 <= h);
- p := j.Customizable(a + b + c + d);
- p := I2.StaticM(p);
+ j.x := 100;
+ var h := j.Twice() + j.F(j.Twice());
+ var a, b := j.Compute(h < 33);
+ var c, d := j.Compute(33 <= h);
+ p := j.Customizable(a + b + c + d);
+ p := I2.StaticM(p);
}
diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect index 4a908ee7..84465fea 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,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(117,10): Error: new cannot be applied to a trait
+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 new file mode 100644 index 00000000..cc667a9a --- /dev/null +++ b/Test/dafny0/Trait/TraitCompile.dfy @@ -0,0 +1,71 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait TT
+{
+ function method Plus(x:int, y:int) : int
+ requires x > y
+ {
+ x + y
+ }
+ function method Times(x:int, y:int) : int
+ requires x > y
+ static function method StaticMinus(x:int, y:int) : int
+ requires x > y
+ {
+ x - y
+ }
+
+ method Double(x: int)
+ {
+ print "d=", x+x, "\n";
+ }
+ method AddFive(x: int)
+ static method StaticTriple(x: int)
+ {
+ print "t=", 3*x, "\n";
+ }
+}
+
+class CC extends TT
+{
+ function method Times(x:int, y:int) : int
+ requires x>y
+ {
+ x * y
+ }
+ method AddFive(x: int)
+ {
+ print "a5=", x+5, "\n";
+ }
+}
+
+method Client(t: TT)
+ requires t != null
+{
+ var x := t.Plus(10, 2);
+ print "x=", x, "\n";
+ t.Double(400);
+ t.AddFive(402);
+ t.StaticTriple(404);
+}
+
+method Main()
+{
+ var c := new CC;
+ var y := c.Plus(100, 20);
+ print "y=", y, "\n";
+ 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";
+
+ c.Double(500);
+ c.AddFive(502);
+ c.StaticTriple(504);
+ TT.StaticTriple(504);
+ CC.StaticTriple(505);
+}
diff --git a/Test/dafny0/Trait/TraitCompile.dfy.expect b/Test/dafny0/Trait/TraitCompile.dfy.expect new file mode 100644 index 00000000..f4f346de --- /dev/null +++ b/Test/dafny0/Trait/TraitCompile.dfy.expect @@ -0,0 +1,18 @@ +
+Dafny program verifier finished with 23 verified, 0 errors
+Program compiled successfully
+Running...
+
+y=120 +x=12 +d=800 +a5=407 +t=1212 +z=30 +z'=30 +w=30 +d=1000 +a5=507 +t=1512 +t=1512 +t=1515 diff --git a/Test/dafny0/Trait/TraitExtend.dfy b/Test/dafny0/Trait/TraitExtend.dfy index 1a59439c..f0e9dd33 100644 --- a/Test/dafny0/Trait/TraitExtend.dfy +++ b/Test/dafny0/Trait/TraitExtend.dfy @@ -3,41 +3,41 @@ trait t
{
- var f: int;
+ var f: int;
- function method Plus (x:int, y:int) : int
- requires x>y;
- {
- x + y
- }
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
- function method Mul (x:int, y:int, z:int) : int
- requires x>y;
- {
- x * y * z
- }
+ function method Mul (x:int, y:int, z:int) : int
+ requires x>y;
+ {
+ x * y * z
+ }
- //function method BodyLess1() : int
+ //function method BodyLess1() : int
- static method GetPhoneNumber (code:int, n:int) returns (z:int)
- {
- z := code + n;
- }
+ static method GetPhoneNumber (code:int, n:int) returns (z:int)
+ {
+ z := code + n;
+ }
- method TestPhone ()
- {
- var num : int;
- num := GetPhoneNumber (10, 30028);
- }
+ method TestPhone ()
+ {
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
+ }
}
class c1 extends t
{
- method P2(x:int, y:int) returns (z:int)
- requires x>y;
- {
- z:= Plus(x,y) + Mul (x,y,1);
- var j:int := Mul (x,y); //error, too few parameters in calling inherited method
- var k:int := Plus(x,y,1); //error, too many parameters in calling inherited method
- }
+ method P2(x:int, y:int) returns (z:int)
+ requires x>y;
+ {
+ z:= Plus(x,y) + Mul (x,y,1);
+ var j:int := Mul (x,y); //error, too few parameters in calling inherited method
+ var k:int := Plus(x,y,1); //error, too many parameters in calling inherited method
+ }
}
\ No newline at end of file diff --git a/Test/dafny0/Trait/TraitExtend.dfy.expect b/Test/dafny0/Trait/TraitExtend.dfy.expect index 2051fd81..69f4befa 100644 --- a/Test/dafny0/Trait/TraitExtend.dfy.expect +++ b/Test/dafny0/Trait/TraitExtend.dfy.expect @@ -1,3 +1,3 @@ -TraitExtend.dfy(40,24): Error: wrong number of arguments to function application (function 'Mul' expects 3, got 2)
-TraitExtend.dfy(41,24): Error: wrong number of arguments to function application (function 'Plus' expects 2, got 3)
+TraitExtend.dfy(40,21): Error: wrong number of arguments to function application (function 'Mul' expects 3, got 2)
+TraitExtend.dfy(41,21): Error: wrong number of arguments to function application (function 'Plus' expects 2, got 3)
2 resolution/type errors detected in TraitExtend.dfy
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy b/Test/dafny0/Trait/TraitMultiModule.dfy index f60db7b4..81f4f401 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy +++ b/Test/dafny0/Trait/TraitMultiModule.dfy @@ -5,22 +5,29 @@ module M1 {
trait T1
{
- method M1 (a:int)
+ method M1 (a:int)
}
class C1 extends T1
{
- method M1 (x:int)
- {
- var y: int := x;
- }
+ method M1 (x:int)
+ {
+ var y: int := x;
+ }
}
}
module M2
{
- class C2 extends T1
- {
-
- }
+ import opened M1
+ class C2 extends T1 // error: currently no support to implement trait in different module
+ {
+ }
+}
-}
\ No newline at end of file +module M3
+{
+ import M1
+ class C2 extends M1.T1 // error: currently no support to implement trait in different module
+ {
+ }
+}
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect index b9031dac..e991553a 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -1,2 +1,3 @@ -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
+TraitMultiModule.dfy(22,19): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.
+TraitMultiModule.dfy(30,22): Error: class 'C2' is in a different module than trait 'M1.T1'. A class may only extend a trait in the same module.
+2 resolution/type errors detected in TraitMultiModule.dfy
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy b/Test/dafny0/Trait/TraitOverride0.dfy index a8fb8596..63ca94ce 100644 --- a/Test/dafny0/Trait/TraitOverride0.dfy +++ b/Test/dafny0/Trait/TraitOverride0.dfy @@ -14,7 +14,7 @@ trait T1 function method Mul (x:int, y:int, z:int) : int
requires x>y;
{
- x * y * z
+ x * y * z
}
function method BodyLess1() : int
@@ -23,13 +23,13 @@ trait T1 static method GetPhoneNumber (code:int, n:int) returns (z:int)
{
- z := code + n;
+ z := code + n;
}
method TestPhone ()
{
- var num : int;
- num := GetPhoneNumber (10, 30028);
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
}
}
@@ -47,24 +47,24 @@ class C1 extends T1 function method BodyLess1(i:int) : int //error, overriding function has too many parameters
{
- 12
+ 12
}
function method Mul (x:int, y:int, z:int) : int //error, can not override implemented methods
requires x>y;
{
- x * y * z
+ x * y * z
}
function method BodyLess2(a:int, b:int) : int
{
- a+b
+ a+b
}
}
class C2 extends T1
{
- //error, there are body-less methods in the parent trait that must be implemented
+ //error, there are body-less methods in the parent trait that must be implemented
}
abstract module AM1
@@ -78,4 +78,4 @@ abstract module AM1 {
method Calc(ii:int, jj:int) returns (kk:int)
}
-}
\ No newline at end of file +}
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy b/Test/dafny0/Trait/TraitOverride1.dfy index c963f847..d0d16401 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy +++ b/Test/dafny0/Trait/TraitOverride1.dfy @@ -4,178 +4,178 @@ //everything should work OK in this test file
trait T1
{
- function method Plus (x:int, y:int) : int
- requires x>y;
- {
- x + y
- }
+ function method Plus (x:int, y:int) : int
+ requires x>y;
+ {
+ x + y
+ }
+
+ function method bb(x:int):int
+ requires x>10;
+
+ function method BodyLess1(a:int) : int
+ requires a > 0;
- function method bb(x:int):int
- requires x>10;
+ function method dd(a:int) : int
- function method BodyLess1(a:int) : int
- requires a > 0;
-
- function method dd(a:int) : int
-
- method Testing()
+ method Testing()
}
class C1 extends T1
{
- function method dd(x:int):int
- {
- 2
- }
-
- method Testing()
- {
- var x:int := 11;
- x := bb(x);
- }
-
- function method bb(x:int):int
- requires x >10;
- {
- x
- }
- function method BodyLess1(bda:int) : int
+ function method dd(x:int):int
+ {
+ 2
+ }
+
+ method Testing()
+ {
+ var x:int := 11;
+ x := bb(x);
+ }
+
+ function method bb(x:int):int
+ requires x >10;
+ {
+ x
+ }
+ function method BodyLess1(bda:int) : int
requires bda > (-10);
- {
- 2
- }
-
- method CallBodyLess(x:int)
- requires x > (-10);
- {
- var k:int := BodyLess1(x);
- assert (k==2);
- }
+ {
+ 2
+ }
+
+ method CallBodyLess(x:int)
+ requires x > (-10);
+ {
+ var k:int := BodyLess1(x);
+ assert (k==2);
+ }
}
trait T2
{
- function method F(x: int): int
- requires x < 100;
- ensures F(x) < 100;
-
- method M(x: int) returns (y: int)
- requires 0 <= x;
- ensures x < y;
+ function method F(x: int): int
+ requires x < 100;
+ ensures F(x) < 100;
+
+ method M(x: int) returns (y: int)
+ requires 0 <= x;
+ ensures x < y;
}
class C2 extends T2
{
- function method F(x: int): int
- requires x < 100;
- ensures F(x) < 100;
- {
- x
- }
-
- method M(x: int) returns (y: int)
- requires -2000 <= x; // a more permissive precondition than in the interface
- ensures 2*x < y; // a more detailed postcondition than in the interface
- {
- y := (2 * x) + 1;
- }
+ function method F(x: int): int
+ requires x < 100;
+ ensures F(x) < 100;
+ {
+ x
+ }
+
+ method M(x: int) returns (y: int)
+ requires -2000 <= x; // a more permissive precondition than in the interface
+ ensures 2*x < y; // a more detailed postcondition than in the interface
+ {
+ y := (2 * x) + 1;
+ }
}
trait T3
{
- function method F(y: int): int
- function method G(y: int): int { 12 }
- method M(y: int)
- method N(y: int) {
- var a:int := 100;
- assert a==100;
- }
+ function method F(y: int): int
+ function method G(y: int): int { 12 }
+ method M(y: int)
+ method N(y: int) {
+ var a:int := 100;
+ assert a==100;
+ }
}
class C3 extends T3
{
- function method NewFunc (a:int, b:int) : int
- {
- a + b
- }
- function method F(y: int): int { 20 }
- method M(y: int) {
- var a:int := 100;
- assert a==100;
- }
+ function method NewFunc (a:int, b:int) : int
+ {
+ a + b
+ }
+ function method F(y: int): int { 20 }
+ method M(y: int) {
+ var a:int := 100;
+ assert a==100;
+ }
}
trait t
{
function f(s2:int):int
- ensures f(s2) > 0;
- //requires s != null && s.Length > 1;
- //reads s, s2;
+ ensures f(s2) > 0;
+ //requires s != null && s.Length > 1;
+ //reads s, s2;
}
class c extends t
{
function f(s3:int):int
- ensures f(s3) > 1;
- //requires s0 != null && s0.Length > (0);
- //reads s0;
+ ensures f(s3) > 1;
+ //requires s0 != null && s0.Length > (0);
+ //reads s0;
{
- 2
+ 2
}
}
trait TT
{
- static function method M(a:int, b:int) : int
- ensures M(a,b) == a + b;
- {
- a + b
- }
+ static function method M(a:int, b:int) : int
+ ensures M(a,b) == a + b;
+ {
+ a + b
+ }
}
class CC extends TT
{
- method Testing(a:int,b:int)
- {
- assert (TT.M(a,b) == a + b);
- }
+ method Testing(a:int,b:int)
+ {
+ assert (TT.M(a,b) == a + b);
+ }
}
trait T4
{
- function method F(y: int): int
-
- function method G(y: int): int
- {
- 100
- }
-
- method M(y: int) returns (kobra:int)
- requires y > 0;
- ensures kobra > 0;
-
- method N(y: int)
- {
- var x: int;
- var y : int;
- y := 10;
- x := 1000;
- y := y + x;
- }
+ function method F(y: int): int
+
+ function method G(y: int): int
+ {
+ 100
+ }
+
+ method M(y: int) returns (kobra:int)
+ requires y > 0;
+ ensures kobra > 0;
+
+ method N(y: int)
+ {
+ var x: int;
+ var y : int;
+ y := 10;
+ x := 1000;
+ y := y + x;
+ }
}
class C4 extends T4
{
- function method F(y: int): int
- {
- 200
- }
+ function method F(y: int): int
+ {
+ 200
+ }
- method M(kk:int) returns (ksos:int)
- requires kk > (-1);
- ensures ksos > 0;
- {
- ksos:=10;
- }
+ method M(kk:int) returns (ksos:int)
+ requires kk > (-1);
+ ensures ksos > 0;
+ {
+ ksos:=10;
+ }
}
diff --git a/Test/dafny0/Trait/TraitPolymorphism.dfy b/Test/dafny0/Trait/TraitPolymorphism.dfy index b1ee9eea..f53d8346 100644 --- a/Test/dafny0/Trait/TraitPolymorphism.dfy +++ b/Test/dafny0/Trait/TraitPolymorphism.dfy @@ -14,20 +14,20 @@ trait T1 function method Mul (x:int, y:int, z:int) : int
requires x>y;
{
- x * y * z
+ x * y * z
}
//function method BodyLess1() : int
static method GetPhoneNumber (code:int, n:int) returns (z:int)
{
- z := code + n;
+ z := code + n;
}
method TestPhone ()
{
- var num : int;
- num := GetPhoneNumber (10, 30028);
+ var num : int;
+ num := GetPhoneNumber (10, 30028);
}
}
diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy b/Test/dafny0/Trait/TraitSpecsOverride0.dfy index 614adc2d..b4bbd9d8 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy @@ -4,56 +4,71 @@ trait J
{
- function method F(k:int, y: array<int>): int
- reads y;
- decreases k;
-
- function method G(y: int): int
- {
- 100
- }
-
- method M(y: int) returns (kobra:int)
- requires y > 0;
- ensures kobra > 0;
-
- method N(y: int)
- {
- var x: int;
- var y : int;
- y := 10;
- x := 1000;
- y := y + x;
- }
-
- method arrM (y: array<int>, x: int, a: int, b: int) returns (c: int)
- requires a > b;
- requires y != null && y.Length > 0;
- ensures c == a + b;
- modifies y;
- decreases x;
+ function method F(k:int, y: array<int>): int
+ reads y;
+ decreases k;
+ ensures F(k, y) < 100
+
+ function method G(y: int): int
+ {
+ 100
+ }
+
+ method M(y: int) returns (kobra:int)
+ requires y > 0;
+ ensures kobra > 0;
+
+ method N(y: int)
+ {
+ var x: int;
+ var y : int;
+ y := 10;
+ x := 1000;
+ y := y + x;
+ }
+
+ method arrM (y: array<int>, x: int, a: int, b: int) returns (c: int)
+ requires a > b;
+ requires y != null && y.Length > 0;
+ ensures c == a + b;
+ modifies y;
+ decreases x;
}
class C extends J
{
- function method F(kk:int, yy: array<int>): int
- {
- 200
- }
+ // F's postcondition (true) is too weak, but that won't be detected until verification time
+ function method F(kk:int, yy: array<int>): int
+ {
+ 200
+ }
- method M(kk:int) returns (ksos:int) //errors here, M must provide its own specifications
- {
- ksos:=10;
- }
+ // M's postcondition (true) is too weak, but that won't be detected until verification time
+ method M(kk:int) returns (ksos:int)
+ {
+ ksos:=10;
+ }
- method arrM (y1: array<int>, x1: int, a1: int, b1: int) returns (c1: int)
- requires a1 > b1;
- requires y1 != null && y1.Length > 0;
- ensures c1 == a1 + b1;
- modifies y1;
- decreases x1;
- {
- y1[0] := a1 + b1;
- c1 := a1 + b1;
- }
-}
\ No newline at end of file + method arrM (y1: array<int>, x1: int, a1: int, b1: int) returns (c1: int)
+ requires a1 > b1;
+ requires y1 != null && y1.Length > 0;
+ ensures c1 == a1 + b1;
+ modifies y1;
+ decreases x1;
+ {
+ y1[0] := a1 + b1;
+ c1 := a1 + b1;
+ }
+}
+
+module BadNonTermination {
+ trait TT1 {
+ method N(x: int)
+ decreases x
+ }
+ class CC1 extends TT1 {
+ method N(x: int)
+ decreases * // error: can't override a terminating method with a possibly non-terminating method
+ { }
+ }
+}
diff --git a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect index 750e13e0..2281c604 100644 --- a/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect +++ b/Test/dafny0/Trait/TraitSpecsOverride0.dfy.expect @@ -1,5 +1,2 @@ -TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Reads clauses anew
-TraitSpecsOverride0.dfy(39,17): Error: Function must provide its own Decreases clauses anew
-TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Requires clauses anew
-TraitSpecsOverride0.dfy(44,8): Error: Method must provide its own Ensures clauses anew
-4 resolution/type errors detected in TraitSpecsOverride0.dfy
+TraitSpecsOverride0.dfy(70,11): Error: not allowed to override a terminating method with a possibly non-terminating method ('N')
+1 resolution/type errors detected in TraitSpecsOverride0.dfy
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy b/Test/dafny0/Trait/TraitUsingParentMembers.dfy index dd45d0e6..fb6480a4 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy @@ -4,41 +4,41 @@ trait P1
{
- method N0() {
- var a: array<int>;
- if (a != null && 5 < a.Length) {
- a[5] := 12; // error: violates modifies clause
- }
- }
+ method N0() {
+ var a: array<int>;
+ if (a != null && 5 < a.Length) {
+ a[5] := 12; // error: violates modifies clause
+ }
+ }
- method Mul(x: int, y: int) returns (r: int)
- requires 0 <= x && 0 <= y;
- ensures r == x*y;
- decreases x;
+ method Mul(x: int, y: int) returns (r: int)
+ requires 0 <= x && 0 <= y;
+ ensures r == x*y;
+ decreases x;
}
class C1 extends P1
{
- method Mul(x: int, y: int) returns (r: int)
- requires 0 <= x && 0 <= y;
- ensures r == x*y;
- decreases x;
- {
- if (x == 0) {
- r := 0;
- } else {
- var m := Mul(x-1, y);
- r := m + y;
- }
- }
+ method Mul(x: int, y: int) returns (r: int)
+ requires 0 <= x && 0 <= y;
+ ensures r == x*y;
+ decreases x;
+ {
+ if (x == 0) {
+ r := 0;
+ } else {
+ var m := Mul(x-1, y);
+ r := m + y;
+ }
+ }
- method Testing(arr:array<int>)
- requires arr != null && arr.Length == 2 && arr[0]== 1 && arr[1] == 10;
- {
- N0(); //calling parent trait methods
- var x := 2;
- var y := 5;
- var z := Mul(x,y);
- assert (z == 10);
- }
-}
\ No newline at end of file + method Testing(arr:array<int>)
+ requires arr != null && arr.Length == 2 && arr[0]== 1 && arr[1] == 10;
+ {
+ N0(); //calling parent trait methods
+ var x := 2;
+ var y := 5;
+ var z := Mul(x,y);
+ assert (z == 10);
+ }
+}
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect index 6849499c..ebda3b9f 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect @@ -1,4 +1,4 @@ -TraitUsingParentMembers.dfy(10,9): Error: assignment may update an array element not in the enclosing context's modifies clause
+TraitUsingParentMembers.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy b/Test/dafny0/Trait/TraitsDecreases.dfy new file mode 100644 index 00000000..53ce28be --- /dev/null +++ b/Test/dafny0/Trait/TraitsDecreases.dfy @@ -0,0 +1,108 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait Trait {
+ // -----------------------
+ method A0(x: nat)
+ // default decreases: x
+ method A1(x: nat)
+ // default decreases: x
+ method A2(x: nat)
+ decreases x
+ method A3(x: nat)
+ decreases x
+ // -----------------------
+ method G0(x: nat, y: bool)
+ decreases x, y
+ method G1(x: nat, y: bool)
+ decreases x+1, y
+ method G2(x: nat, y: bool)
+ decreases x
+ method G3(x: nat, y: bool)
+ decreases x+1, y
+ method G4(x: nat, y: bool)
+ decreases y, x
+ method G5(x: nat, y: bool)
+ decreases y, x
+ method G6(x: nat, y: bool)
+ decreases true, x
+ method G7(x: nat, y: bool)
+ decreases false, x
+ method G8(x: nat, y: bool)
+ requires x < 100
+ decreases 120, y
+ method G9(x: nat, y: bool)
+ requires x < 100
+ decreases 120, y
+ method G10(x: nat, y: bool)
+ requires x < 100
+ decreases x, y
+}
+
+class Class extends Trait {
+ // -----------------------
+ method A0(x: nat)
+ // default decreases: x
+ { }
+ method A1(x: nat)
+ decreases x
+ { }
+ method A2(x: nat)
+ // default decreases: x
+ { }
+ method A3(x: nat)
+ decreases x
+ { }
+ // -----------------------
+ method G0(x: nat, y: bool)
+ decreases y, x // error: opposite order from default
+ { }
+ method G1(x: nat, y: bool)
+ decreases x, x // fine -- it's below the one in the trait
+ { }
+ method G2(x: nat, y: bool) // fine -- (x,y) is below the trait's (x,\top)
+ // default decreases: x, y
+ { }
+ method G3(x: nat, y: bool)
+ decreases x, y // fine -- trait decrease is above this one
+ { }
+ method G4(x: nat, y: bool)
+ decreases y, x+1 // error: this decreases is above the trait's decreases
+ { }
+ method G5(x: nat, y: bool)
+ decreases y // error: this is above the trait's decreases clause
+ { }
+ method G6(x: nat, y: bool)
+ decreases y, x // good -- this is the same or below the one in the trait
+ { }
+ method G7(x: nat, y: bool)
+ decreases y, x // error: this might be above the one in the trait
+ { }
+ method G8(x: nat, y: bool)
+ decreases x, y // fine -- given the precondition in the trait, this is below the one in the trait
+ { }
+ method G9(x: nat, y: bool)
+ requires x < 105
+ decreases 120, y // fine -- given the precondition in the trait, this is below the one in the trait
+ { }
+ method G10(x: nat, y: bool)
+ requires x < 100
+ decreases 120, y // error: this is above the one in the trait
+ { }
+}
+
+
+trait TT {
+ method M(x: int)
+ decreases *
+ method P(x: int)
+ decreases *
+}
+class CC extends TT {
+ method M(x: int)
+ decreases x
+ { }
+ method P(x: int)
+ decreases *
+ { }
+}
diff --git a/Test/dafny0/Trait/TraitsDecreases.dfy.expect b/Test/dafny0/Trait/TraitsDecreases.dfy.expect new file mode 100644 index 00000000..6c76f9a8 --- /dev/null +++ b/Test/dafny0/Trait/TraitsDecreases.dfy.expect @@ -0,0 +1,17 @@ +TraitsDecreases.dfy(57,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(69,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(72,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(78,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+TraitsDecreases.dfy(88,10): Error: method's decreases clause must be below or equal to that in the trait
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 63 verified, 5 errors
diff --git a/Test/dafny0/Trait/TraitsMultipleInheritance.dfy b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy index 67acbc67..640d0d8d 100644 --- a/Test/dafny0/Trait/TraitsMultipleInheritance.dfy +++ b/Test/dafny0/Trait/TraitsMultipleInheritance.dfy @@ -2,11 +2,11 @@ // RUN: %diff "%s.expect" "%t"
trait J1{
- var x: int;
+ var x: int;
}
trait J2{
- var y: int;
+ var y: int;
}
class C extends J1, J2{
|