Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" statement)

1 files changed, 7 insertions, 7 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 439930b5..d4a0ad9a 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -144,7 +144,7 @@ class Modifies {
   method F(s: set<Modifies>)

     modifies s;

   {

-    foreach (m in s | 2 <= m.x) {

+    parallel (m | m in s && m != null && 2 <= m.x) {

       m.x := m.x + 1;

     }

     if (this in s) {

@@ -157,17 +157,17 @@ class Modifies {
   {

     var m := 3;  // this is a different m

 

-    foreach (m in s | m == this) {

+    parallel (m | m in s && m == this) {

       m.x := m.x + 1;

     }

     if (s <= {this}) {

-      foreach (m in s) {

+      parallel (m | m in s) {

         m.x := m.x + 1;

       }

       F(s);

     }

-    foreach (m in s) {

-      assert m.x < m.x + 10;  // nothing wrong with asserting something

+    parallel (m | m in s) ensures true; { assert m == null || m.x < m.x + 10; }

+    parallel (m | m != null && m in s) {

       m.x := m.x + 1;  // error: may violate modifies clause

     }

   }

@@ -322,10 +322,10 @@ class SomeType
 {

   var x: int;

   method DoIt(stack: seq<SomeType>)

+    requires null !in stack;

     modifies stack;

   {

-    // the following line once gave rise to a crash in the translation

-    foreach (n in stack) {

+    parallel (n | n in stack) {

       n.x := 10;

     }

   }