diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-24 13:51:47 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-24 13:51:47 -0700 |
| commit | 381b00d89ff2a948297a501666c427b22e24f7b1 (patch) | |
| tree | ed3a1b7e69b358a9034df342926ef524033e17d5 /Test/VSI-Benchmarks | |
| parent | cf064ddef7b6cb91023d3de7220345fcccc87b9e (diff) | |
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
Diffstat (limited to 'Test/VSI-Benchmarks')
| -rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 4 |
1 files changed, 2 insertions, 2 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;
|