Dafny: allow class-member declarations at top level of any module (not just the default module); these go into the (new) default class of each module

1 files changed, 30 insertions, 0 deletions

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index fb379c33..2cfbf19a 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -33,6 +33,36 @@ module B refines A {
 }
 
 // ------------------------------------------------
+
+module A_AnonymousClass {
+  var x: int;
+  method Increment(d: int)
+    modifies this;
+  {
+    x := x + d;
+  }
+}
+
+module B_AnonymousClass refines A_AnonymousClass {
+  method Increment(d: int)
+    ensures x <= old(x) + d;
+}
+
+module C_AnonymousClass refines B_AnonymousClass {
+  method Increment(d: int)
+    ensures old(x) + d <= x;
+  method Main()
+    modifies this;
+  {
+    x := 25;
+    Increment(30);
+    assert x == 55;
+    Increment(12);
+    assert x == 66;  // error: it's 67
+  }
+}
+
+// ------------------------------------------------
 /*  SOON
 module Abstract {
   class MyNumber {