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

18 files changed, 90 insertions, 90 deletions

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index 612b96ba..53d82207 100644
--- a/Test/VSI-Benchmarks/b5.dfy
+++ b/Test/VSI-Benchmarks/b5.dfy
@@ -57,12 +57,12 @@ class Queue<T> {
     tail.next := n;

     tail := n;

 

-    parallel (m | m in spine) {

+    forall m | m in spine {

       m.tailContents := m.tailContents + [t];

     }

     contents := head.tailContents;

 

-    parallel (m | m in spine) {

+    forall m | m in spine {

       m.footprint := m.footprint + n.footprint;

     }

     footprint := footprint + n.footprint;

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index d3cecc28..06692314 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -41,7 +41,7 @@ comethod {:induction false} Theorem0()
 ghost method Theorem0_Manual()

   ensures atmost(zeros(), ones());

 {

-  parallel (k: nat) {

+  forall k: nat {

     Theorem0_Lemma(k);

   }

 }

diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index 43ef4e69..e0c58867 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -208,7 +208,7 @@ iterator DoleOutReferences(u: Cell) yields (r: Cell, c: Cell)
       assert c in _new;  // as is checked here as well

       assert r.data == 12;  // error: it may have changed 

     } else {

-      parallel (z | z in myCells) {

+      forall z | z in myCells {

         z.data := z.data + 1;  // we're allowed to modify these, because they are all in _new

       }

     }

diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
index 11bf4fbe..cd712b7d 100644
--- a/Test/dafny0/LetExpr.dfy
+++ b/Test/dafny0/LetExpr.dfy
@@ -38,7 +38,7 @@ method M3(a: array<int>) returns (r: int)
 

   assert Fib(1000) == 1000;  // does it still know this?

 

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

+  forall i | 0 <= i < a.Length ensures true; {

     var j := i+1;

     assert j < a.Length ==> a[i] == a[j];

   }

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index ac11c1eb..37004441 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -19,23 +19,23 @@ method ParallelStatement_Resolve(
   requires a != null && null !in spine;

   modifies a, spine;

 {

-  parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {

+  forall (i: int | 0 <= i < a.Length && i % 2 == 0) {

     a[i] := a[(i + 1) % a.Length] + 3;

   }

 

-  parallel (o | o in spine) {

+  forall (o | o in spine) {

     o.st := o.st + Repr;

   }

 

-  parallel (x, y | x in S && 0 <= y+x < 100) {

+  forall (x, y | x in S && 0 <= y+x < 100) {

     Lemma(clx, x, y);  // error: precondition does not hold (clx may be null)

   }

 

-  parallel (x, y | x in S && 0 <= y+x < 100) {

+  forall (x, y | x in S && 0 <= y+x < 100) {

     cly.CLemma(x + y);  // error: receiver might be null

   }

 

-  parallel (p | 0 <= p)

+  forall (p | 0 <= p)

     ensures F(p) <= Sum(p) + p - 1;  // error (no connection is known between F and Sum)

   {

     assert 0 <= G(p);

@@ -73,7 +73,7 @@ method M0(S: set<C>)
   ensures forall o :: o in S ==> o.data == 85;

   ensures forall o :: o != null && o !in S ==> o.data == old(o.data);

 {

-  parallel (s | s in S) {

+  forall (s | s in S) {

     s.data := 85;

   }

 }

@@ -81,18 +81,18 @@ method M0(S: set<C>)
 method M1(S: set<C>, x: C)

   requires null !in S && x in S;

 {

-  parallel (s | s in S)

+  forall (s | s in S)

     ensures s.data < 100;

   {

     assume s.data == 85;

   }

   if (*) {

-    assert x.data == 85;  // error (cannot be inferred from parallel ensures clause)

+    assert x.data == 85;  // error (cannot be inferred from forall ensures clause)

   } else {

     assert x.data < 120;

   }

 

-  parallel (s | s in S)

+  forall (s | s in S)

     ensures s.data < 70;  // error

   {

     assume s.data == 85;

@@ -104,10 +104,10 @@ method M2() returns (a: array<int>)
   ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j];

 {

   a := new int[250];

-  parallel (i: nat | i < 125) {

+  forall (i: nat | i < 125) {

     a[i] := 423;

   }

-  parallel (i | 125 <= i < 250) {

+  forall (i | 125 <= i < 250) {

     a[i] := 300 + i;

   }

 }

@@ -115,7 +115,7 @@ method M2() returns (a: array<int>)
 method M4(S: set<C>, k: int)

   modifies S;

 {

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

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

     s.n := k;  // error: k might be negative

   }

 }

@@ -124,25 +124,25 @@ method M5()
 {

   if {

   case true =>

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

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

       PowerLemma(x, x);

     }

     assert Pred(34, 34);

 

   case true =>

-    parallel (x,y | 0 <= x < 100 && y == x+1) {

+    forall (x,y | 0 <= x < 100 && y == x+1) {

       PowerLemma(x, y);

     }

     assert Pred(34, 35);

 

   case true =>

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

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

       PowerLemma(x, y);

     }

     assert Pred(34, 35);

 

   case true =>

-    parallel (x | x in set k | 0 <= k < 100) {

+    forall (x | x in set k | 0 <= k < 100) {

       PowerLemma(x, x);

     }

     assert Pred(34, 34);

@@ -152,17 +152,17 @@ method M5()
 method Main()

 {

   var a := new int[180];

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

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

     a[i] := 2*i + 100;

   }

   var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];

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

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

     a[20+i] := sq[i];

   }

-  parallel (t | t in sq) {

+  forall (t | t in sq) {

     a[t] := 1000;

   }

-  parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {

+  forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) {

     a[u] := 6000 + t;

   }

   var k := 0;

@@ -178,11 +178,11 @@ method DuplicateUpdate() {
   var a := new int[180];

   var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];

   if (*) {

-    parallel (t,u | t in sq && 10 <= u < 10+t) {

+    forall (t,u | t in sq && 10 <= u < 10+t) {

       a[u] := 6000 + t;  // error: a[10] (and a[11]) are assigned more than once

     }

   } else {

-    parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {

+    forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) {

       a[u] := 6000 + t;  // with the 't < 4' conjunct in the line above, this is fine

     }

   }

@@ -193,8 +193,8 @@ ghost method DontDoMuch(x: int)
 }

 

 method OmittedRange() {

-  parallel (x) { }

-  parallel (x) {

+  forall (x) { }

+  forall (x) {

     DontDoMuch(x);

   }

 }

@@ -210,7 +210,7 @@ ghost static method TwoState0(y: int)
 }

 

 method TwoState_Main0() {

-  parallel (x) { TwoState0(x); }

+  forall (x) { TwoState0(x); }

   assert false;  // error: this location is indeed reachable (if the translation before it is sound)

 }

 

@@ -222,7 +222,7 @@ ghost static method TwoState1(y: int)
 }

 

 method TwoState_Main1() {

-  parallel (x) { TwoState1(x); }

+  forall (x) { TwoState1(x); }

   assert false;  // error: this location is indeed reachable (if the translation before it is sound)

 }

 

@@ -231,7 +231,7 @@ method X_Legit(c: TwoState_C)
   modifies c;

 {

   c.data := c.data + 1;

-  parallel (x | c.data <= x)

+  forall (x | c.data <= x)

     ensures old(c.data) < x;  // note that the 'old' refers to the method's initial state

   {

   }

@@ -241,12 +241,12 @@ method X_Legit(c: TwoState_C)
 // ensures clause.

 // However, there's an important difference in the translation, which is that the

 // occurrence of 'fresh' here refers to the initial state of the TwoStateMain2

-// method, not the beginning of the 'parallel' statement.

-// Still, care needs to be taken in the translation to make sure that the parallel

+// method, not the beginning of the 'forall' statement.

+// Still, care needs to be taken in the translation to make sure that the forall

 // statement's effect on the heap is not optimized away.

 method TwoState_Main2()

 {

-  parallel (x: int)

+  forall (x: int)

     ensures exists o: TwoState_C :: o != null && fresh(o);

   {

     TwoState0(x);

@@ -257,12 +257,12 @@ method TwoState_Main2()
 // At first glance, this looks like an inlined version of TwoState_Main0 above.

 // However, there's an important difference in the translation, which is that the

 // occurrence of 'fresh' here refers to the initial state of the TwoStateMain3

-// method, not the beginning of the 'parallel' statement.

-// Still, care needs to be taken in the translation to make sure that the parallel

+// method, not the beginning of the 'forall' statement.

+// Still, care needs to be taken in the translation to make sure that the forall

 // statement's effect on the heap is not optimized away.

 method TwoState_Main3()

 {

-  parallel (x: int)

+  forall (x: int)

     ensures exists o: TwoState_C :: o != null && fresh(o);

   {

     var p := new TwoState_C;

@@ -270,7 +270,7 @@ method TwoState_Main3()
   assert false;  // error: this location is indeed reachable (if the translation before it is sound)

 }

 

-// ------- empty parallel statement -----------------------------------------

+// ------- empty forall statement -----------------------------------------

 

 var emptyPar: int;

 

@@ -278,7 +278,7 @@ method Empty_Parallel0()
   modifies this;

   ensures emptyPar == 8;

 {

-  parallel () {

+  forall () {

     this.emptyPar := 8;

   }

 }

@@ -290,19 +290,19 @@ ghost method EmptyPar_Lemma(x: int)
 method Empty_Parallel1()

   ensures EmptyPar_P(8);

 {

-  parallel () {

+  forall {

     EmptyPar_Lemma(8);

   }

 }

 

 method Empty_Parallel2()

 {

-  parallel ()

+  forall

     ensures exists k :: EmptyPar_P(k);

   {

     var y := 8;

     assume EmptyPar_P(y);

   }

   assert exists k :: EmptyPar_P(k);  // yes

-  assert EmptyPar_P(8);  // error: the parallel statement's ensures clause does not promise this

+  assert EmptyPar_P(8);  // error: the forall statement's ensures clause does not promise this

 }

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

   }

 }

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

     modifies s;

   {

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

+    forall 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

 

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

+    forall m | m in s && m == this {

       m.x := m.x + 1;

     }

     if (s <= {this}) {

-      parallel (m | m in s) {

+      forall (m | m in s) {

         m.x := m.x + 1;

       }

       F(s);

     }

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

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

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

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

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

     }

   }

@@ -304,7 +304,7 @@ class SomeType
     requires null !in stack;

     modifies stack;

   {

-    parallel (n | n in stack) {

+    forall n | n in stack {

       n.x := 10;

     }

   }

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index b6ef0d68..758f5f44 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;

 

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

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

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

+  forall s | s != null && s in S {

     s.x := 0;

   }

 

diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy
index 0edfab81..8396ec5c 100644
--- a/Test/dafny1/Queue.dfy
+++ b/Test/dafny1/Queue.dfy
@@ -85,12 +85,12 @@ class Queue<T> {
     tail.next := n;

     tail := n;

 

-    parallel (m | m in spine) {

+    forall m | m in spine {

       m.tailContents := m.tailContents + [t];

     }

     contents := head.tailContents;

 

-    parallel (m | m in spine) {

+    forall m | m in spine {

       m.footprint := m.footprint + n.footprint;

     }

     footprint := footprint + n.footprint;

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 79803f35..bbfab50d 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -209,7 +209,7 @@ ghost method Window(xs: List, ys: List)
   }

 }

 

-// In the following we use a combination of calc and parallel

+// In the following we use a combination of calc and forall

 

 function ith<a>(xs: List, i: nat): a

   requires i < length(xs);

@@ -253,7 +253,7 @@ ghost method lemma_extensionality(xs: List, ys: List)
             }

             Cons(y, xrest);

             { 

-              parallel (j: nat | j < length(xrest)) {

+              forall (j: nat | j < length(xrest)) {

                 calc {

                   ith(xrest, j);

                   ith(xs, j + 1);

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.

diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index 4373136b..e1a93730 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -85,7 +85,7 @@ class BreadthFirstSearch<Vertex(==)>
       ghost var pathToV := Find(source, v, paths);

     

       if (v == dest) {

-        parallel (p | IsPath(source, dest, p))

+        forall p | IsPath(source, dest, p)

           ensures |pathToV| <= |p|;

         {

           Lemma_IsPath_R(source, dest, p, AllVertices);

@@ -110,7 +110,7 @@ class BreadthFirstSearch<Vertex(==)>
 

     // show that "dest" in not in any reachability set, no matter 

     // how many successors one follows

-    parallel (nn)

+    forall nn

       ensures dest !in R(source, nn, AllVertices);

     {

       if (Value(nn) < Value(dd)) {

@@ -122,7 +122,7 @@ class BreadthFirstSearch<Vertex(==)>
 

     // Now, show what what the above means in terms of IsPath.  More 

     // precisely, show that there is no path "p" from "source" to "dest".

-    parallel (p | IsPath(source, dest, p))

+    forall p | IsPath(source, dest, p)

       // this and the previous two lines will establish the 

       // absurdity of a "p" satisfying IsPath(source, dest, p)

       ensures false;  

@@ -130,7 +130,7 @@ class BreadthFirstSearch<Vertex(==)>
       Lemma_IsPath_R(source, dest, p, AllVertices);

       // a consequence of Lemma_IsPath_R is:  

       // dest in R(source, ToNat(|p|), AllVertices)

-      // but that contradicts the conclusion of the preceding parallel statement

+      // but that contradicts the conclusion of the preceding forall statement

     }

 

     d := -1;  // indicate "no path"

diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
index 46daf48d..dcc2e22d 100644
--- a/Test/vstte2012/Combinators.dfy
+++ b/Test/vstte2012/Combinators.dfy
@@ -225,7 +225,7 @@ ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)
         // that FindAndStep(b) gives C[Step(u)].

         return Apply(t.car, r), value_C(t.car, C), u;

       } else {

-        parallel (C,u | IsContext(C) && t == EvalExpr(C,u))

+        forall C,u | IsContext(C) && t == EvalExpr(C,u)

           ensures Step(u) == u;

         {

           // The following assert and the first assert of each "case" are

@@ -442,7 +442,7 @@ ghost method VerificationTask3()
   ensures forall n: nat ::

     TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);

 {

-  parallel (n: nat) {

+  forall n: nat {

     VT3(n);

   }

 }

diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
index 47ed19a4..1aa06408 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -116,7 +116,7 @@ ghost method lemma1(t: Tree, s:seq<int>)
 ghost method lemma2(s: seq<int>)

   ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?;

 {

-  parallel(t | toList(0,t) == s) {

+  forall t | toList(0,t) == s {

     lemma1(t, s);

   } 

 }

@@ -130,7 +130,7 @@ ghost method lemma2(s: seq<int>)
 ghost method completeness()

   ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?);

 {

-  parallel(s) {

+  forall s {

     lemma2(s);

   }

 }