diff options
author | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:13:03 -0700 |
---|---|---|
committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:13:03 -0700 |
commit | bef7f2ff0dbe833b157970efa16b12086776ef70 (patch) | |
tree | 78b2b8f6da0f312a72c60e3cfb9dd4ffa9a4e00f /Source | |
parent | 68d57324e25c44f022e55bbc55fffd4e22842928 (diff) |
Dafny: improved checking of inherited postconditions (in refinements)
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 20 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 2 |
2 files changed, 12 insertions, 10 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 6af14b14..60aa1bfd 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -454,7 +454,7 @@ namespace Microsoft.Dafny }
moduleUnderConstruction = null;
}
- Function CloneFunction(IToken tok, Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody) {
+ Function CloneFunction(IToken tok, Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody, bool checkPrevPostconditions) {
Contract.Requires(moreBody == null || f is Predicate);
Contract.Requires(moreBody == null || replacementBody == null);
@@ -465,9 +465,10 @@ namespace Microsoft.Dafny var decreases = refinementCloner.CloneSpecExpr(f.Decreases);
List<Expression> ens;
- if (moreBody != null || replacementBody != null)
+ if (checkPrevPostconditions) // note, if a postcondition includes something that changes in the module, the translator will notice this and still re-check the postcondition
ens = f.Ens.ConvertAll(rawCloner.CloneExpr);
- else ens = f.Ens.ConvertAll(refinementCloner.CloneExpr);
+ else
+ ens = f.Ens.ConvertAll(refinementCloner.CloneExpr);
if (moreEnsures != null) {
ens.AddRange(moreEnsures);
}
@@ -502,7 +503,7 @@ namespace Microsoft.Dafny }
}
- Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, Specification<Expression> decreases, BlockStmt replacementBody) {
+ Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, Specification<Expression> decreases, BlockStmt newBody, bool checkPreviousPostconditions) {
Contract.Requires(m != null);
Contract.Requires(decreases != null);
@@ -512,14 +513,15 @@ namespace Microsoft.Dafny var mod = refinementCloner.CloneSpecFrameExpr(m.Mod);
List<MaybeFreeExpression> ens;
- if (replacementBody != null)
+ if (checkPreviousPostconditions)
ens = m.Ens.ConvertAll(rawCloner.CloneMayBeFreeExpr);
- else ens = m.Ens.ConvertAll(refinementCloner.CloneMayBeFreeExpr);
+ else
+ ens = m.Ens.ConvertAll(refinementCloner.CloneMayBeFreeExpr);
if (moreEnsures != null) {
ens.AddRange(moreEnsures);
}
- var body = replacementBody ?? refinementCloner.CloneBlockStmt(m.Body);
+ var body = newBody ?? refinementCloner.CloneBlockStmt(m.Body);
if (m is Constructor) {
return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,
req, mod, ens, decreases, body, null, false);
@@ -604,7 +606,7 @@ namespace Microsoft.Dafny } else if (f.Body != null) {
reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");
}
- nw.Members[index] = CloneFunction(f.tok, prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody);
+ nw.Members[index] = CloneFunction(f.tok, prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody, prevFunction.Body == null);
}
} else {
@@ -654,7 +656,7 @@ namespace Microsoft.Dafny replacementBody = MergeBlockStmt(replacementBody, prevMethod.Body);
}
}
- nw.Members[index] = CloneMethod(prevMethod, m.Ens, decreases, replacementBody);
+ nw.Members[index] = CloneMethod(prevMethod, m.Ens, decreases, replacementBody, prevMethod.Body == null);
}
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index f2011b72..a090515e 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1609,7 +1609,7 @@ namespace Microsoft.Dafny { var splits = new List<SplitExprInfo>();
bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, etran);
foreach (var s in splits) {
- if (!s.IsFree) {
+ if (!s.IsFree && !RefinementToken.IsInherited(s.E.tok, currentModule)) {
ens.Add(Ensures(s.E.tok, s.IsFree, s.E, null, null));
}
}
|