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, 36 insertions, 19 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3be192cc..73c24335 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1019,24 +1019,21 @@ Execution trace:
 Dafny program verifier finished with 27 verified, 6 errors

 

 -------------------- ParallelResolveErrors.dfy --------------------

-ParallelResolveErrors.dfy(8,6): Error: LHS of assignment must denote a mutable variable or field

-ParallelResolveErrors.dfy(13,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement

-ParallelResolveErrors.dfy(31,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(43,13): Error: set choose operator not supported inside parallel statement

-ParallelResolveErrors.dfy(48,13): Error: new allocation not supported in parallel statements

-ParallelResolveErrors.dfy(53,13): Error: new allocation not supported in parallel statements

-ParallelResolveErrors.dfy(60,19): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(64,18): Error: return statement is not allowed inside a parallel statement

-ParallelResolveErrors.dfy(71,21): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(72,20): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(73,20): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(82,24): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(83,24): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(94,43): Error: fresh expressions are not allowed in this context

-ParallelResolveErrors.dfy(101,50): Error: old expressions are not allowed in this context

-ParallelResolveErrors.dfy(124,12): Error: old expressions are not allowed in this context

-ParallelResolveErrors.dfy(144,45): Error: fresh expressions are not allowed in this context

-17 resolution/type errors detected in ParallelResolveErrors.dfy

+ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field

+ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement

+ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement

+ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements

+ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods

+ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement

+ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop

+ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop

+14 resolution/type errors detected in ParallelResolveErrors.dfy

 

 -------------------- Parallel.dfy --------------------

 Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.

@@ -1116,8 +1113,28 @@ Execution trace:
     (0,0): anon19_Then

     (0,0): anon20_Then

     (0,0): anon5

+Parallel.dfy(214,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

+Parallel.dfy(226,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

+Parallel.dfy(254,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon5

+Parallel.dfy(270,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon5

 

-Dafny program verifier finished with 24 verified, 8 errors

+Dafny program verifier finished with 34 verified, 12 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(44,22): Error: assertion violation