Dafny: parallel statements:

- removed the awkward restriction that method postconditions cannot use old/fresh if there's no modifies clause and no out-parameters; instead, implemented parallel statements to handle these cases
- also allow old/fresh in ensures clauses of parallel statements
- allow TypeRhs and choose expressions in Call/Proof parallel statements
- disallow calls to non-ghost methods in parallel statements (since those may do "print" statements and we don't want to allow those to take place in parallel; besides, the compiler wants to omit the parallel statement altogether and could not do so if there were print statements)

1 files changed, 72 insertions, 1 deletions

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 539974fd..24f85e5d 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -53,7 +53,7 @@ method ParallelStatement_Resolve(
   }

 }

 

-method Lemma(c: C, x: int, y: int)

+ghost method Lemma(c: C, x: int, y: int)

   requires c != null;

   ensures c.data <= x+y;

 ghost method PowerLemma(x: int, y: int)

@@ -198,3 +198,74 @@ method OmittedRange() {
     DontDoMuch(x);

   }

 }

+

+// ----------------------- two-state postconditions ---------------------------------

+

+class TwoState_C { ghost var data: int; }

+

+ghost static method TwoState0(y: int)

+  ensures exists o: TwoState_C :: o != null && fresh(o);

+{

+  var p := new TwoState_C;

+}

+

+method TwoState_Main0() {

+  parallel (x) { TwoState0(x); }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}

+

+ghost static method TwoState1(y: int)

+  ensures exists c: TwoState_C :: c != null && c.data != old(c.data);

+{

+  var c := new TwoState_C;

+  c.data := c.data + 1;

+}

+

+method TwoState_Main1() {

+  parallel (x) { TwoState1(x); }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}

+

+method X_Legit(c: TwoState_C)

+  requires c != null;

+  modifies c;

+{

+  c.data := c.data + 1;

+  parallel (x | c.data <= x)

+    ensures old(c.data) < x;  // note that the 'old' refers to the method's initial state

+  {

+  }

+}

+

+// At first glance, this looks like a version of TwoState_Main0 above, but with an

+// ensures clause.

+// However, there's an important difference in the translation, which is that the

+// occurrence of 'fresh' here refers to the initial state of the TwoStateMain2

+// method, not the beginning of the 'parallel' statement.

+// Still, care needs to be taken in the translation to make sure that the parallel

+// statement's effect on the heap is not optimized away.

+method TwoState_Main2()

+{

+  parallel (x: int)

+    ensures exists o: TwoState_C :: o != null && fresh(o);

+  {

+    TwoState0(x);

+  }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}

+

+// At first glance, this looks like an inlined version of TwoState_Main0 above.

+// However, there's an important difference in the translation, which is that the

+// occurrence of 'fresh' here refers to the initial state of the TwoStateMain3

+// method, not the beginning of the 'parallel' statement.

+// Still, care needs to be taken in the translation to make sure that the parallel

+// statement's effect on the heap is not optimized away.

+method TwoState_Main3()

+{

+  parallel (x: int)

+    ensures exists o: TwoState_C :: o != null && fresh(o);

+  {

+    var p := new TwoState_C;

+  }

+  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+}