diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-25 17:02:16 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-25 17:02:16 -0700 |
| commit | 2423c9862c847a6ffbf5d826e45bae4fa5d0f1ec (patch) | |
| tree | 16655fe75ad924f026ee9a4efca09ba6d2939e43 /Test/dafny0/Parallel.dfy | |
| parent | aa7ebf6af120f1c30ec04a8fb377ddbc71ecf5d2 (diff) | |
Dafny: implemented compilation of parallel statements
Dafny: beefed up resolution of parallel statements
Diffstat (limited to 'Test/dafny0/Parallel.dfy')
| -rw-r--r-- | Test/dafny0/Parallel.dfy | 39 |
1 files changed, 39 insertions, 0 deletions
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
+ }
+ }
+}
|