From 494e09b9a1fe9aaddb816ce7fd31bfe7cdbebfb2 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 18 Jan 2012 01:48:13 -0800 Subject: Dafny: allow a refinement to provide a function/method body if the function/method being refined didn't have one --- Dafny/DafnyAst.cs | 1 + Dafny/RefinementTransformer.cs | 112 ++++++++++++++++++++++++----------------- Test/dafny0/Answer | 11 +++- Test/dafny0/Refinement.dfy | 11 ++-- 4 files changed, 82 insertions(+), 53 deletions(-) diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 58dcc262..b410b37d 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -2047,6 +2047,7 @@ namespace Microsoft.Dafny { public class LiteralExpr : Expression { public readonly object Value; + [Pure] public static bool IsTrue(Expression e) { Contract.Requires(e != null); if (e is LiteralExpr) { diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index 21bca5d2..d47b1f11 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -120,7 +120,11 @@ namespace Microsoft.Dafny { } IToken Tok(IToken tok) { - return new RefinementToken(tok, moduleUnderConstruction); + if (moduleUnderConstruction == null) { + return tok; + } else { + return new RefinementToken(tok, moduleUnderConstruction); + } } // -------------------------------------------------- Cloning --------------------------------------------------------------- @@ -164,29 +168,10 @@ namespace Microsoft.Dafny { return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null); } else if (member is Function) { var f = (Function)member; - return CloneFunction(f, f.IsGhost, null, null); + return CloneFunction(f, f.IsGhost, null, null, null); } else { var m = (Method)member; - return CloneMethod(m, CloneBlockStmt(m.Body)); - } - } - - Method CloneMethod(Method m, BlockStmt body) { - Contract.Requires(m != null); - Contract.Requires(body != null); - - var tps = m.TypeArgs.ConvertAll(CloneTypeParam); - var ins = m.Ins.ConvertAll(CloneFormal); - var req = m.Req.ConvertAll(CloneMayBeFreeExpr); - var mod = CloneSpecFrameExpr(m.Mod); - var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr); - var decreases = CloneSpecExpr(m.Decreases); - if (m is Constructor) { - return new Constructor(Tok(m.tok), m.Name, tps, ins, - req, mod, ens, decreases, body, null); - } else { - return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal), - req, mod, ens, decreases, body, null); + return CloneMethod(m, null, null); } } @@ -517,25 +502,35 @@ namespace Microsoft.Dafny { return new GuardedAlternative(Tok(alt.Tok), CloneExpr(alt.Guard), alt.Body.ConvertAll(CloneStmt)); } - Function CloneFunction(Function f, bool isGhost, List moreEnsures, Expression moreBody) { + Function CloneFunction(Function f, bool isGhost, List moreEnsures, Expression moreBody, Expression replacementBody) { Contract.Requires(moreBody == null || f is Predicate); + Contract.Requires(moreBody == null || replacementBody == null); var tps = f.TypeArgs.ConvertAll(CloneTypeParam); var formals = f.Formals.ConvertAll(CloneFormal); var req = f.Req.ConvertAll(CloneExpr); var reads = f.Reads.ConvertAll(CloneFrameExpr); + var decreases = CloneSpecExpr(f.Decreases); + + var previousModuleUnderConstruction = moduleUnderConstruction; + if (moreBody != null || replacementBody != null) { moduleUnderConstruction = null; } var ens = f.Ens.ConvertAll(CloneExpr); + moduleUnderConstruction = previousModuleUnderConstruction; if (moreEnsures != null) { ens.AddRange(moreEnsures); } - var decreases = CloneSpecExpr(f.Decreases); - var body = CloneExpr(f.Body); - if (moreBody != null) { - if (body == null) { + + Expression body; + if (replacementBody != null) { + body = replacementBody; + } else if (moreBody != null) { + if (f.Body == null) { body = moreBody; } else { - body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, body, moreBody); + body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, CloneExpr(f.Body), moreBody); } + } else { + body = CloneExpr(f.Body); } if (f is Predicate) { @@ -547,6 +542,33 @@ namespace Microsoft.Dafny { } } + Method CloneMethod(Method m, List moreEnsures, BlockStmt replacementBody) { + Contract.Requires(m != null); + + var tps = m.TypeArgs.ConvertAll(CloneTypeParam); + var ins = m.Ins.ConvertAll(CloneFormal); + var req = m.Req.ConvertAll(CloneMayBeFreeExpr); + var mod = CloneSpecFrameExpr(m.Mod); + var decreases = CloneSpecExpr(m.Decreases); + + var previousModuleUnderConstruction = moduleUnderConstruction; + if (replacementBody != null) { moduleUnderConstruction = null; } + var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr); + if (replacementBody != null) { moduleUnderConstruction = previousModuleUnderConstruction; } + if (moreEnsures != null) { + ens.AddRange(moreEnsures); + } + + var body = replacementBody ?? CloneBlockStmt(m.Body); + if (m is Constructor) { + return new Constructor(Tok(m.tok), m.Name, tps, ins, + req, mod, ens, decreases, body, null); + } else { + return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal), + req, mod, ens, decreases, body, null); + } + } + // -------------------------------------------------- Merging --------------------------------------------------------------- ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) { @@ -603,17 +625,17 @@ namespace Microsoft.Dafny { if (!TypesAreEqual(prevFunction.ResultType, f.ResultType)) { reporter.Error(f, "the result type of function '{0}' ({1}) differs from the result type of the corresponding function in the module it refines ({2})", f.Name, f.ResultType, prevFunction.ResultType); } - - var newBody = f.Body; - if (newBody != null) { - if (prevFunction.Body == null || isPredicate) { - // cool - } else { - reporter.Error(nwMember, "a refining function is not allowed to extend/change the body"); - newBody = null; - } + + Expression moreBody = null; + Expression replacementBody = null; + if (isPredicate) { + moreBody = f.Body; + } else if (prevFunction.Body == null) { + replacementBody = f.Body; + } else if (f.Body != null) { + reporter.Error(nwMember, "a refining function is not allowed to extend/change the body"); } - nw.Members[index] = CloneFunction(prevFunction, f.IsGhost, f.Ens, newBody); + nw.Members[index] = CloneFunction(prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody); } } else { @@ -644,20 +666,16 @@ namespace Microsoft.Dafny { CheckAgreement_Parameters(m.tok, prevMethod.Ins, m.Ins, m.Name, "method", "in-parameter"); CheckAgreement_Parameters(m.tok, prevMethod.Outs, m.Outs, m.Name, "method", "out-parameter"); - var newBody = m.Body; - if (newBody != null) { + var replacementBody = m.Body; + if (replacementBody != null) { if (prevMethod.Body == null) { // cool } else { - reporter.Error(m, "body of refining method is not yet supported"); // TODO - newBody = null; + reporter.Error(m, "body of refining method is not yet supported"); // TODO (merge the new body into the old) + replacementBody = null; } } - var clone = CloneMethod(prevMethod, newBody ?? CloneBlockStmt(prevMethod.Body)); - foreach (var e in m.Ens) { - clone.Ens.Add(e); - } - nw.Members[index] = clone; + nw.Members[index] = CloneMethod(prevMethod, m.Ens, replacementBody); } } } diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 71089e91..57d44098 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1338,11 +1338,18 @@ Execution trace: Refinement.dfy(61,14): Error: assertion violation Execution trace: (0,0): anon0 -Refinement.dfy(70,17): Error: assertion violation +Refinement.dfy(71,17): Error: assertion violation +Execution trace: + (0,0): anon0 +Refinement.dfy(69,15): Error: possible violation of function postcondition +Execution trace: + (0,0): anon3_Else +Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this return path. +Refinement.dfy(74,15): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 -Dafny program verifier finished with 29 verified, 4 errors +Dafny program verifier finished with 28 verified, 6 errors -------------------- RefinementErrors.dfy -------------------- RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index 96fe056f..d99ffdc9 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -66,6 +66,7 @@ module C_AnonymousClass refines B_AnonymousClass { module BodyFree { function F(x: int): int + ensures 0 <= F(x); method TestF() { assert F(6) == F(7); // error: no information about F so far } @@ -86,10 +87,12 @@ module SomeBody refines BodyFree { } module FullBodied refines BodyFree { -//SOON: method M() returns (a: int, b: int) -// { // error: does not establish postcondition -// a := b + 1; -// } + function F(x: int): int + { x } // error: does not meet the inherited postcondition (note, confusing error-message location) + method M() returns (a: int, b: int) + { // error: does not establish postcondition + a := b + 1; + } } // ------------------------------------------------ -- cgit v1.2.3