summaryrefslogtreecommitdiff
path: root/Test/dafny0/Refinement.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Refinement.dfy')
-rw-r--r--Test/dafny0/Refinement.dfy4
1 files changed, 2 insertions, 2 deletions
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;
}