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

4 files changed, 42 insertions, 65 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 697bdd9e..04d60716 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -173,11 +173,18 @@ SmallTests.dfy(131,9): Error: call may violate context's modifies clause
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(171,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+SmallTests.dfy(171,9): Error: assignment may update an object field not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon3

+    (0,0): anon22_Else

+    (0,0): anon5

+    (0,0): anon24_Else

+    (0,0): anon11

+    (0,0): anon26_Else

+    (0,0): anon16

+    (0,0): anon28_Then

+    (0,0): anon29_Then

+    (0,0): anon19

 SmallTests.dfy(199,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -374,46 +381,37 @@ Execution trace:
     (0,0): anon23_Then

     (0,0): anon24_Then

     (0,0): anon11

-Definedness.dfy(199,24): Error: possible violation of function precondition

+Definedness.dfy(193,19): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-Definedness.dfy(201,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(203,33): Error: range expression must be well defined

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(218,19): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(216,5): anon7_LoopHead

+    Definedness.dfy(191,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(218,23): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(193,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(218,28): Error: possible division by zero

+Definedness.dfy(193,28): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(216,5): anon7_LoopHead

+    Definedness.dfy(191,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(239,46): Error: possible violation of function postcondition

+Definedness.dfy(214,46): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-Definedness.dfy(246,22): Error: target object may be null

+Definedness.dfy(221,22): Error: target object may be null

 Execution trace:

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Definedness.dfy(262,24): Error: possible violation of function postcondition

+Definedness.dfy(237,24): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon7_Then

     (0,0): anon2

     (0,0): anon8_Else

 

-Dafny program verifier finished with 23 verified, 39 errors

+Dafny program verifier finished with 22 verified, 36 errors

 

 -------------------- FunctionSpecifications.dfy --------------------

 FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition

@@ -1128,21 +1126,25 @@ TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this
 TypeAntecedents.dfy(54,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon15_Then

+    (0,0): anon25_Then

     (0,0): anon6

-    (0,0): anon18_Then

+    (0,0): anon28_Then

     (0,0): anon8

-    (0,0): anon19_Then

-    (0,0): anon10

-    (0,0): anon20_Then

-    (0,0): anon21_Then

-    (0,0): anon14

+    (0,0): anon29_Else

+    (0,0): anon13

+    (0,0): anon31_Else

+    (0,0): anon18

+    (0,0): anon33_Then

+    (0,0): anon20

+    (0,0): anon34_Then

+    (0,0): anon35_Then

+    (0,0): anon24

 TypeAntecedents.dfy(63,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon15_Else

-    (0,0): anon16_Then

-    (0,0): anon17_Else

+    (0,0): anon25_Else

+    (0,0): anon26_Then

+    (0,0): anon27_Else

 

 Dafny program verifier finished with 12 verified, 3 errors

 

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 44b54f3d..f99d1503 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -185,31 +185,6 @@ class StatementTwoShoes {
   function G(w: int): int { 5 }

   function method H(x: int): int { -x }

 

-  method V(s: set<StatementTwoShoes>, a: int, b: int)

-    modifies s;

-  {

-

-    foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null

-    {

-      assume 0 <= m.x;

-      assert m.x < 1000;

-

-      m.x := m.x + 1;

-    }

-    foreach (m in s + {F(a)})  // error: collection expression may not be well defined (fn precondition)

-    {

-      m.x := 5;  // error: possible modifies clause violation

-    }

-    foreach (m in s | F(H(m.x)) == this)  // error: range expression may not be well defined

-    {

-      m.x := H(m.x);

-    }

-    foreach (m in s)

-    {

-      m.x := 100 / m.x;  // error: RhS may not be well defined

-    }

-  }

-

   method W(x: int)

   {

     var i := 0;

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;

     }

   }

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 5982a9e6..b6ef0d68 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -68,8 +68,8 @@ method M(list: List, S: set<MyClass>) returns (ret: int)
   ghost var l := NF();

   assert l != null ==> l.H() == 5;

 

-  foreach (s in S) {

-    assert s == null || s.H() == 5;

+  parallel (s | s in S) ensures true; { assert s == null || s.H() == 5; }

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

     s.x := 0;

   }