From a8953bef9bebfaa4afb56a914060360c7453e8b8 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Fri, 31 Jul 2015 16:43:34 -0700
Subject: Allow forall statements in refinements

---
 Test/dafny0/RefinementErrors.dfy | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

(limited to 'Test/dafny0/RefinementErrors.dfy')

diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
index 121b33aa..8d60a8e4 100644
--- a/Test/dafny0/RefinementErrors.dfy
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -59,3 +59,40 @@ module BB refines B {
     { 10 }
   }
 }
+
+module Forall0 {
+  class C {
+    var a: int
+    method M()
+      modifies this
+    {
+    }
+    lemma Lemma(x: int)
+    {
+    }
+  }
+}
+module Forall1 refines Forall0 {
+  class C {
+    var b: int
+    method M...
+    {
+      forall x { Lemma(x); }  // allowed
+      var s := {4};
+      forall x | x in s ensures x == 4 { }  // allowed
+      forall x {  // allowed
+        calc {
+          x in s;
+        ==
+          x == 4;
+        }
+      }
+      forall c | c in {this} {
+        c.b := 17;  // allowed
+      }
+      forall c | c in {this} {
+        c.a := 17;  // error: not allowed to update previously defined field
+      }
+    }
+  }
+}
-- 
cgit v1.2.3