From d47400c8a1ba72497cc145173aa6ad9f6b1b5a85 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 23 Feb 2014 17:27:26 -0800 Subject: Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma") --- Source/Dafny/Cloner.cs | 34 ++--- Source/Dafny/Dafny.atg | 18 +-- Source/Dafny/DafnyAst.cs | 48 +++---- Source/Dafny/Parser.cs | 22 +-- Source/Dafny/Printer.cs | 10 +- Source/Dafny/RefinementTransformer.cs | 4 +- Source/Dafny/Resolver.cs | 166 +++++++++++----------- Source/Dafny/Scanner.cs | 4 +- Source/Dafny/Translator.cs | 34 ++--- Source/DafnyExtension/OutliningTagger.cs | 6 +- Source/DafnyExtension/TokenTagger.cs | 2 +- Test/dafny0/Answer | 12 +- Test/dafny0/CoPrefix.dfy | 36 ++--- Test/dafny0/CoResolution.dfy | 24 ++-- Test/dafny0/Coinductive.dfy | 6 +- Test/dafny0/CoinductiveProofs.dfy | 30 ++-- Test/dafny3/Filter.dfy | 30 ++-- Test/dafny3/InductionVsCoinduction.dfy | 18 +-- Test/dafny3/InfiniteTrees.dfy | 62 ++++---- Test/dafny3/Paulson.dfy | 22 +-- Test/dafny3/SimpleCoinduction.dfy | 20 +-- Test/dafny3/Streams.dfy | 42 +++--- Test/dafny3/WideTrees.dfy | 4 +- Test/dafny3/Zip.dfy | 16 +-- Util/Emacs/dafny-mode.el | 2 +- Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 4 +- Util/latex/dafny.sty | 2 +- Util/vim/dafny.vim | 2 +- 28 files changed, 342 insertions(+), 338 deletions(-) diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 9aca7306..452c71e4 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -567,8 +567,8 @@ namespace Microsoft.Dafny if (m is Constructor) { return new Constructor(Tok(m.tok), m.Name, tps, ins, req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); - } else if (m is CoMethod) { - return new CoMethod(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), + } else if (m is CoLemma) { + return new CoLemma(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null); } else if (m is Lemma) { return new Lemma(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), @@ -584,8 +584,8 @@ namespace Microsoft.Dafny } /// - /// Subclass of Cloner that collects some common functionality between CoMethodPostconditionSubstituter and - /// CoMethodBodyCloner. + /// Subclass of Cloner that collects some common functionality between CoLemmaPostconditionSubstituter and + /// CoLemmaBodyCloner. /// abstract class CoCloner : Cloner { @@ -609,16 +609,16 @@ namespace Microsoft.Dafny } /// - /// The CoMethodPostconditionSubstituter clones the postcondition declared on a comethod, but replaces + /// The CoLemmaPostconditionSubstituter clones the postcondition declared on a colemma, but replaces /// the calls and equalities in "coConclusions" with corresponding prefix versions. The resulting - /// expression is then appropriate to be a postcondition of the comethod's corresponding prefix method. + /// expression is then appropriate to be a postcondition of the colemma's corresponding prefix lemma. /// It is assumed that the source expression has been resolved. Note, the "k" given to the constructor /// is not cloned with each use; it is simply used as is. /// - class CoMethodPostconditionSubstituter : CoCloner + class CoLemmaPostconditionSubstituter : CoCloner { readonly ISet coConclusions; - public CoMethodPostconditionSubstituter(ISet coConclusions, Expression k, Resolver resolver) + public CoLemmaPostconditionSubstituter(ISet coConclusions, Expression k, Resolver resolver) : base(k, resolver) { Contract.Requires(coConclusions != null); @@ -660,13 +660,13 @@ namespace Microsoft.Dafny } /// - /// The task of the CoMethodBodyCloner is to fill in the implicit _k-1 arguments in corecursive comethod calls. + /// The task of the CoLemmaBodyCloner is to fill in the implicit _k-1 arguments in corecursive colemma calls. /// The source statement and the given "k" are assumed to have been resolved, and the resulting statement will also be resolved. /// - class CoMethodBodyCloner : CoCloner + class CoLemmaBodyCloner : CoCloner { - readonly CoMethod context; - public CoMethodBodyCloner(CoMethod context, Expression k, Resolver resolver) + readonly CoLemma context; + public CoLemmaBodyCloner(CoLemma context, Expression k, Resolver resolver) : base(k, resolver) { Contract.Requires(context != null); @@ -681,8 +681,8 @@ namespace Microsoft.Dafny var call = (CallStmt)s.ResolvedStatements[0]; var moduleCaller = context.EnclosingClass.Module; var moduleCallee = call.Method.EnclosingClass.Module; - if (call.Method is CoMethod && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(call.Method)) { - // we're looking at a recursive call to a comethod + if (call.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(call.Method)) { + // we're looking at a recursive call to a colemma var args = new List(); args.Add(k); foreach (var arg in call.Args) { @@ -699,11 +699,11 @@ namespace Microsoft.Dafny } } else if (stmt is CallStmt) { var s = (CallStmt)stmt; - if (s.Method is CoMethod) { + if (s.Method is CoLemma) { var moduleCaller = context.EnclosingClass.Module; var moduleCallee = s.Method.EnclosingClass.Module; - if (s.Method is CoMethod && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { - // we're looking at a recursive call to a comethod + if (s.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { + // we're looking at a recursive call to a colemma var args = new List(); args.Add(k); foreach (var arg in s.Args) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 51a4785b..563c1d6c 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -559,7 +559,7 @@ MethodDecl BlockStmt body = null; bool isLemma = false; bool isConstructor = false; - bool isCoMethod = false; + bool isCoLemma = false; IToken signatureEllipsis = null; IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; @@ -567,8 +567,10 @@ MethodDecl SYNC ( "method" | "lemma" (. isLemma = true; .) - | "comethod" (. isCoMethod = true; .) - | "colemma" (. isCoMethod = true; .) + | "colemma" (. isCoLemma = true; .) + | "comethod" (. isCoLemma = true; + errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'"); + .) | "constructor" (. if (allowConstructor) { isConstructor = true; } else { @@ -587,9 +589,9 @@ MethodDecl if (mmod.IsStatic) { SemErr(t, "constructors cannot be declared 'static'"); } - } else if (isCoMethod) { + } else if (isCoLemma) { if (mmod.IsGhost) { - SemErr(t, "comethods cannot be declared 'ghost' (they are automatically 'ghost')"); + SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')"); } } .) @@ -636,9 +638,9 @@ MethodDecl if (isConstructor) { m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); - } else if (isCoMethod) { - m = new CoMethod(id, id.val, mmod.IsStatic, typeArgs, ins, outs, - req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + } else if (isCoLemma) { + m = new CoLemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs, + req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isLemma) { m = new Lemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index f29242ab..eee1b06f 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1124,8 +1124,8 @@ namespace Microsoft.Dafny { /// declarations. /// Note, an iterator declaration is a class, in this sense. /// Note, if the given list are the top-level declarations of a module, the yield will include - /// co-methods but not their associated prefix methods (which are tucked into the co-method's - /// .PrefixMethod field). + /// colemmas but not their associated prefix lemmas (which are tucked into the colemma's + /// .PrefixLemma field). /// public static IEnumerable AllCallables(List declarations) { foreach (var d in declarations) { @@ -1171,12 +1171,12 @@ namespace Microsoft.Dafny { } } - public static IEnumerable AllCoMethods(List declarations) { + public static IEnumerable AllCoLemmas(List declarations) { foreach (var d in declarations) { var cl = d as ClassDecl; if (cl != null) { foreach (var member in cl.Members) { - var m = member as CoMethod; + var m = member as CoLemma; if (m != null) { yield return m; } @@ -1950,7 +1950,7 @@ namespace Microsoft.Dafny { /// /// An ImplicitFormal is a parameter that is declared implicitly, in particular the "_k" depth parameter - /// of each comethod (for use in the comethod body only, not the specification). + /// of each colemma (for use in the comethod body only, not the specification). /// public class ImplicitFormal : Formal { @@ -2257,16 +2257,16 @@ namespace Microsoft.Dafny { } /// - /// An PrefixPredicate is the inductive unrolling P# implicitly declared for every copredicate P. + /// A PrefixLemma is the inductive unrolling M# implicitly declared for every colemma M. /// - public class PrefixMethod : Method + public class PrefixLemma : Method { public readonly Formal K; - public readonly CoMethod Co; - public PrefixMethod(IToken tok, string name, bool isStatic, - List typeArgs, Formal k, List ins, List outs, - List req, Specification mod, List ens, Specification decreases, - BlockStmt body, Attributes attributes, CoMethod co) + public readonly CoLemma Co; + public PrefixLemma(IToken tok, string name, bool isStatic, + List typeArgs, Formal k, List ins, List outs, + List req, Specification mod, List ens, Specification decreases, + BlockStmt body, Attributes attributes, CoLemma co) : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) { Contract.Requires(k != null); Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k); @@ -2276,19 +2276,19 @@ namespace Microsoft.Dafny { } } - public class CoMethod : Method + public class CoLemma : Method { - public PrefixMethod PrefixMethod; // filled in during resolution (name registration) - - public CoMethod(IToken tok, string name, - bool isStatic, - List typeArgs, - List ins, [Captured] List outs, - List req, [Captured] Specification mod, - List ens, - Specification decreases, - BlockStmt body, - Attributes attributes, IToken signatureEllipsis) + public PrefixLemma PrefixLemma; // filled in during resolution (name registration) + + public CoLemma(IToken tok, string name, + bool isStatic, + List typeArgs, + List ins, [Captured] List outs, + List req, [Captured] Specification mod, + List ens, + Specification decreases, + BlockStmt body, + Attributes attributes, IToken signatureEllipsis) : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(tok != null); Contract.Requires(name != null); diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index d064606f..a52d840c 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -860,7 +860,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { BlockStmt body = null; bool isLemma = false; bool isConstructor = false; - bool isCoMethod = false; + bool isCoLemma = false; IToken signatureEllipsis = null; IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; @@ -873,10 +873,12 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { isLemma = true; } else if (la.kind == 42) { Get(); - isCoMethod = true; + isCoLemma = true; } else if (la.kind == 43) { Get(); - isCoMethod = true; + isCoLemma = true; + errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'"); + } else if (la.kind == 44) { Get(); if (allowConstructor) { @@ -898,9 +900,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { if (mmod.IsStatic) { SemErr(t, "constructors cannot be declared 'static'"); } - } else if (isCoMethod) { + } else if (isCoLemma) { if (mmod.IsGhost) { - SemErr(t, "comethods cannot be declared 'ghost' (they are automatically 'ghost')"); + SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')"); } } @@ -959,9 +961,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) { if (isConstructor) { m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); - } else if (isCoMethod) { - m = new CoMethod(id, id.val, mmod.IsStatic, typeArgs, ins, outs, - req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); + } else if (isCoLemma) { + m = new CoLemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs, + req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); } else if (isLemma) { m = new Lemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis); @@ -3687,8 +3689,8 @@ public class Errors { case 39: s = "\">\" expected"; break; case 40: s = "\"method\" expected"; break; case 41: s = "\"lemma\" expected"; break; - case 42: s = "\"comethod\" expected"; break; - case 43: s = "\"colemma\" expected"; break; + case 42: s = "\"colemma\" expected"; break; + case 43: s = "\"comethod\" expected"; break; case 44: s = "\"constructor\" expected"; break; case 45: s = "\"modifies\" expected"; break; case 46: s = "\"free\" expected"; break; diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 601c5761..a5057286 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -267,10 +267,10 @@ namespace Microsoft.Dafny { if (m is Method) { if (state != 0) { wr.WriteLine(); } PrintMethod((Method)m, indent, false); - var com = m as CoMethod; - if (com != null && com.PrefixMethod != null) { + var com = m as CoLemma; + if (com != null && com.PrefixLemma != null) { Indent(indent); wr.WriteLine("/***"); - PrintMethod(com.PrefixMethod, indent, false); + PrintMethod(com.PrefixLemma, indent, false); Indent(indent); wr.WriteLine("***/"); } state = 2; @@ -441,9 +441,9 @@ namespace Microsoft.Dafny { Contract.Requires(method != null); Indent(indent); - string k = method is Constructor ? "constructor" : method is CoMethod ? "comethod" : method is Lemma ? "lemma" : "method"; + string k = method is Constructor ? "constructor" : method is CoLemma ? "colemma" : method is Lemma ? "lemma" : "method"; if (method.IsStatic) { k = "static " + k; } - if (method.IsGhost && !(method is Lemma) && !(method is CoMethod)) { k = "ghost " + k; } + if (method.IsGhost && !(method is Lemma) && !(method is CoLemma)) { k = "ghost " + k; } string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name; PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs); if (method.SignatureIsOmitted) { diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index acee1845..75dbaad3 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -564,8 +564,8 @@ namespace Microsoft.Dafny if (m is Constructor) { return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins, req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); - } else if (m is CoMethod) { - return new CoMethod(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), + } else if (m is CoLemma) { + return new CoLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); } else if (m is Lemma) { return new Lemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal), diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 564e4164..2262c4da 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -354,22 +354,22 @@ namespace Microsoft.Dafny foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls)) { ICallable m; string s; - if (clbl is CoMethod) { - var prefixMethod = ((CoMethod)clbl).PrefixMethod; - m = prefixMethod; - s = prefixMethod.Name + " "; + if (clbl is CoLemma) { + var prefixLemma = ((CoLemma)clbl).PrefixLemma; + m = prefixLemma; + s = prefixLemma.Name + " "; } else { m = clbl; s = ""; } FillInDefaultDecreases(m); - if (m.InferredDecreases || m is PrefixMethod) { + if (m.InferredDecreases || m is PrefixLemma) { bool showIt = false; if (m is Function) { // show the inferred decreases clause only if it will ever matter, i.e., if the function is recursive showIt = ((Function)m).IsRecursive; - } else if (m is PrefixMethod) { + } else if (m is PrefixLemma) { // always show the decrease clause, since at the very least it will start with "_k", which the programmer did not write explicitly showIt = true; } else { @@ -386,7 +386,7 @@ namespace Microsoft.Dafny } s += ";"; // always terminate with a semi-colon, even in the case of an empty decreases clause // Note, in the following line, we use the location information for "clbl", not "m". These - // are the same, except in the case where "clbl" is a CoMethod and "m" is a prefix method. + // are the same, except in the case where "clbl" is a CoLemma and "m" is a prefix lemma. ReportAdditionalInformation(clbl.Tok, s, clbl.Tok.val.Length); } } @@ -402,7 +402,7 @@ namespace Microsoft.Dafny return; } var decr = clbl.Decreases.Expressions; - if (decr.Count == 0 || (clbl is PrefixMethod && decr.Count == 1)) { + if (decr.Count == 0 || (clbl is PrefixLemma && decr.Count == 1)) { // The default for a function starts with the function's reads clause, if any if (clbl is Function) { var fn = (Function)clbl; @@ -853,7 +853,7 @@ namespace Microsoft.Dafny foreach (MemberDecl m in cl.Members) { if (!members.ContainsKey(m.Name)) { members.Add(m.Name, m); - if (m is CoPredicate || m is CoMethod) { + if (m is CoPredicate || m is CoLemma) { var extraName = m.Name + "#"; MemberDecl extraMember; var cloner = new Cloner(); @@ -873,24 +873,24 @@ namespace Microsoft.Dafny // In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles. moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop); } else { - var com = (CoMethod)m; + var com = (CoLemma)m; // _k has already been added to 'formals', so append the original formals formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal)); // prepend _k to the given decreases clause var decr = new List(); decr.Add(new IdentifierExpr(com.tok, k.Name)); decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr)); - // Create prefix method. Note that the body is not cloned, but simply shared. - com.PrefixMethod = new PrefixMethod(com.tok, extraName, com.IsStatic, + // Create prefix lemma. Note that the body is not cloned, but simply shared. + com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.IsStatic, com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal), com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod), - new List(), // Note, the postconditions are filled in after the comethod's postconditions have been resolved + new List(), // Note, the postconditions are filled in after the colemma's postconditions have been resolved new Specification(decr, null), - null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the comethod is known + null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the colemma is known cloner.CloneAttributes(com.Attributes), com); - extraMember = com.PrefixMethod; + extraMember = com.PrefixLemma; // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles. - moduleDef.CallGraph.AddEdge(com.PrefixMethod, com); + moduleDef.CallGraph.AddEdge(com.PrefixLemma, com); } members.Add(extraName, extraMember); } @@ -1119,8 +1119,8 @@ namespace Microsoft.Dafny if (m is Constructor) { return new Constructor(m.tok, m.Name, tps, ins, req, mod, ens, decreases, null, null, null); - } else if (m is CoMethod) { - return new CoMethod(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), + } else if (m is CoLemma) { + return new CoLemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, null, null, null); } else if (m is Lemma) { return new Lemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), @@ -1414,40 +1414,40 @@ namespace Microsoft.Dafny } if (ErrorCount == prevErrorCount) { - // fill in the postconditions and bodies of prefix methods - foreach (var com in ModuleDefinition.AllCoMethods(declarations)) { - var prefixMethod = com.PrefixMethod; - if (prefixMethod == null) { - continue; // something went wrong during registration of the prefix method (probably a duplicated comethod name) - } - Contract.Assume(prefixMethod.Ens.Count == 0 && prefixMethod.Body == null); // there are not supposed have have been filled in before - // compute the postconditions of the prefix method - var k = prefixMethod.Ins[0]; + // fill in the postconditions and bodies of prefix lemmas + foreach (var com in ModuleDefinition.AllCoLemmas(declarations)) { + var prefixLemma = com.PrefixLemma; + if (prefixLemma == null) { + continue; // something went wrong during registration of the prefix lemma (probably a duplicated colemma name) + } + Contract.Assume(prefixLemma.Ens.Count == 0 && prefixLemma.Body == null); // there are not supposed have have been filled in before + // compute the postconditions of the prefix lemma + var k = prefixLemma.Ins[0]; foreach (var p in com.Ens) { var coConclusions = new HashSet(); - CheckCoMethodConclusions(p.E, true, coConclusions); - var subst = new CoMethodPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this); + CheckCoLemmaConclusions(p.E, true, coConclusions); + var subst = new CoLemmaPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this); var post = subst.CloneExpr(p.E); - prefixMethod.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); + prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); } - // Compute the statement body of the prefix method + // Compute the statement body of the prefix lemma if (com.Body != null) { var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1)); - var subst = new CoMethodBodyCloner(com, kMinusOne, this); + var subst = new CoLemmaBodyCloner(com, kMinusOne, this); var mainBody = subst.CloneBlockStmt(com.Body); var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name)); var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, kPositive, mainBody, null); - prefixMethod.Body = new BlockStmt(com.tok, condBody.EndTok, new List() { condBody }); + prefixLemma.Body = new BlockStmt(com.tok, condBody.EndTok, new List() { condBody }); } - // The prefix method now has all its components, so it's finally time we resolve it - currentClass = (ClassDecl)prefixMethod.EnclosingClass; + // The prefix lemma now has all its components, so it's finally time we resolve it + currentClass = (ClassDecl)prefixLemma.EnclosingClass; allTypeParameters.PushMarker(); ResolveTypeParameters(currentClass.TypeArgs, false, currentClass); - ResolveTypeParameters(prefixMethod.TypeArgs, false, prefixMethod); - ResolveMethod(prefixMethod); + ResolveTypeParameters(prefixLemma.TypeArgs, false, prefixLemma); + ResolveMethod(prefixLemma); allTypeParameters.PopMarker(); currentClass = null; - CheckTypeInference_Member(prefixMethod); + CheckTypeInference_Member(prefixLemma); } } @@ -1666,7 +1666,7 @@ namespace Microsoft.Dafny } } // Check that copredicates are not recursive with non-copredicate functions, and - // check that comethods are not recursive with non-comethod methods. + // check that colemmas are not recursive with non-colemma methods. foreach (var d in declarations) { if (d is ClassDecl) { foreach (var member in ((ClassDecl)d).Members) { @@ -1684,10 +1684,10 @@ namespace Microsoft.Dafny if (fn.Body != null) { CoPredicateChecks(fn.Body, fn, CallingPosition.Positive); } - } else if (member is CoMethod) { - var m = (CoMethod)member; + } else if (member is CoLemma) { + var m = (CoLemma)member; if (m.Body != null) { - CoMethodChecks(m.Body, m); + CoLemmaChecks(m.Body, m); } } } @@ -2160,13 +2160,13 @@ namespace Microsoft.Dafny #endregion CoPredicateChecks // ------------------------------------------------------------------------------------------------------ - // ----- CoMethodChecks --------------------------------------------------------------------------------- + // ----- CoLemmaChecks ---------------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ - #region CoMethodChecks - class CoMethodChecks_Visitor : ResolverBottomUpVisitor + #region CoLemmaChecks + class CoLemmaChecks_Visitor : ResolverBottomUpVisitor { - CoMethod context; - public CoMethodChecks_Visitor(Resolver resolver, CoMethod context) + CoLemma context; + public CoLemmaChecks_Visitor(Resolver resolver, CoLemma context) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(context != null); @@ -2175,15 +2175,15 @@ namespace Microsoft.Dafny protected override void VisitOneStmt(Statement stmt) { if (stmt is CallStmt) { var s = (CallStmt)stmt; - if (s.Method is CoMethod || s.Method is PrefixMethod) { + if (s.Method is CoLemma || s.Method is PrefixLemma) { // all is cool } else { - // the call goes from a comethod context to a non-comethod callee + // the call goes from a colemma context to a non-colemma callee var moduleCaller = context.EnclosingClass.Module; var moduleCallee = s.Method.EnclosingClass.Module; if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { - // we're looking at a recursive call (to a non-comethod) - Error(s.Tok, "a recursive call from a comethod can go only to other comethods and prefix methods"); + // we're looking at a recursive call (to a non-colemma) + Error(s.Tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } } } @@ -2192,23 +2192,23 @@ namespace Microsoft.Dafny { if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; - // the call goes from a comethod context to a non-comethod callee + // the call goes from a colemma context to a non-colemma callee var moduleCaller = context.EnclosingClass.Module; var moduleCallee = e.Function.EnclosingClass.Module; if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) { - // we're looking at a recursive call (to a non-comethod) - Error(e.tok, "a recursive call from a comethod can go only to other comethods and prefix methods"); + // we're looking at a recursive call (to a non-colemma) + Error(e.tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } } } } - void CoMethodChecks(Statement stmt, CoMethod context) { + void CoLemmaChecks(Statement stmt, CoLemma context) { Contract.Requires(stmt != null); Contract.Requires(context != null); - var v = new CoMethodChecks_Visitor(this, context); + var v = new CoLemmaChecks_Visitor(this, context); v.Visit(stmt); } - #endregion CoMethodChecks + #endregion CoLemmaChecks // ------------------------------------------------------------------------------------------------------ // ----- CheckEqualityTypes ----------------------------------------------------------------------------- @@ -2582,10 +2582,10 @@ namespace Microsoft.Dafny ResolveTypeParameters(m.TypeArgs, true, m); ResolveMethodSignature(m); allTypeParameters.PopMarker(); - var com = m as CoMethod; - if (com != null && com.PrefixMethod != null && ec == ErrorCount) { - var mm = com.PrefixMethod; - // resolve signature of the prefix method + var com = m as CoLemma; + if (com != null && com.PrefixLemma != null && ec == ErrorCount) { + var mm = com.PrefixLemma; + // resolve signature of the prefix lemma mm.EnclosingClass = cl; allTypeParameters.PushMarker(); ResolveTypeParameters(mm.TypeArgs, true, mm); @@ -3091,8 +3091,8 @@ namespace Microsoft.Dafny ResolveFrameExpression(fe, "modifies", m); if (m is Lemma) { Error(fe.tok, "lemmas are not allowed to have modifies clauses"); - } else if (m is CoMethod) { - Error(fe.tok, "comethods are not allowed to have modifies clauses"); + } else if (m is CoLemma) { + Error(fe.tok, "colemmas are not allowed to have modifies clauses"); } } foreach (Expression e in m.Decreases.Expressions) { @@ -3106,8 +3106,8 @@ namespace Microsoft.Dafny // Add out-parameters to a new scope that will also include the outermost-level locals of the body // Don't care about any duplication errors among the out-parameters, since they have already been reported scope.PushMarker(); - if (m is CoMethod && m.Outs.Count != 0) { - Error(m.Outs[0].tok, "comethods are not allowed to have out-parameters"); + if (m is CoLemma && m.Outs.Count != 0) { + Error(m.Outs[0].tok, "colemmas are not allowed to have out-parameters"); } else { foreach (Formal p in m.Outs) { scope.Push(p.Name, p); @@ -3125,18 +3125,18 @@ namespace Microsoft.Dafny // Resolve body if (m.Body != null) { - var com = m as CoMethod; - if (com != null && com.PrefixMethod != null) { + var com = m as CoLemma; + if (com != null && com.PrefixLemma != null) { // The body may mentioned the implicitly declared parameter _k. Throw it into the // scope before resolving the body. - var k = com.PrefixMethod.Ins[0]; + var k = com.PrefixLemma.Ins[0]; scope.Push(k.Name, k); // we expect no name conflict for _k } var codeContext = m; ResolveBlockStatement(m.Body, m.IsGhost, codeContext); } - // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for comethods) + // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas) ResolveAttributes(m.Attributes, false, m); scope.PopMarker(); // for the out-parameters and outermost-level locals @@ -7735,35 +7735,35 @@ namespace Microsoft.Dafny /// /// This method adds to "coConclusions" all copredicate calls and codatatype equalities that occur /// in positive positions and not under existential quantification. If "expr" is the postcondition - /// of a comethod, then the "coConclusions" are the subexpressions that need to be replaced in order - /// to create the postcondition of the corresponding prefix method. + /// of a colemma, then the "coConclusions" are the subexpressions that need to be replaced in order + /// to create the postcondition of the corresponding prefix lemma. /// - void CheckCoMethodConclusions(Expression expr, bool position, ISet coConclusions) { + void CheckCoLemmaConclusions(Expression expr, bool position, ISet coConclusions) { Contract.Requires(expr != null); if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; - CheckCoMethodConclusions(e.ResolvedExpression, position, coConclusions); + CheckCoLemmaConclusions(e.ResolvedExpression, position, coConclusions); } else if (expr is LetExpr) { var e = (LetExpr)expr; // For simplicity, only look in the body of the let expression, that is, ignoring the RHS of the // binding and ignoring what that binding would expand to in the body. - CheckCoMethodConclusions(e.Body, position, coConclusions); + CheckCoLemmaConclusions(e.Body, position, coConclusions); } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; if (e.Op == UnaryExpr.Opcode.Not) { - CheckCoMethodConclusions(e.E, !position, coConclusions); + CheckCoLemmaConclusions(e.E, !position, coConclusions); } } else if (expr is BinaryExpr) { var bin = (BinaryExpr)expr; if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And || bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) { - CheckCoMethodConclusions(bin.E0, position, coConclusions); - CheckCoMethodConclusions(bin.E1, position, coConclusions); + CheckCoLemmaConclusions(bin.E0, position, coConclusions); + CheckCoLemmaConclusions(bin.E1, position, coConclusions); } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) { - CheckCoMethodConclusions(bin.E0, !position, coConclusions); - CheckCoMethodConclusions(bin.E1, position, coConclusions); + CheckCoLemmaConclusions(bin.E0, !position, coConclusions); + CheckCoLemmaConclusions(bin.E1, position, coConclusions); } else if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) { coConclusions.Add(bin); } else if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.NeqCommon && bin.E0.Type.IsCoDatatype) { @@ -7772,16 +7772,16 @@ namespace Microsoft.Dafny } else if (expr is ITEExpr) { var ite = (ITEExpr)expr; - CheckCoMethodConclusions(ite.Thn, position, coConclusions); - CheckCoMethodConclusions(ite.Els, position, coConclusions); + CheckCoLemmaConclusions(ite.Thn, position, coConclusions); + CheckCoLemmaConclusions(ite.Els, position, coConclusions); } else if (expr is StmtExpr) { var e = (StmtExpr)expr; - CheckCoMethodConclusions(e.E, position, coConclusions); + CheckCoLemmaConclusions(e.E, position, coConclusions); } else if (expr is OldExpr) { var e = (OldExpr)expr; - CheckCoMethodConclusions(e.E, position, coConclusions); + CheckCoLemmaConclusions(e.E, position, coConclusions); } else if (expr is FunctionCallExpr && position) { var fexp = (FunctionCallExpr)expr; diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index a65a32eb..92809143 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -511,8 +511,8 @@ public class Scanner { case "returns": t.kind = 36; break; case "method": t.kind = 40; break; case "lemma": t.kind = 41; break; - case "comethod": t.kind = 42; break; - case "colemma": t.kind = 43; break; + case "colemma": t.kind = 42; break; + case "comethod": t.kind = 43; break; case "constructor": t.kind = 44; break; case "modifies": t.kind = 45; break; case "free": t.kind = 46; break; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 7013a7ee..cb316008 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1109,10 +1109,10 @@ namespace Microsoft.Dafny { // the method spec itself sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.InterModuleCall)); sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.IntraModuleCall)); - if (m is CoMethod) { - // Let the CoCall and Impl forms to use m.PrefixMethod signature and specification (and - // note that m.PrefixMethod.Body == m.Body. - m = ((CoMethod)m).PrefixMethod; + if (m is CoLemma) { + // Let the CoCall and Impl forms to use m.PrefixLemma signature and specification (and + // note that m.PrefixLemma.Body == m.Body. + m = ((CoLemma)m).PrefixLemma; sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.CoCall)); } if (m.Body != null) { @@ -2224,7 +2224,7 @@ namespace Microsoft.Dafny { Bpl.StmtList stmts; if (!wellformednessProc) { - if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoMethod)) { + if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoLemma)) { var posts = new List(); m.Ens.ForEach(mfe => posts.Add(mfe.E)); var allIns = new List(); @@ -4156,7 +4156,7 @@ namespace Microsoft.Dafny { /// CoCall /// This procedure is suitable for (intra-module) co-calls. /// In these calls, some uses of copredicates may be replaced by - /// proof certificates. Note, unless the method is a comethod, there + /// proof certificates. Note, unless the method is a colemma, there /// is no reason to include a procedure for co-calls. /// Implementation /// This procedure is suitable for checking the implementation of the @@ -6321,10 +6321,10 @@ namespace Microsoft.Dafny { // consult the call graph to figure out if this is a recursive call var module = method.EnclosingClass.Module; if (codeContext != null && module == currentModule) { - // Note, prefix methods are not recorded in the call graph, but their corresponding comethods are. + // Note, prefix lemmas are not recorded in the call graph, but their corresponding colemmas are. // Similarly, an iterator is not recorded in the call graph, but its MoveNext method is. ICallable cllr = - codeContext is PrefixMethod ? ((PrefixMethod)codeContext).Co : + codeContext is PrefixLemma ? ((PrefixLemma)codeContext).Co : codeContext is IteratorDecl ? ((IteratorDecl)codeContext).Member_MoveNext : codeContext; if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) { @@ -6334,11 +6334,11 @@ namespace Microsoft.Dafny { MethodTranslationKind kind; var callee = method; - if (method is CoMethod && isRecursiveCall) { + if (method is CoLemma && isRecursiveCall) { kind = MethodTranslationKind.CoCall; - callee = ((CoMethod)method).PrefixMethod; - } else if (method is PrefixMethod) { - // an explicit call to a prefix method is allowed only inside the SCC of the corresponding comethod, + callee = ((CoLemma)method).PrefixLemma; + } else if (method is PrefixLemma) { + // an explicit call to a prefix lemma is allowed only inside the SCC of the corresponding colemma, // so we consider this to be a co-call kind = MethodTranslationKind.CoCall; } else if (module == currentModule) { @@ -6373,13 +6373,13 @@ namespace Microsoft.Dafny { var param = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified? Bpl.Expr bActual; - if (i == 0 && method is CoMethod && isRecursiveCall) { - // Treat this call to M(args) as a call to the corresponding prefix method M#(_k - 1, args), so insert an argument here. - var k = ((PrefixMethod)codeContext).K; + if (i == 0 && method is CoLemma && isRecursiveCall) { + // Treat this call to M(args) as a call to the corresponding prefix lemma M#(_k - 1, args), so insert an argument here. + var k = ((PrefixLemma)codeContext).K; bActual = Bpl.Expr.Sub(new Bpl.IdentifierExpr(k.tok, k.AssignUniqueName(currentDeclaration), Bpl.Type.Int), Bpl.Expr.Literal(1)); } else { Expression actual; - if (method is CoMethod && isRecursiveCall) { + if (method is CoLemma && isRecursiveCall) { actual = Args[i - 1]; } else { actual = Args[i]; @@ -10084,7 +10084,7 @@ namespace Microsoft.Dafny { // The argument position is considered to be "variant" if the function is recursive and... // ... it has something to do with why the callee is well-founded, which happens when... if (f is ImplicitFormal) { - // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix method, or + // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or variantArgument = true; } else if (decr.Exists(ee => ContainsFreeVariable(ee, false, f))) { // ... it participates in the effective decreases clause of the function, which happens when it is diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs index d643da5d..7c786d7e 100644 --- a/Source/DafnyExtension/OutliningTagger.cs +++ b/Source/DafnyExtension/OutliningTagger.cs @@ -171,11 +171,11 @@ namespace DafnyLanguage } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) { var nm = m is Dafny.Constructor ? "constructor" : - m is Dafny.CoMethod ? "comethod" : + m is Dafny.CoLemma ? "colemma" : m is Dafny.Lemma ? "lemma" : - // m is Dafny.PrefixMethod ? "prefix method" : // this won't ever occur here + // m is Dafny.PrefixLemma ? "prefix lemma" : // this won't ever occur here "method"; - if (m.IsGhost && !(m is Dafny.CoMethod)) { + if (m.IsGhost && !(m is Dafny.CoLemma)) { nm = "ghost " + nm; } newRegions.Add(new OutliningRegion(m, nm)); diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 88f956bd..b4896e9e 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -264,7 +264,7 @@ namespace DafnyLanguage case "class": case "codatatype": case "colemma": - case "comethod": + case "colemma": case "constructor": case "copredicate": case "datatype": diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index a41cd0cd..f56af482 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -60,7 +60,7 @@ lemma M(x: int) { } -comethod M'(x': int) +colemma M'(x': int) ensures true; { } @@ -1392,11 +1392,11 @@ CoResolution.dfy(64,10): Error: a copredicate is not allowed to declare any read CoResolution.dfy(70,31): Error: a copredicate is not allowed to declare any ensures clause CoResolution.dfy(79,20): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(83,20): Error: a recursive call from a copredicate can go only to other copredicates -CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to other comethods and prefix methods -CoResolution.dfy(106,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods -CoResolution.dfy(107,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods -CoResolution.dfy(126,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods -CoResolution.dfy(127,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods +CoResolution.dfy(92,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas +CoResolution.dfy(106,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas +CoResolution.dfy(107,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas +CoResolution.dfy(126,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas +CoResolution.dfy(127,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates 16 resolution/type errors detected in CoResolution.dfy diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy index 06692314..7c010a09 100644 --- a/Test/dafny0/CoPrefix.dfy +++ b/Test/dafny0/CoPrefix.dfy @@ -26,7 +26,7 @@ copredicate atmost(a: Stream, b: Stream) case Cons(h,t) => b.Cons? && h <= b.head && atmost(t, b.tail) } -comethod {:induction false} Theorem0() +colemma {:induction false} Theorem0() ensures atmost(zeros(), ones()); { // the following shows two equivalent ways to getting essentially the @@ -48,7 +48,7 @@ ghost method Theorem0_Manual() datatype Natural = Zero | Succ(Natural); -comethod {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural) +colemma {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural) ensures atmost(zeros(), ones()); decreases y; { @@ -62,7 +62,7 @@ comethod {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Nat Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y); } -comethod {:induction false} Theorem0_TerminationFailure_DefaultDecreases(y: Natural) +colemma {:induction false} Theorem0_TerminationFailure_DefaultDecreases(y: Natural) ensures atmost(zeros(), ones()); { match (y) { @@ -80,7 +80,7 @@ ghost method {:induction true} Theorem0_Lemma(k: nat) { } -comethod {:induction false} Theorem1() +colemma {:induction false} Theorem1() ensures append(zeros(), ones()) == zeros(); { Theorem1(); @@ -98,14 +98,14 @@ copredicate Pos(s: IList) s.head > 0 && Pos(s.tail) } -comethod {:induction false} Theorem2(n: int) +colemma {:induction false} Theorem2(n: int) requires 1 <= n; ensures Pos(UpIList(n)); { Theorem2(n+1); } -comethod {:induction false} Theorem2_NotAProof(n: int) +colemma {:induction false} Theorem2_NotAProof(n: int) requires 1 <= n; ensures Pos(UpIList(n)); { // error: this is not a proof (without automatic induction) @@ -125,7 +125,7 @@ function GG(h: T): TList TCons(h, GG(Next(h))) } -comethod {:induction false} Compare(h: T) +colemma {:induction false} Compare(h: T) ensures FF(h) == GG(h); { assert FF(h).head == GG(h).head; @@ -143,7 +143,7 @@ comethod {:induction false} Compare(h: T) } } -comethod {:induction false} BadTheorem(s: IList) +colemma {:induction false} BadTheorem(s: IList) ensures false; { // error: postcondition violation BadTheorem(s.tail); @@ -153,36 +153,36 @@ comethod {:induction false} BadTheorem(s: IList) // Make sure recursive calls get checked for termination module Recursion { - comethod X() { Y(); } - comethod Y() { X(); } + colemma X() { Y(); } + colemma Y() { X(); } - comethod G(x: int) + colemma G(x: int) ensures x < 100; { // error: postcondition violation (when _k == 0) H(x); } - comethod H(x: int) + colemma H(x: int) ensures x < 100; { // error: postcondition violation (when _k == 0) G(x); } - comethod A(x: int) { B(x); } - comethod B(x: int) + colemma A(x: int) { B(x); } + colemma B(x: int) { A#[10](x); // error: this is a recursive call, and the termination metric may not be going down } - comethod A'(x: int) { B'(x); } - comethod B'(x: int) + colemma A'(x: int) { B'(x); } + colemma B'(x: int) { if (10 < _k) { A'#[10](x); } } - comethod A''(x: int) { B''(x); } - comethod B''(x: int) + colemma A''(x: int) { B''(x); } + colemma B''(x: int) { if (0 < x) { A''#[_k](x-1); diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 9ab52d53..a7111a09 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -18,7 +18,7 @@ module TestModule { S#[_k](d) // error: _k is not an identifier in scope } - comethod CM(d: set) + colemma CM(d: set) { var b; b := this.S#[5](d); @@ -82,26 +82,26 @@ module Mojul1 { copredicate X() { Y() } copredicate Y() { X#[10]() } // error: X is not allowed to depend on X# - comethod M() + colemma M() { N(); } - comethod N() + colemma N() { Z(); - W(); // error: not allowed to make co-recursive call to non-comethod + W(); // error: not allowed to make co-recursive call to non-colemma } ghost method Z() { } ghost method W() { M(); } - comethod G() { H(); } - comethod H() { G#[10](); } // fine for comethod/prefix-method + colemma G() { H(); } + colemma H() { G#[10](); } // fine for colemma/prefix-lemma } module CallGraph { - // comethod -> copredicate -> comethod - // comethod -> copredicate -> prefix method - comethod CoLemma(n: nat) + // colemma -> copredicate -> colemma + // colemma -> copredicate -> prefix lemma + colemma CoLemma(n: nat) { var q := Q(n); // error var r := R(n); // error @@ -119,9 +119,9 @@ module CallGraph { false } - // comethod -> prefix predicate -> comethod - // comethod -> prefix predicate -> prefix method - comethod CoLemma_D(n: nat) + // colemma -> prefix predicate -> colemma + // colemma -> prefix predicate -> prefix lemma + colemma CoLemma_D(n: nat) { var q := Q_D#[n](n); // error var r := R_D#[n](n); // error diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy index b31dc5be..27b279c3 100644 --- a/Test/dafny0/Coinductive.dfy +++ b/Test/dafny0/Coinductive.dfy @@ -133,7 +133,7 @@ module CoPredicateResolutionErrors { // -------------------------------------------------- -module UnfruitfulCoMethodConclusions { +module UnfruitfulCoLemmaConclusions { codatatype Stream = Cons(head: T, tail: Stream); copredicate Positive(s: Stream) @@ -141,13 +141,13 @@ module UnfruitfulCoMethodConclusions { s.head > 0 && Positive(s.tail) } - comethod BadTheorem(s: Stream) + colemma BadTheorem(s: Stream) ensures false; { BadTheorem(s.tail); } - comethod CM(s: Stream) + colemma CM(s: Stream) ensures true && !false; ensures s.head == 8 ==> Positive(s); ensures s.tail == s; diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy index b7dea89d..d3112233 100644 --- a/Test/dafny0/CoinductiveProofs.dfy +++ b/Test/dafny0/CoinductiveProofs.dfy @@ -10,14 +10,14 @@ copredicate Pos(s: Stream) 0 < s.head && Pos(s.tail) } -comethod {:induction false} PosLemma0(n: int) +colemma {:induction false} PosLemma0(n: int) requires 1 <= n; ensures Pos(Upward(n)); { PosLemma0(n + 1); // this completes the proof } -comethod {:induction false} PosLemma1(n: int) +colemma {:induction false} PosLemma1(n: int) requires 1 <= n; ensures Pos(Upward(n)); { @@ -27,7 +27,7 @@ comethod {:induction false} PosLemma1(n: int) } } -comethod {:induction false} Outside_CoMethod_Caller_PosLemma(n: int) +colemma {:induction false} Outside_CoLemma_Caller_PosLemma(n: int) requires 1 <= n; ensures Pos(Upward(n)); { @@ -51,19 +51,19 @@ copredicate X(s: Stream) // this is equivalent to always returning 'true' X(s) } -comethod {:induction false} AlwaysLemma_X0(s: Stream) +colemma {:induction false} AlwaysLemma_X0(s: Stream) ensures X(s); // prove that X(s) really is always 'true' { // error: this is not the right proof AlwaysLemma_X0(s.tail); } -comethod {:induction false} AlwaysLemma_X1(s: Stream) +colemma {:induction false} AlwaysLemma_X1(s: Stream) ensures X(s); // prove that X(s) really is always 'true' { AlwaysLemma_X1(s); // this is the right proof } -comethod {:induction false} AlwaysLemma_X2(s: Stream) +colemma {:induction false} AlwaysLemma_X2(s: Stream) ensures X(s); { AlwaysLemma_X2(s); @@ -77,19 +77,19 @@ copredicate Y(s: Stream) // this is equivalent to always returning 'true' Y(s.tail) } -comethod {:induction false} AlwaysLemma_Y0(s: Stream) +colemma {:induction false} AlwaysLemma_Y0(s: Stream) ensures Y(s); // prove that Y(s) really is always 'true' { AlwaysLemma_Y0(s.tail); // this is a correct proof } -comethod {:induction false} AlwaysLemma_Y1(s: Stream) +colemma {:induction false} AlwaysLemma_Y1(s: Stream) ensures Y(s); { // error: this is not the right proof AlwaysLemma_Y1(s); } -comethod {:induction false} AlwaysLemma_Y2(s: Stream) +colemma {:induction false} AlwaysLemma_Y2(s: Stream) ensures Y(s); { AlwaysLemma_Y2(s.tail); @@ -103,7 +103,7 @@ copredicate Z(s: Stream) false } -comethod {:induction false} AlwaysLemma_Z(s: Stream) +colemma {:induction false} AlwaysLemma_Z(s: Stream) ensures Z(s); // says, perversely, that Z(s) is always 'true' { // error: this had better not lead to a proof AlwaysLemma_Z(s); @@ -119,7 +119,7 @@ copredicate Even(s: Stream) s.head % 2 == 0 && Even(s.tail) } -comethod {:induction false} Lemma0(n: int) +colemma {:induction false} Lemma0(n: int) ensures Even(Doubles(n)); { Lemma0(n+1); @@ -130,25 +130,25 @@ function UpwardBy2(n: int): Stream Cons(n, UpwardBy2(n + 2)) } -comethod {:induction false} Lemma1(n: int) +colemma {:induction false} Lemma1(n: int) ensures Even(UpwardBy2(2*n)); { Lemma1(n+1); } -comethod {:induction false} ProveEquality(n: int) +colemma {:induction false} ProveEquality(n: int) ensures Doubles(n) == UpwardBy2(2*n); { ProveEquality(n+1); } -comethod {:induction false} BadEquality0(n: int) +colemma {:induction false} BadEquality0(n: int) ensures Doubles(n) == UpwardBy2(n); { // error: postcondition does not hold BadEquality0(n+1); } -comethod {:induction false} BadEquality1(n: int) +colemma {:induction false} BadEquality1(n: int) ensures Doubles(n) == UpwardBy2(n+1); { // error: postcondition does not hold BadEquality1(n+1); diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy index 287b4006..4b39876a 100644 --- a/Test/dafny3/Filter.dfy +++ b/Test/dafny3/Filter.dfy @@ -13,20 +13,20 @@ copredicate IsSubStream(s: Stream, u: Stream) In(s.head, u) && IsSubStream(s.tail, u) } -ghost method Lemma_InTail(x: T, s: Stream) +lemma Lemma_InTail(x: T, s: Stream) requires In(x, s.tail); ensures In(x, s); { var n :| 0 <= n && Tail(s.tail, n).head == x; assert Tail(s, n+1).head == x; } -comethod Lemma_TailSubStream(s: Stream, u: Stream) +colemma Lemma_TailSubStream(s: Stream, u: Stream) requires IsSubStream(s, u.tail); ensures IsSubStream(s, u); { Lemma_InTail(s.head, u); } -ghost method Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat) // this lemma could have been used to prove the previous one +lemma Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat) // this lemma could have been used to prove the previous one requires IsSubStream#[k](s, u.tail); ensures IsSubStream#[k](s, u); { @@ -35,7 +35,7 @@ ghost method Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat) // this lemma c Lemma_TailSubStreamK(s.tail, u, k-1); } } -ghost method Lemma_InSubStream(x: T, s: Stream, u: Stream) +lemma Lemma_InSubStream(x: T, s: Stream, u: Stream) requires In(x, s) && IsSubStream(s, u); ensures In(x, u); { @@ -57,7 +57,7 @@ copredicate AllP(s: Stream, h: PredicateHandle) { P(s.head, h) && AllP(s.tail, h) } -ghost method Lemma_InAllP(x: T, s: Stream, h: PredicateHandle) +lemma Lemma_InAllP(x: T, s: Stream, h: PredicateHandle) requires In(x, s) && AllP(s, h); ensures P(x, h); { @@ -80,7 +80,7 @@ copredicate AlwaysAnother(s: Stream, h: PredicateHandle) { IsAnother(s, h) && AlwaysAnother(s.tail, h) } -comethod Lemma_AllImpliesAlwaysAnother(s: Stream, h: PredicateHandle) +colemma Lemma_AllImpliesAlwaysAnother(s: Stream, h: PredicateHandle) requires AllP(s, h); ensures AlwaysAnother(s, h); { @@ -118,7 +118,7 @@ function Filter(s: Stream, h: PredicateHandle): Stream Filter(s.tail, h) } // properties about Filter -comethod Filter_AlwaysAnother(s: Stream, h: PredicateHandle) +colemma Filter_AlwaysAnother(s: Stream, h: PredicateHandle) requires AlwaysAnother(s, h); ensures AllP(Filter(s, h), h); decreases Next(s, h); @@ -129,7 +129,7 @@ comethod Filter_AlwaysAnother(s: Stream, h: PredicateHandle) Filter_AlwaysAnother#[_k](s.tail, h); } } -comethod Filter_IsSubStream(s: Stream, h: PredicateHandle) +colemma Filter_IsSubStream(s: Stream, h: PredicateHandle) requires AlwaysAnother(s, h); ensures IsSubStream(Filter(s, h), s); decreases Next(s, h); @@ -160,7 +160,7 @@ comethod Filter_IsSubStream(s: Stream, h: PredicateHandle) } // The following says nothing about the order of the elements in the stream -ghost method Theorem_Filter(s: Stream, h: PredicateHandle) +lemma Theorem_Filter(s: Stream, h: PredicateHandle) requires AlwaysAnother(s, h); ensures forall x :: In(x, Filter(s, h)) <==> In(x, s) && P(x, h); { @@ -177,7 +177,7 @@ ghost method Theorem_Filter(s: Stream, h: PredicateHandle) } } -ghost method FS_Ping(s: Stream, h: PredicateHandle, x: T) +lemma FS_Ping(s: Stream, h: PredicateHandle, x: T) requires AlwaysAnother(s, h) && In(x, Filter(s, h)); ensures In(x, s) && P(x, h); { @@ -189,7 +189,7 @@ ghost method FS_Ping(s: Stream, h: PredicateHandle, x: T) Lemma_InAllP(x, Filter(s, h), h); } -ghost method FS_Pong(s: Stream, h: PredicateHandle, x: T, k: nat) +lemma FS_Pong(s: Stream, h: PredicateHandle, x: T, k: nat) requires AlwaysAnother(s, h) && In(x, s) && P(x, h); requires Tail(s, k).head == x; ensures In(x, Filter(s, h)); @@ -226,19 +226,19 @@ copredicate IncrFrom(s: Stream, low: int, ord: PredicateHandle) low <= Ord(s.head, ord) && IncrFrom(s.tail, Ord(s.head, ord) + 1, ord) } -comethod Lemma_Incr0(s: Stream, low: int, ord: PredicateHandle) +colemma Lemma_Incr0(s: Stream, low: int, ord: PredicateHandle) requires IncrFrom(s, low, ord); ensures Increasing(s, ord); { } -comethod Lemma_Incr1(s: Stream, ord: PredicateHandle) +colemma Lemma_Incr1(s: Stream, ord: PredicateHandle) requires Increasing(s, ord); ensures IncrFrom(s, Ord(s.head, ord), ord); { Lemma_Incr1(s.tail, ord); } -ghost method Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: PredicateHandle) +lemma Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: PredicateHandle) requires Increasing(s, ord) && AlwaysAnother(s, h); ensures Increasing(Filter(s, h), ord); { @@ -246,7 +246,7 @@ ghost method Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: Lemma_FilterPreservesIncrFrom(s, h, Ord(s.head, ord), ord); Lemma_Incr0(Filter(s, h), Ord(s.head, ord), ord); } -comethod Lemma_FilterPreservesIncrFrom(s: Stream, h: PredicateHandle, low: int, ord: PredicateHandle) +colemma Lemma_FilterPreservesIncrFrom(s: Stream, h: PredicateHandle, low: int, ord: PredicateHandle) requires IncrFrom(s, low, ord) && AlwaysAnother(s, h) && low <= Ord(s.head, ord); ensures IncrFrom(Filter(s, h), low, ord); decreases Next(s, h); diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy index 8709a6d8..5c5c0412 100644 --- a/Test/dafny3/InductionVsCoinduction.dfy +++ b/Test/dafny3/InductionVsCoinduction.dfy @@ -62,7 +62,7 @@ function SAppend(xs: Stream, ys: Stream): Stream we also get ==#[k]. */ -ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stream) +lemma {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stream) ensures SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c)); decreases k; { @@ -72,7 +72,7 @@ ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, } } -ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream) +lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream) ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c)); { forall k:nat { SAppendIsAssociativeK(k, a, b, c); } @@ -80,8 +80,8 @@ ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream) assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); } -// Equivalent proof using the comethod syntax. -comethod {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream) +// Equivalent proof using the colemma syntax. +colemma {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream) ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c)); { match (a) { @@ -91,26 +91,26 @@ comethod {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream) } // In fact the proof can be fully automatic. -comethod SAppendIsAssociative_Auto(a:Stream, b:Stream, c:Stream) +colemma SAppendIsAssociative_Auto(a:Stream, b:Stream, c:Stream) ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c)); { } -comethod {:induction false} UpPos(n:int) +colemma {:induction false} UpPos(n:int) requires n > 0; ensures Pos(Up(n)); { UpPos(n+1); } -comethod UpPos_Auto(n:int) +colemma UpPos_Auto(n:int) requires n > 0; ensures Pos(Up(n)); { } // This does induction and coinduction in the same proof. -comethod {:induction false} FivesUpPos(n:int) +colemma {:induction false} FivesUpPos(n:int) requires n > 0; ensures Pos(FivesUp(n)); decreases 4 - (n-1) % 5; @@ -124,7 +124,7 @@ comethod {:induction false} FivesUpPos(n:int) // Again, Dafny can just employ induction tactic and do it automatically. // The only hint required is the decrease clause. -comethod FivesUpPos_Auto(n:int) +colemma FivesUpPos_Auto(n:int) requires n > 0; ensures Pos(FivesUp(n)); decreases 4 - (n-1) % 5; diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy index e189dc4a..32a868bb 100644 --- a/Test/dafny3/InfiniteTrees.dfy +++ b/Test/dafny3/InfiniteTrees.dfy @@ -10,12 +10,12 @@ function Tail(s: Stream, n: nat): Stream if t == Nil then t else t.tail } -ghost method Tail_Lemma0(s: Stream, n: nat) +lemma Tail_Lemma0(s: Stream, n: nat) requires s.Cons? && Tail(s, n).Cons?; ensures Tail(s, n).tail == Tail(s.tail, n); { } -ghost method Tail_Lemma1(s: Stream, k: nat, n: nat) +lemma Tail_Lemma1(s: Stream, k: nat, n: nat) requires k <= n; ensures Tail(s, n).Cons? ==> Tail(s, k).Cons?; // Note, the contrapositive of this lemma says: Tail(s, k) == Nil ==> Tail(s, n) == Nil @@ -24,7 +24,7 @@ ghost method Tail_Lemma1(s: Stream, k: nat, n: nat) assert Tail(s, n) == Tail(s, n-1).tail; } } -ghost method Tail_Lemma2(s: Stream, n: nat) +lemma Tail_Lemma2(s: Stream, n: nat) requires s.Cons? && Tail(s.tail, n).Cons?; ensures Tail(s, n).Cons?; { @@ -48,7 +48,7 @@ function AnInfiniteStream(): Stream { Cons(0, AnInfiniteStream()) } -comethod Proposition0() +colemma Proposition0() ensures IsNeverEndingStream(AnInfiniteStream()); { } @@ -76,7 +76,7 @@ copredicate LowerThan(s: Stream, n: nat) // Co-predicate LowerThan(s, n) recurses on LowerThan(s.tail, n). Thus, a property of LowerThan is that // LowerThan(s, h) implies LowerThan(s', h) for any suffix s' of s. -ghost method LowerThan_Lemma(s: Stream, n: nat, h: nat) +lemma LowerThan_Lemma(s: Stream, n: nat, h: nat) ensures LowerThan(s, h) ==> LowerThan(Tail(s, n), h); { Tail_Lemma1(s, 0, n); @@ -113,7 +113,7 @@ function SkinnyTree(): Tree { Node(Cons(SkinnyTree(), Nil)) } -ghost method Proposition1() +lemma Proposition1() ensures IsFiniteSomewhere(SkinnyTree()) && !HasBoundedHeight(SkinnyTree()); { assert forall n :: 0 <= n ==> !LowerThan(SkinnyTree().children, n); @@ -121,7 +121,7 @@ ghost method Proposition1() // Any tree where all paths have bounded height are finite somewhere. -ghost method Theorem0(t: Tree) +lemma Theorem0(t: Tree) requires HasBoundedHeight(t); ensures IsFiniteSomewhere(t); { @@ -133,7 +133,7 @@ ghost method Theorem0(t: Tree) */ var k := FindNil(t.children, n); } -ghost method FindNil(s: Stream, n: nat) returns (k: nat) +lemma FindNil(s: Stream, n: nat) returns (k: nat) requires LowerThan(s, n); ensures !InfiniteEverywhere#[k](s); { @@ -175,17 +175,17 @@ function ATreeChildren(): Stream { Cons(Node(Nil), ATreeChildren()) } -ghost method Proposition2() +lemma Proposition2() ensures !HasFiniteHeightEverywhere_Bad(ATree()); { Proposition2_Lemma0(); Proposition2_Lemma1(ATreeChildren()); } -comethod Proposition2_Lemma0() +colemma Proposition2_Lemma0() ensures IsNeverEndingStream(ATreeChildren()); { } -comethod Proposition2_Lemma1(s: Stream) +colemma Proposition2_Lemma1(s: Stream) requires IsNeverEndingStream(s); ensures InfiniteHeightSomewhere_Bad(s); { @@ -237,7 +237,7 @@ copredicate ValidPath(t: Tree, p: Stream) var ch := Tail(t.children, index); ch.Cons? && ValidPath(ch.head, tail) } -ghost method ValidPath_Lemma(p: Stream) +lemma ValidPath_Lemma(p: Stream) ensures ValidPath(Node(Nil), p) ==> p == Nil; { if ValidPath(Node(Nil), p) { @@ -258,7 +258,7 @@ predicate HasFiniteHeight(t: Tree) // From this definition, we can prove that any tree of bounded height is also of finite height. -ghost method Theorem1(t: Tree) +lemma Theorem1(t: Tree) requires HasBoundedHeight(t); ensures HasFiniteHeight(t); { @@ -267,7 +267,7 @@ ghost method Theorem1(t: Tree) Theorem1_Lemma(t, n, p); } } -ghost method Theorem1_Lemma(t: Tree, n: nat, p: Stream) +lemma Theorem1_Lemma(t: Tree, n: nat, p: Stream) requires LowerThan(t.children, n) && ValidPath(t, p); ensures !IsNeverEndingStream(p); decreases n; @@ -311,7 +311,7 @@ function EverLongerSkinnyTrees(n: nat): Stream Cons(SkinnyFiniteTree(n), EverLongerSkinnyTrees(n+1)) } -ghost method EverLongerSkinnyTrees_Lemma(k: nat, n: nat) +lemma EverLongerSkinnyTrees_Lemma(k: nat, n: nat) ensures Tail(EverLongerSkinnyTrees(k), n).Cons?; ensures Tail(EverLongerSkinnyTrees(k), n).head == SkinnyFiniteTree(k+n); decreases n; @@ -330,13 +330,13 @@ ghost method EverLongerSkinnyTrees_Lemma(k: nat, n: nat) } } -ghost method Proposition3() +lemma Proposition3() ensures !HasBoundedHeight(FiniteUnboundedTree()) && HasFiniteHeight(FiniteUnboundedTree()); { Proposition3a(); Proposition3b(); } -ghost method Proposition3a() +lemma Proposition3a() ensures !HasBoundedHeight(FiniteUnboundedTree()); { var ch := FiniteUnboundedTree().children; @@ -350,7 +350,7 @@ ghost method Proposition3a() LowerThan_Lemma(ch, n+1, n); } } -ghost method Proposition3b() +lemma Proposition3b() ensures HasFiniteHeight(FiniteUnboundedTree()); { var t := FiniteUnboundedTree(); @@ -369,7 +369,7 @@ ghost method Proposition3b() Proposition3b_Lemma(si, index, p.tail); } } -ghost method Proposition3b_Lemma(t: Tree, h: nat, p: Stream) +lemma Proposition3b_Lemma(t: Tree, h: nat, p: Stream) requires LowerThan(t.children, h) && ValidPath(t, p); ensures !IsNeverEndingStream(p); decreases h; @@ -495,7 +495,7 @@ function N2S'(n: nat, num: Number): Stream case Succ(next) => N2S'(n + 1, next) } -ghost method Path_Lemma0(t: Tree, p: Stream) +lemma Path_Lemma0(t: Tree, p: Stream) requires ValidPath(t, p); ensures ValidPath_Alt(t, S2N(p)); { @@ -503,7 +503,7 @@ ghost method Path_Lemma0(t: Tree, p: Stream) Path_Lemma0'(t, p); } } -comethod Path_Lemma0'(t: Tree, p: Stream) +colemma Path_Lemma0'(t: Tree, p: Stream) requires ValidPath(t, p); ensures ValidPath_Alt(t, S2N(p)); { @@ -526,7 +526,7 @@ comethod Path_Lemma0'(t: Tree, p: Stream) } } } -comethod Path_Lemma0''(tChildren: Stream, n: nat, tail: Stream) +colemma Path_Lemma0''(tChildren: Stream, n: nat, tail: Stream) requires var ch := Tail(tChildren, n); ch.Cons? && ValidPath(ch.head, tail); ensures ValidPath_Alt'(tChildren, S2N'(n, tail)); { @@ -545,7 +545,7 @@ comethod Path_Lemma0''(tChildren: Stream, n: nat, tail: Stream) Path_Lemma0'(tChildren.head, tail); } } -ghost method Path_Lemma1(t: Tree, r: CoOption) +lemma Path_Lemma1(t: Tree, r: CoOption) requires ValidPath_Alt(t, r); ensures ValidPath(t, N2S(r)); { @@ -553,7 +553,7 @@ ghost method Path_Lemma1(t: Tree, r: CoOption) Path_Lemma1'(t, r); } } -comethod Path_Lemma1'(t: Tree, r: CoOption) +colemma Path_Lemma1'(t: Tree, r: CoOption) requires ValidPath_Alt(t, r); ensures ValidPath(t, N2S(r)); decreases 1; @@ -576,7 +576,7 @@ comethod Path_Lemma1'(t: Tree, r: CoOption) } } } -comethod Path_Lemma1''(s: Stream, n: nat, num: Number) +colemma Path_Lemma1''(s: Stream, n: nat, num: Number) requires ValidPath_Alt'(Tail(s, n), num); ensures ValidPath(Node(s), N2S'(n, num)); decreases 0, num; @@ -596,14 +596,14 @@ comethod Path_Lemma1''(s: Stream, n: nat, num: Number) } } } -ghost method Path_Lemma2(p: Stream) +lemma Path_Lemma2(p: Stream) ensures IsNeverEndingStream(p) ==> InfinitePath(S2N(p)); { if IsNeverEndingStream(p) { Path_Lemma2'(p); } } -comethod Path_Lemma2'(p: Stream) +colemma Path_Lemma2'(p: Stream) requires IsNeverEndingStream(p); ensures InfinitePath(S2N(p)); { @@ -622,7 +622,7 @@ comethod Path_Lemma2'(p: Stream) } } } -comethod Path_Lemma2''(p: Stream, n: nat, tail: Stream) +colemma Path_Lemma2''(p: Stream, n: nat, tail: Stream) requires IsNeverEndingStream(p) && p.tail == tail; ensures InfinitePath'(S2N'(n, tail)); { @@ -648,7 +648,7 @@ comethod Path_Lemma2''(p: Stream, n: nat, tail: Stream) } } } -ghost method Path_Lemma3(r: CoOption) +lemma Path_Lemma3(r: CoOption) ensures InfinitePath(r) ==> IsNeverEndingStream(N2S(r)); { if InfinitePath(r) { @@ -657,7 +657,7 @@ ghost method Path_Lemma3(r: CoOption) } } } -comethod Path_Lemma3'(n: nat, num: Number) +colemma Path_Lemma3'(n: nat, num: Number) requires InfinitePath'(num); ensures IsNeverEndingStream(N2S'(n, num)); decreases num; @@ -678,7 +678,7 @@ comethod Path_Lemma3'(n: nat, num: Number) } } -ghost method Theorem2(t: Tree) +lemma Theorem2(t: Tree) ensures HasFiniteHeight(t) <==> HasFiniteHeight_Alt(t); { if HasFiniteHeight_Alt(t) { diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy index 431ff543..37586ec7 100644 --- a/Test/dafny3/Paulson.dfy +++ b/Test/dafny3/Paulson.dfy @@ -10,7 +10,7 @@ function Apply(f: FunctionHandle, argument: T): T // Function composition function After(f: FunctionHandle, g: FunctionHandle): FunctionHandle -ghost method Definition_After(f: FunctionHandle, g: FunctionHandle, arg: T) +lemma Definition_After(f: FunctionHandle, g: FunctionHandle, arg: T) ensures Apply(After(f, g), arg) == Apply(f, Apply(g, arg)); function Lmap(f: FunctionHandle, a: LList): LList @@ -29,7 +29,7 @@ function Lappend(a: LList, b: LList): LList // ---------- Section 8.3 ---------- -comethod Example6(f: FunctionHandle, g: FunctionHandle, M: LList) +colemma Example6(f: FunctionHandle, g: FunctionHandle, M: LList) ensures Lmap(After(f, g), M) == Lmap(f, Lmap(g, M)); { match M { @@ -61,7 +61,7 @@ function Iterates(f: FunctionHandle>, M: LList): LList> Cons(M, Iterates(f, Apply(f, M))) } -comethod Eq24(f: FunctionHandle>, M: LList) +colemma Eq24(f: FunctionHandle>, M: LList) ensures Lmap(f, Iterates(f, M)) == Iterates(f, Apply(f, M)); { calc { @@ -80,7 +80,7 @@ comethod Eq24(f: FunctionHandle>, M: LList) } } -ghost method CorollaryEq24(f: FunctionHandle>, M: LList) +lemma CorollaryEq24(f: FunctionHandle>, M: LList) ensures Iterates(f, M) == Cons(M, Lmap(f, Iterates(f, M))); { Eq24(f, M); @@ -92,7 +92,7 @@ ghost method CorollaryEq24(f: FunctionHandle>, M: LList) // Let h be any function function h(f: FunctionHandle>, M: LList): LList> // ... that satisfies the property in CorollaryEq24: -ghost method Definition_h(f: FunctionHandle>, M: LList) +lemma Definition_h(f: FunctionHandle>, M: LList) ensures h(f, M) == Cons(M, Lmap(f, h(f, M))); // Functions to support the proof: @@ -107,19 +107,19 @@ function LmapIter(n: nat, f: FunctionHandle, arg: LList): LList if n == 0 then arg else Lmap(f, LmapIter(n-1, f, arg)) } -ghost method Lemma25(n: nat, f: FunctionHandle, b: A, M: LList) +lemma Lemma25(n: nat, f: FunctionHandle, b: A, M: LList) ensures LmapIter(n, f, Cons(b, M)) == Cons(Iter(n, f, b), LmapIter(n, f, M)); { // proof is by (automatic) induction } -ghost method Lemma26(n: nat, f: FunctionHandle, x: LList) // (26) in the paper, but with f := LMap f +lemma Lemma26(n: nat, f: FunctionHandle, x: LList) // (26) in the paper, but with f := LMap f ensures LmapIter(n, f, Lmap(f, x)) == LmapIter(n+1, f, x); { // proof is by (automatic) induction } -comethod BisimulationLemma(n: nat, f: FunctionHandle>, u: LList) +colemma BisimulationLemma(n: nat, f: FunctionHandle>, u: LList) ensures LmapIter(n, f, h(f, u)) == LmapIter(n, f, Iterates(f, u)); { calc { @@ -146,7 +146,7 @@ comethod BisimulationLemma(n: nat, f: FunctionHandle>, u: LList) } } -ghost method Example7(f: FunctionHandle>) +lemma Example7(f: FunctionHandle>) // Given the definition of h, prove h(f, _) == Iterates(f, _): ensures forall M :: h(f, M) == Iterates(f, M); { @@ -157,13 +157,13 @@ ghost method Example7(f: FunctionHandle>) // ---------- Section 8.5 ---------- -comethod Example8(f: FunctionHandle, M: LList, N: LList) +colemma Example8(f: FunctionHandle, M: LList, N: LList) ensures Lmap(f, Lappend(M, N)) == Lappend(Lmap(f, M), Lmap(f, N)); { // A proof doesn't get any simpler than this } -comethod Associativity(a: LList, b: LList, c: LList) +colemma Associativity(a: LList, b: LList, c: LList) ensures Lappend(Lappend(a, b), c) == Lappend(a, Lappend(b, c)); { // Again, Dafny does this proof completely automatically diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy index cc92a6f1..b5b0c8bf 100644 --- a/Test/dafny3/SimpleCoinduction.dfy +++ b/Test/dafny3/SimpleCoinduction.dfy @@ -18,7 +18,7 @@ function Inc(s: Stream): Stream Cons(s.head + 1, Inc(s.tail)) } -ghost method {:induction false} UpLemma(k: nat, n: int) +lemma {:induction false} UpLemma(k: nat, n: int) ensures Inc(Up(n)) ==#[k] Up(n+1); { if (k != 0) { @@ -26,18 +26,18 @@ ghost method {:induction false} UpLemma(k: nat, n: int) } } -comethod {:induction false} CoUpLemma(n: int) +colemma {:induction false} CoUpLemma(n: int) ensures Inc(Up(n)) == Up(n+1); { CoUpLemma(n+1); } -ghost method UpLemma_Auto(k: nat, n: int) +lemma UpLemma_Auto(k: nat, n: int) ensures Inc(Up(n)) ==#[k] Up(n+1); { } -comethod CoUpLemma_Auto(n: int) +colemma CoUpLemma_Auto(n: int) ensures Inc(Up(n)) == Up(n+1); { } @@ -49,7 +49,7 @@ function Repeat(n: int): Stream Cons(n, Repeat(n)) } -comethod RepeatLemma(n: int) +colemma RepeatLemma(n: int) ensures Inc(Repeat(n)) == Repeat(n+1); { } @@ -61,7 +61,7 @@ copredicate True(s: Stream) True(s.tail) } -comethod AlwaysTrue(s: Stream) +colemma AlwaysTrue(s: Stream) ensures True(s); { } @@ -71,7 +71,7 @@ copredicate AlsoTrue(s: Stream) AlsoTrue(s) } -comethod AlsoAlwaysTrue(s: Stream) +colemma AlsoAlwaysTrue(s: Stream) ensures AlsoTrue(s); { } @@ -81,7 +81,7 @@ copredicate TT(y: int) TT(y+1) } -comethod AlwaysTT(y: int) +colemma AlwaysTT(y: int) ensures TT(y); { } @@ -112,12 +112,12 @@ copredicate AtMost(a: IList, b: IList) case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail) } -comethod ZerosAndOnes_Theorem0() +colemma ZerosAndOnes_Theorem0() ensures AtMost(zeros(), ones()); { } -comethod ZerosAndOnes_Theorem1() +colemma ZerosAndOnes_Theorem1() ensures Append(zeros(), ones()) == zeros(); { } diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy index f13c5c0a..1d566545 100644 --- a/Test/dafny3/Streams.dfy +++ b/Test/dafny3/Streams.dfy @@ -40,7 +40,7 @@ function map_fg(M: Stream): Stream // ----- Theorems // map (f * g) M = map f (map g M) -comethod Theorem0(M: Stream) +colemma Theorem0(M: Stream) ensures map_fg(M) == map_f(map_g(M)); { match (M) { @@ -49,21 +49,21 @@ comethod Theorem0(M: Stream) Theorem0(N); } } -comethod Theorem0_Alt(M: Stream) +colemma Theorem0_Alt(M: Stream) ensures map_fg(M) == map_f(map_g(M)); { if (M.Cons?) { Theorem0_Alt(M.tail); } } -ghost method Theorem0_Par(M: Stream) +lemma Theorem0_Par(M: Stream) ensures map_fg(M) == map_f(map_g(M)); { forall k: nat { Theorem0_Ind(k, M); } } -ghost method Theorem0_Ind(k: nat, M: Stream) +lemma Theorem0_Ind(k: nat, M: Stream) ensures map_fg(M) ==#[k] map_f(map_g(M)); { if (k != 0) { @@ -74,13 +74,13 @@ ghost method Theorem0_Ind(k: nat, M: Stream) } } } -ghost method Theorem0_AutoInd(k: nat, M: Stream) +lemma Theorem0_AutoInd(k: nat, M: Stream) ensures map_fg(M) ==#[k] map_f(map_g(M)); // { // TODO: this is not working yet, apparently // } // map f (append M N) = append (map f M) (map f N) -comethod Theorem1(M: Stream, N: Stream) +colemma Theorem1(M: Stream, N: Stream) ensures map_f(append(M, N)) == append(map_f(M), map_f(N)); { match (M) { @@ -89,21 +89,21 @@ comethod Theorem1(M: Stream, N: Stream) Theorem1(M', N); } } -comethod Theorem1_Alt(M: Stream, N: Stream) +colemma Theorem1_Alt(M: Stream, N: Stream) ensures map_f(append(M, N)) == append(map_f(M), map_f(N)); { if (M.Cons?) { Theorem1_Alt(M.tail, N); } } -ghost method Theorem1_Par(M: Stream, N: Stream) +lemma Theorem1_Par(M: Stream, N: Stream) ensures map_f(append(M, N)) == append(map_f(M), map_f(N)); { forall k: nat { Theorem1_Ind(k, M, N); } } -ghost method Theorem1_Ind(k: nat, M: Stream, N: Stream) +lemma Theorem1_Ind(k: nat, M: Stream, N: Stream) ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N)); { // this time, try doing the 'if' inside the 'match' (instead of the other way around) @@ -115,24 +115,24 @@ ghost method Theorem1_Ind(k: nat, M: Stream, N: Stream) } } } -ghost method Theorem1_AutoInd(k: nat, M: Stream, N: Stream) +lemma Theorem1_AutoInd(k: nat, M: Stream, N: Stream) ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N)); // { // TODO: this is not working yet, apparently // } -ghost method Theorem1_AutoForall() +lemma Theorem1_AutoForall() { // assert forall k: nat, M, N :: map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N)); // TODO: this is not working yet, apparently } // append NIL M = M -ghost method Theorem2(M: Stream) +lemma Theorem2(M: Stream) ensures append(Nil, M) == M; { // trivial } // append M NIL = M -comethod Theorem3(M: Stream) +colemma Theorem3(M: Stream) ensures append(M, Nil) == M; { match (M) { @@ -141,7 +141,7 @@ comethod Theorem3(M: Stream) Theorem3(N); } } -comethod Theorem3_Alt(M: Stream) +colemma Theorem3_Alt(M: Stream) ensures append(M, Nil) == M; { if (M.Cons?) { @@ -150,7 +150,7 @@ comethod Theorem3_Alt(M: Stream) } // append M (append N P) = append (append M N) P -comethod Theorem4(M: Stream, N: Stream, P: Stream) +colemma Theorem4(M: Stream, N: Stream, P: Stream) ensures append(M, append(N, P)) == append(append(M, N), P); { match (M) { @@ -159,7 +159,7 @@ comethod Theorem4(M: Stream, N: Stream, P: Stream) Theorem4(M', N, P); } } -comethod Theorem4_Alt(M: Stream, N: Stream, P: Stream) +colemma Theorem4_Alt(M: Stream, N: Stream, P: Stream) ensures append(M, append(N, P)) == append(append(M, N), P); { if (M.Cons?) { @@ -241,7 +241,7 @@ function Prepend(x: T, M: Stream): Stream case Cons(s, N) => Cons(Cons(x, s), Prepend(x, N)) } -comethod Prepend_Lemma(x: T, M: Stream) +colemma Prepend_Lemma(x: T, M: Stream) ensures StreamOfNonEmpties(Prepend(x, M)); { match M { @@ -250,7 +250,7 @@ comethod Prepend_Lemma(x: T, M: Stream) } } -ghost method Theorem_Flatten(M: Stream, startMarker: T) +lemma Theorem_Flatten(M: Stream, startMarker: T) ensures StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma; // but until (co-)method can be called from functions, @@ -261,7 +261,7 @@ ghost method Theorem_Flatten(M: Stream, startMarker: T) Lemma_Flatten(Nil, M, startMarker); } -comethod Lemma_Flatten(prefix: Stream, M: Stream, startMarker: T) +colemma Lemma_Flatten(prefix: Stream, M: Stream, startMarker: T) ensures StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma; // but until (co-)method can be called from functions, @@ -325,7 +325,7 @@ comethod Lemma_Flatten(prefix: Stream, M: Stream, startMarker: T) } } -comethod Lemma_FlattenAppend0(s: Stream, M: Stream, startMarker: T) +colemma Lemma_FlattenAppend0(s: Stream, M: Stream, startMarker: T) ensures PrependThenFlattenStartMarker(s, M, startMarker) == append(s, PrependThenFlattenStartMarker(Nil, M, startMarker)); { match (s) { @@ -335,7 +335,7 @@ comethod Lemma_FlattenAppend0(s: Stream, M: Stream, startMarker: T) } } -comethod Lemma_FlattenAppend1(s: Stream, M: Stream) +colemma Lemma_FlattenAppend1(s: Stream, M: Stream) requires StreamOfNonEmpties(M); ensures PrependThenFlattenNonEmpties(s, M) == append(s, PrependThenFlattenNonEmpties(Nil, M)); { diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy index e381726e..3fa99256 100644 --- a/Test/dafny3/WideTrees.dfy +++ b/Test/dafny3/WideTrees.dfy @@ -36,12 +36,12 @@ function SmallTrees(n: nat): Stream if n == 0 then SNil else SCons(SmallTree(n-1), SmallTrees(n)) } // prove that the tree returned by SmallTree is finite -ghost method Theorem(n: nat) +lemma Theorem(n: nat) ensures HasBoundedHeight(SmallTree(n)); { Lemma(n); } -comethod Lemma(n: nat) +colemma Lemma(n: nat) ensures LowerThan(SmallTrees(n), n); { if 0 < n { diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy index 80e8cd91..629861f9 100644 --- a/Test/dafny3/Zip.dfy +++ b/Test/dafny3/Zip.dfy @@ -23,11 +23,11 @@ function even(xs: Stream): Stream function odd(xs: Stream): Stream { even(xs.tl) } -comethod EvenOddLemma(xs: Stream) +colemma EvenOddLemma(xs: Stream) ensures zip(even(xs), odd(xs)) == xs; { EvenOddLemma(xs.tl.tl); } -comethod EvenZipLemma(xs:Stream, ys:Stream) +colemma EvenZipLemma(xs:Stream, ys:Stream) ensures even(zip(xs, ys)) == xs; { /* Automatic. */ } @@ -35,7 +35,7 @@ function bzip(xs: Stream, ys: Stream, f:bool) : Stream { if f then Cons(xs.hd, bzip(xs.tl, ys, !f)) else Cons(ys.hd, bzip(xs, ys.tl, !f)) } -comethod BzipZipLemma(xs:Stream, ys:Stream) +colemma BzipZipLemma(xs:Stream, ys:Stream) ensures zip(xs, ys) == bzip(xs, ys, true); { BzipZipLemma(xs.tl, ys.tl); } @@ -54,7 +54,7 @@ function blink(): Stream Cons(0, Cons(1, blink())) } -comethod BzipBlinkLemma() +colemma BzipBlinkLemma() ensures zip(const(0), const(1)) == blink(); { BzipBlinkLemma(); @@ -66,13 +66,13 @@ function zip2(xs: Stream, ys: Stream): Stream Cons(xs.hd, zip2(ys, xs.tl)) } -comethod Zip201Lemma() +colemma Zip201Lemma() ensures zip2(const(0), const(1)) == blink(); { Zip201Lemma(); } -comethod ZipZip2Lemma(xs:Stream, ys:Stream) +colemma ZipZip2Lemma(xs:Stream, ys:Stream) ensures zip(xs, ys) == zip2(xs, ys); { ZipZip2Lemma(xs.tl, ys.tl); @@ -84,13 +84,13 @@ function bswitch(xs: Stream, f:bool) : Stream else Cons(xs.hd, bswitch(xs.tl, !f)) } -comethod BswitchLemma(xs:Stream) +colemma BswitchLemma(xs:Stream) ensures zip(odd(xs), even(xs)) == bswitch(xs, true); { BswitchLemma(xs.tl.tl); } -comethod Bswitch2Lemma(xs:Stream, ys:Stream) +colemma Bswitch2Lemma(xs:Stream, ys:Stream) ensures zip(xs, ys) == bswitch(zip(ys, xs), true); { Bswitch2Lemma(xs.tl, ys.tl); diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index c77fed74..d663665b 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -32,7 +32,7 @@ `(,(dafny-regexp-opt '( "class" "datatype" "codatatype" "type" "iterator" "function" "predicate" "copredicate" - "ghost" "var" "method" "lemma" "constructor" "comethod" "colemma" + "ghost" "var" "method" "lemma" "constructor" "colemma" "abstract" "module" "import" "default" "as" "opened" "static" "refines" "returns" "yields" "requires" "ensures" "modifies" "reads" "free" "invariant" "decreases" "include" diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index fe7c6638..d8ec579a 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -17,7 +17,7 @@ namespace Demo StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String"); this.MarkReservedWords( // NOTE: these keywords must also appear once more below - "class", "ghost", "static", "var", "method", "constructor", "comethod", "datatype", "codatatype", + "class", "ghost", "static", "var", "method", "constructor", "colemma", "datatype", "codatatype", "iterator", "type", "assert", "assume", "new", "this", "object", "refines", "abstract", "module", "import", "as", "default", "opened", @@ -267,7 +267,7 @@ namespace Demo | "var" | "method" | "constructor" - | "comethod" + | "colemma" | "datatype" | "codatatype" | "type" diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index d4624def..41e0779b 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -9,7 +9,7 @@ bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map, function,predicate,copredicate, ghost,var,static,refines, - method,lemma,constructor,comethod,colemma, + method,lemma,constructor,colemma, returns,yields,abstract,module,import,default,opened,as,in, requires,modifies,ensures,reads,decreases,free,include % expressions diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index 06e1252e..f533a621 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -6,7 +6,7 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate -syntax keyword method lemma constructor comethod colemma +syntax keyword method lemma constructor colemma syntax keyword dafnyTypeDef class datatype codatatype type iterator syntax keyword abstract module import opened as default syntax keyword dafnyConditional if then else match case -- cgit v1.2.3