From 2423c9862c847a6ffbf5d826e45bae4fa5d0f1ec Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 25 Oct 2011 17:02:16 -0700
Subject: Dafny: implemented compilation of parallel statements Dafny: beefed
 up resolution of parallel statements

---
 Test/dafny0/Parallel.dfy | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'Test/dafny0/Parallel.dfy')

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index e3ba0d67..817120ce 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -148,3 +148,42 @@ method M5()
     assert Pred(34, 34);
   }
 }
+
+method Main()
+{
+  var a := new int[180];
+  parallel (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|) {
+    a[20+i] := sq[i];
+  }
+  parallel (t | t in sq) {
+    a[t] := 1000;
+  }
+  parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
+    a[u] := 6000 + t;
+  }
+  var k := 0;
+  while (k < 180) {
+    if (k != 0) { print ", "; }
+    print a[k];
+    k := k + 1;
+  }
+  print "\n";
+}
+
+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) {
+      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) {
+      a[u] := 6000 + t;  // with the 't < 4' conjunct in the line above, this is fine
+    }
+  }
+}
-- 
cgit v1.2.3