Dafny: allow signatures to be omitted on refining functions/methods

2 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 6c6b54eb..58cc29fc 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1373,7 +1373,7 @@ RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be rename
 RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')

 RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

 RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

-RefinementErrors.dfy(46,11): Error: body of refining method is not yet supported

+RefinementErrors.dfy(47,4): Error: body of refining method is not yet supported

 RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

 12 resolution/type errors detected in RefinementErrors.dfy

 

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index 280227f1..fc531e23 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -25,7 +25,7 @@ module B refines A {
     }
     method M(x: int) returns (y: int)
       ensures y % 2 == 0;  // add a postcondition
-    method Q() returns (q: int, r: int, s: int)
+    method Q ...
       ensures 12 <= r;
       ensures 1200 <= s;  // error: postcondition is not established by
                           // inherited method body
@@ -44,7 +44,7 @@ module A_AnonymousClass {
 }
 
 module B_AnonymousClass refines A_AnonymousClass {
-  method Increment(d: int)
+  method Increment...
     ensures x <= old(x) + d;
 }