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

3 files changed, 50 insertions, 21 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8e4c2f12..27c97dc2 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1301,8 +1301,11 @@ Refinement.dfy[B](12,5): Error BP5003: A postcondition might not hold on this re
 Refinement.dfy(30,20): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

+Refinement.dfy(61,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 8 verified, 2 errors

+Dafny program verifier finished with 15 verified, 3 errors

 

 -------------------- RefinementErrors.dfy --------------------

 RefinementErrors.dfy(13,11): Error: a refining method is not allowed to extend the modifies clause

@@ -1370,10 +1373,10 @@ Predicates.dfy[B](17,15): Related location: This is the postcondition that might
 Predicates.dfy(28,9): Related location: Related location

 Execution trace:

     (0,0): anon0

-Predicates.dfy(85,18): Error: assertion violation

+Predicates.dfy(84,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Predicates.dfy(89,16): Error: assertion violation

+Predicates.dfy(88,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

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;

   }

 }

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 {