Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional.

1 files changed, 19 insertions, 19 deletions

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index f260edb5..c740f88c 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -13,16 +13,16 @@ class C {
 

 method M0(IS: set<int>)

 {

-  parallel (i | 0 <= i < 20) {

+  forall (i | 0 <= i < 20) {

     i := i + 1;  // error: not allowed to assign to bound variable

   }

 

   var k := 0;

-  parallel (i | 0 <= i < 20) {

-    k := k + i;  // error: not allowed to assign to local k, since k is not declared inside parallel block

+  forall (i | 0 <= i < 20) {

+    k := k + i;  // error: not allowed to assign to local k, since k is not declared inside forall block

   }

 

-  parallel (i | 0 <= i < 20)

+  forall (i | 0 <= i < 20)

     ensures true;

   {

     var x := i;

@@ -31,16 +31,16 @@ method M0(IS: set<int>)
 

   ghost var y;

   var z;

-  parallel (i | 0 <= i)

+  forall (i | 0 <= i)

     ensures true;

   {

     var x := i;

     x := x + 1;

-    y := 18;  // (this statement is not allowed, since y is declared outside the parallel, but that check happens only if the first resolution pass of the parallel statement passes, which it doesn't in this case because of the next line)

-    z := 20;  // error: assigning to a non-ghost variable inside a ghost parallel block

+    y := 18;  // (this statement is not allowed, since y is declared outside the forall, but that check happens only if the first resolution pass of the forall statement passes, which it doesn't in this case because of the next line)

+    z := 20;  // error: assigning to a non-ghost variable inside a ghost forall block

   }

 

-  parallel (i | 0 <= i)

+  forall (i | 0 <= i)

     ensures true;

   {

     ghost var x := i;

@@ -48,15 +48,15 @@ method M0(IS: set<int>)
   }

 

   var ia := new int[20];

-  parallel (i | 0 <= i < 20) {

+  forall (i | 0 <= i < 20) {

     ia[i] := choose IS;  // error: set choose not allowed

   }

 

   var ca := new C[20];

-  parallel (i | 0 <= i < 20) {

+  forall (i | 0 <= i < 20) {

     ca[i] := new C;  // error: new allocation not allowed

   }

-  parallel (i | 0 <= i < 20)

+  forall (i | 0 <= i < 20)

     ensures true;

   {

     var c := new C;  // allowed

@@ -69,27 +69,27 @@ method M0(IS: set<int>)
 }

 

 method M1() {

-  parallel (i | 0 <= i < 20) {

+  forall (i | 0 <= i < 20) {

     assert i < 100;

     if (i == 17) { break; }  // error: nothing to break out of

   }

 

-  parallel (i | 0 <= i < 20) ensures true; {

-    if (i == 8) { return; }  // error: return not allowed inside parallel block

+  forall (i | 0 <= i < 20) ensures true; {

+    if (i == 8) { return; }  // error: return not allowed inside forall block

   }

 

   var m := 0;

   label OutsideLoop:

   while (m < 20) {

-    parallel (i | 0 <= i < 20) {

-      if (i == 17) { break; }  // error: not allowed to break out of loop that sits outside parallel

+    forall (i | 0 <= i < 20) {

+      if (i == 17) { break; }  // error: not allowed to break out of loop that sits outside forall

       if (i == 8) { break break; }  // error: ditto (also: attempt to break too far)

       if (i == 9) { break OutsideLoop; }  // error: ditto

     }

     m := m + 1;

   }

 

-  parallel (i | 0 <= i < 20) {

+  forall (i | 0 <= i < 20) {

     var j := 0;

     while (j < i) {

       if (j == 6) { break; }  // fine

@@ -102,7 +102,7 @@ method M1() {
 

 method M2() {

   var a := new int[100];

-  parallel (x | 0 <= x < 100) {

-    a[x] :| assume a[x] > 0;  // error: not allowed to update heap location in a parallel statement with an assume

+  forall (x | 0 <= x < 100) {

+    a[x] :| assume a[x] > 0;  // error: not allowed to update heap location in a forall statement with an assume

   }

 }