Dafny: continued translation of "parallel" statements (Assign and Proof forms are mostly there, Call is missing and so is compilation)

Dafny: included some test cases for the "parallel" statement
Dafny: starting changing old "foreach" statements to the new "parallel" statement

5 files changed, 96 insertions, 45 deletions

diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
index cd132ef3..612b96ba 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;

 

-    foreach (m in spine) {

+    parallel (m | m in spine) {

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

     }

     contents := head.tailContents;

 

-    foreach (m in spine) {

+    parallel (m | m in spine) {

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

     }

     footprint := footprint + n.footprint;

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a3e5e11f..4b3d9814 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -947,6 +947,42 @@ Execution trace:
 

 Dafny program verifier finished with 27 verified, 6 errors

 

+-------------------- Parallel.dfy --------------------

+Parallel.dfy(29,18): Error: possible violation of postcondition of parallel statement

+Execution trace:

+    (0,0): anon0

+    (0,0): anon17_Else

+    (0,0): anon7

+    (0,0): anon20_Else

+    (0,0): anon10

+    (0,0): anon21_Then

+    (0,0): anon22_Then

+    (0,0): anon14

+Parallel.dfy(34,19): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon17_Else

+    (0,0): anon7

+    (0,0): anon20_Else

+    (0,0): anon10

+    (0,0): anon21_Then

+    (0,0): anon22_Then

+Parallel.dfy(76,19): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Else

+    (0,0): anon3

+    (0,0): anon11_Then

+Parallel.dfy(82,20): Error: possible violation of postcondition of parallel statement

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Else

+    (0,0): anon3

+    (0,0): anon11_Then

+    (0,0): anon12_Then

+

+Dafny program verifier finished with 12 verified, 4 errors

+

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(44,22): Error: assertion violation

 Execution trace:

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 0928c070..88a67957 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -1,48 +1,16 @@
-/*

-method ParallelStatement_Syntax()

-{

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

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

-  }

-

-  parallel (o | o in spine) {

-    o.f := o.f + Repr;

-  }

-

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

-    Lemma(x, y);

-  }

-

-  parallel (p | 0 <= p)

-    ensures F(p) <= Sum(p) * (p-1) + 100;

-  {

-    assert G(p);

-    ghost var t;

-    if (p % 2 == 0) {

-      assert G(p) == F(p+2);

-      t := p*p;

-    } else {

-      assume H(p, 20) < 100;  // don't know how to justify this

-      t := p;

-    }

-    PowerLemma(p, t);

-    t := t + 1;

-    PowerLemma(p, t);

-  }

-}

-*/

-

 class C {

-  var f: set<object>;

+  var data: int;

+  var st: set<object>;

 }

 

+// This method more or less just tests the syntax, resolution, and basic verification

 method ParallelStatement_Resolve(

     a: array<int>,

     spine: set<C>,

     Repr: set<object>,

     S: set<int>

   )

-  requires a != null;

+  requires a != null && null !in spine;

   modifies a, spine;

 {

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

@@ -50,7 +18,7 @@ method ParallelStatement_Resolve(
   }

 

   parallel (o | o in spine) {

-    o.f := o.f + Repr;

+    o.st := o.st + Repr;

   }

 

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

@@ -58,12 +26,12 @@ method ParallelStatement_Resolve(
   }

 

   parallel (p | 0 <= p)

-    ensures F(p) <= Sum(p) * (p-1) + 100;

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

   {

     assert 0 <= G(p);

     ghost var t;

     if (p % 2 == 0) {

-      assert G(p) == F(p+2);

+      assert G(p) == F(p+2);  // error (there's nothing that gives any relation between F and G)

       t := p*p;

     } else {

       assume H(p, 20) < 100;  // don't know how to justify this

@@ -79,6 +47,53 @@ method Lemma(x: int, y: int)
 ghost method PowerLemma(x: int, y: int)

 

 function F(x: int): int

-function G(x: int): int

+function G(x: int): nat

 function H(x: int, y: int): int

 function Sum(x: int): int

+

+// ---------------------------------------------------------------------

+

+method M0(S: set<C>)

+  requires null !in S;

+  modifies S;

+  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) {

+    s.data := 85;

+  }

+}

+

+method M1(S: set<C>, x: C)

+  requires null !in S && x in S;

+{

+  parallel (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)

+  } else {

+    assert x.data < 120;

+  }

+

+  parallel (s | s in S)

+    ensures s.data < 70;  // error

+  {

+    assume s.data == 85;

+  }

+}

+

+method M2() returns (a: array<int>)

+  ensures a != null;

+  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) {

+    a[i] := 423;

+  }

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

+    a[i] := 300 + i;

+  }

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index bfa88b54..a670ced5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -16,7 +16,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Comprehensions.dfy Basics.dfy ControlStructures.dfy

-            Termination.dfy DTypes.dfy

+            Termination.dfy DTypes.dfy Parallel.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

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

     tail := n;

 

-    foreach (m in spine) {

+    parallel (m | m in spine) {

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

     }

     contents := head.tailContents;

 

-    foreach (m in spine) {

+    parallel (m | m in spine) {

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

     }

     footprint := footprint + n.footprint;