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

5 files changed, 8 insertions, 8 deletions

diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 26e57c7f..2f8c2a9e 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -75,7 +75,7 @@ ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream,
 ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

 {

-  parallel (k:nat) { SAppendIsAssociativeK(k, a, b, c); }

+  forall k:nat { SAppendIsAssociativeK(k, a, b, c); }

   // assert for clarity only, postcondition follows directly from it

   assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c)));

 }

diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy
index 3af868ca..c5e8f3a3 100644
--- a/Test/dafny3/Iter.dfy
+++ b/Test/dafny3/Iter.dfy
@@ -32,7 +32,7 @@ class List<T> {
   {

     if (n == a.Length) {

       var b := new T[2 * a.Length];

-      parallel (i | 0 <= i < a.Length) {

+      forall i | 0 <= i < a.Length {

         b[i] := a[i];

       }

       assert b[..n] == a[..n] == Contents;

diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 5331b808..700b531c 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -22,7 +22,7 @@ ghost method FibLemma(n: nat)
 }

 

 /*

-  The 'parallel' statement has the effect of applying its body simultaneously

+  The 'forall' statement has the effect of applying its body simultaneously

   to all values of the bound variables---in the first example, to all k

   satisfying 0 <= k < n, and in the second example, to all non-negative n. 

 */

@@ -30,7 +30,7 @@ ghost method FibLemma(n: nat)
 ghost method FibLemma_Alternative(n: nat)

   ensures Fib(n) % 2 == 0 <==> n % 3 == 0;

 {

-  parallel (k | 0 <= k < n) {

+  forall k | 0 <= k < n {

     FibLemma_Alternative(k);

   }

 }

@@ -38,7 +38,7 @@ ghost method FibLemma_Alternative(n: nat)
 ghost method FibLemma_All()

   ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);

 {

-  parallel (n | 0 <= n) {

+  forall n | 0 <= n {

     FibLemma(n);

   }

 }

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index 757d6a37..1198c7e0 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -59,7 +59,7 @@ comethod Theorem0_Alt(M: Stream<X>)
 ghost method Theorem0_Par(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

-  parallel (k: nat) {

+  forall k: nat {

     Theorem0_Ind(k, M);

   }

 }

@@ -99,7 +99,7 @@ comethod Theorem1_Alt(M: Stream<X>, N: Stream<X>)
 ghost method Theorem1_Par(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

-  parallel (k: nat) {

+  forall k: nat {

     Theorem1_Ind(k, M, N);

   }

 }

diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 371b012a..80e8cd91 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -8,7 +8,7 @@ properties, drawing from:
 Some proofs are automatic (EvenZipLemma), whereas some others require a single

 recursive call to be made explicitly.

 

-Note that the automatically inserted parallel statement

+Note that the automatically inserted forall statement

 is in principle strong enough in all cases above, but the incompletness

 of reasoning with quantifiers in SMT solvers make the explicit calls

 necessary.