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

3 files changed, 8 insertions, 8 deletions

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);

   }

 }