From 381b00d89ff2a948297a501666c427b22e24f7b1 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 24 Oct 2011 13:51:47 -0700 Subject: 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 --- Test/VSI-Benchmarks/b5.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/VSI-Benchmarks') 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 { 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; -- cgit v1.2.3