3 files changed, 29 insertions, 17 deletions
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index ff88c67f..48b1beaf 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1763,7 +1763,9 @@ namespace Microsoft.Dafny {
         Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, that, predef.RefType), predef.Null),
         etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, that, predef.RefType), Resolver.GetThisType(m.tok, m.EnclosingClass)));
       Bpl.Formal thatVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, that, predef.RefType, wh), true);
-      proc.InParams.Add(thatVar);      
+      proc.InParams.Add(thatVar);   
+      
+      // add outs of m to the outs of the refinement procedure   
       foreach (Formal p in m.Outs) {
         Bpl.Type varType = TrType(p.Type);
         Bpl.Expr w = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
@@ -1825,6 +1827,16 @@ namespace Microsoft.Dafny {
       TrStmt(r.Body, builder, localVariables, etran);
       currentMethod = null;
       
+      //  assert output variables of r and m are pairwise equal
+      assert outParams.Length % 2 == 0;
+      int k = outParams.Length / 2;
+      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 I($Heap1, $Heap)      
       builder.Add(new Bpl.AssertCmd(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that)));
                                                 
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3de8e9e9..0f980af2 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -450,4 +450,4 @@ Dafny program verifier finished with 5 verified, 0 errors
 
 -------------------- Refinement.dfy --------------------
 
-Dafny program verifier finished with 54 verified, 0 errors
+Dafny program verifier finished with 53 verified, 0 errors
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index 205f3b6c..c10d86f3 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -18,7 +18,7 @@ class A {
   
   method Test1(p: int) returns (i: int) 
   {   
-    assume true;
+    i := p;
   }
 
   method Test2() returns (o: object)
@@ -51,7 +51,17 @@ class B refines A {
 // Carrol Morgan's calculator
 // 7/2/2010 Kuat
 
+class Util {
+  static function method seqsum(x:seq<int>) : int
+    decreases x;
+  {
+    if (x == []) then 0 else x[0] + seqsum(x[1..])
+  }
+}
+
+
 class ACalc {
+  var util: Util;
   var vals: seq<int>;
   
   method reset() 
@@ -69,21 +79,17 @@ class ACalc {
   method mean() returns (m: int)     
     requires |vals| > 0;
   {
-    m := seqsum(vals)/|vals|;
-  }
-
-  static function method seqsum(x:seq<int>) : int
-    decreases x;
-  {
-    if (x == []) then 0 else x[0] + seqsum(x[1..])
+    m := util.seqsum(vals)/|vals|;
   }
 }
 
 
+
 class CCalc refines ACalc {
+  var util2: Util;
   var sum: int;
   var num: int;
-  replaces vals by sum == seqsum2(vals) && num == |vals|;
+  replaces vals by sum == util2.seqsum(vals) && num == |vals|;
 
   refines reset() 
     modifies this;
@@ -104,12 +110,6 @@ class CCalc refines ACalc {
   {
     m := sum/num;
   }
-
-  static function method seqsum2(x:seq<int>) : int
-    decreases x;
-  {
-    if (x == []) then 0 else x[0] + seqsum2(x[1..])
-  }
 }
 
 // Sequence refined to a singly linked list