From 42e7b5c7b4651aca44689bf8412094693bf5e056 Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Wed, 14 Jul 2010 01:10:29 +0000
Subject: Dafny: added comments for refinements assertions.

---
 Dafny/Translator.ssc | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index dcd1b60f..e80f546b 100644
--- a/Dafny/Translator.ssc
+++ b/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;
-- 
cgit v1.2.3