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, 14 insertions, 18 deletions

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 2583ef19..334b3842 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -79,27 +79,23 @@ module Tight refines Loose {
 }

 

 module UnawareClient imports Loose {

-  class Client {

-    method Main() {

-      var n := new MyNumber.Init();

-      assert n.N == 0;  // error: this is not known

-      n.Inc();

-      n.Inc();

-      var k := n.Get();

-      assert k == 4;  // error: this is not known

-    }

+  method Main() {

+    var n := new MyNumber.Init();

+    assert n.N == 0;  // error: this is not known

+    n.Inc();

+    n.Inc();

+    var k := n.Get();

+    assert k == 4;  // error: this is not known

   }

 }

 

 module AwareClient imports Tight {

-  class Client {

-    method Main() {

-      var n := new MyNumber.Init();

-      assert n.N == 0;

-      n.Inc();

-      n.Inc();

-      var k := n.Get();

-      assert k == 4;

-    }

+  method Main() {

+    var n := new MyNumber.Init();

+    assert n.N == 0;

+    n.Inc();

+    n.Inc();

+    var k := n.Get();

+    assert k == 4;

   }

 }