Dafny: support input/output parameters in refined methods.

2 files changed, 10 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 2577557a..15986246 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -450,4 +450,4 @@ Dafny program verifier finished with 5 verified, 0 errors
 

 -------------------- Counter.dfy --------------------

 

-Dafny program verifier finished with 19 verified, 0 errors

+Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/dafny0/Counter.dfy b/Test/dafny0/Counter.dfy
index c38b28dc..63f2fc3c 100644
--- a/Test/dafny0/Counter.dfy
+++ b/Test/dafny0/Counter.dfy
@@ -15,8 +15,10 @@ class A {
     requires n > 0; 
   { n := n - 1;}  
   
-  method Test1() returns (i: int) 
-  { i := 0;}
+  method Test1(p: int) returns (i: int) 
+  {   
+    assume true;
+  }
 
   method Test2() returns (o: object)
   { o := this; }
@@ -38,6 +40,11 @@ class B refines A {
     modifies this;
     requires inc > dec; 
   { dec := dec + 1; }
+
+  refines Test1(p: int) returns (i: int) 
+  {
+    i := p;
+  }
 }