summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar kyessenov <unknown>2010-07-14 01:10:29 +0000
committerGravatar kyessenov <unknown>2010-07-14 01:10:29 +0000
commit3a84a2bd812728ae120b8f8b69be183f5ba72f98 (patch)
treec54740cffd509889dc034326b561c96186880b13
parentb2b89f7c880f7b3c432fee81cafd0d11bfc36982 (diff)
Dafny: added comments for refinements assertions.
-rw-r--r--Source/Dafny/Translator.ssc15
1 files changed, 9 insertions, 6 deletions
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index dcd1b60f..e80f546b 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1738,6 +1738,7 @@ namespace Microsoft.Dafny {
void AddMethodRefinement(MethodRefinement! m)
requires sink != null && predef != null;
{
+ // r is abstract, m is concrete
Method r = m.Refined;
assert r != null;
assert m.EnclosingClass != null;
@@ -1748,7 +1749,7 @@ namespace Microsoft.Dafny {
ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);
// TODO: this straight inlining does not handle recursive calls
- // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure
+ // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames
// generate procedure declaration with pre-condition wp(r, true)
Bpl.Procedure! proc = AddMethod(r, false, true);
@@ -1792,7 +1793,7 @@ namespace Microsoft.Dafny {
Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, Bpl.Expr.True);
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));
- // assume I($Heap, $Heap)
+ // assume I($Heap, $Heap)
builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));
// assign input formals of m (except "this")
@@ -1840,12 +1841,14 @@ namespace Microsoft.Dafny {
for (int i = 0; i < k; i++) {
Bpl.Variable rOut = outParams[i];
Bpl.Variable mOut = outParams[i+k];
- assert rOut != null && mOut != null;
- builder.Add(new Bpl.AssertCmd(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut))));
+ assert rOut != null && mOut != null;
+ builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)),
+ "Refinement method may not produce the same value for output variable " + m.Outs[i].Name));
}
// assert I($Heap1, $Heap)
- builder.Add(new Bpl.AssertCmd(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that)));
+ builder.Add(Assert(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that),
+ "Refinement method may not preserve the coupling invariant"));
Bpl.StmtList stmts = builder.Collect(m.tok);
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
@@ -2866,7 +2869,7 @@ namespace Microsoft.Dafny {
void AddComment(Bpl.StmtListBuilder! builder, Statement! stmt, string! comment) {
builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));
- }
+ }
Bpl.Expr GetWhereClause(IToken! tok, Bpl.Expr! x, Type! type, ExpressionTranslator! etran)
requires predef != null;