diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-13 17:44:45 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-13 17:44:45 -0700 |
| commit | 3d56fc351f6a71d90e72ef115477d1be663cfba5 (patch) | |
| tree | c0dbc350b8447b199e3233ba86dea7329553984c /Test/dafny0/ParallelResolveErrors.dfy | |
| parent | b2eb7236b06ea3102b8cf86fc8f41c555a089614 (diff) | |
Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
Diffstat (limited to 'Test/dafny0/ParallelResolveErrors.dfy')
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index ab711d02..f260edb5 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -103,6 +103,6 @@ method M1() { method M2() {
var a := new int[100];
parallel (x | 0 <= x < 100) {
- a[x] :| a[x] > 0; // error: not allowed to update heap location in a parallel statement with a(n implicit) assume
+ a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a parallel statement with an assume
}
}
|