diff options
| author |  Rustan Leino <unknown> | 2013-03-06 15:09:04 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-03-06 15:09:04 -0800 |
| commit | 172554c51fad4092f2b4e52a921ad0e86fa67ca6 (patch) | |
| tree | cc3c3430f1a379255f9c4990b26df1c21e06bd38 /Test/dafny0/SmallTests.dfy | |
| parent | d584ab2b4240b58cd4ef59e53b970a05d8d13f79 (diff) | |
Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional.
Diffstat (limited to 'Test/dafny0/SmallTests.dfy')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index c55d6140..2f12fdd2 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -144,7 +144,7 @@ class Modifies { method F(s: set<Modifies>)
modifies s;
{
- parallel (m | m in s && m != null && 2 <= m.x) {
+ forall m | m in s && m != null && 2 <= m.x {
m.x := m.x + 1;
}
if (this in s) {
@@ -157,17 +157,17 @@ class Modifies { {
var m := 3; // this is a different m
- parallel (m | m in s && m == this) {
+ forall m | m in s && m == this {
m.x := m.x + 1;
}
if (s <= {this}) {
- parallel (m | m in s) {
+ forall (m | m in s) {
m.x := m.x + 1;
}
F(s);
}
- parallel (m | m in s) ensures true; { assert m == null || m.x < m.x + 10; }
- parallel (m | m != null && m in s) {
+ forall (m | m in s) ensures true; { assert m == null || m.x < m.x + 10; }
+ forall (m | m != null && m in s) {
m.x := m.x + 1; // error: may violate modifies clause
}
}
@@ -304,7 +304,7 @@ class SomeType requires null !in stack;
modifies stack;
{
- parallel (n | n in stack) {
+ forall n | n in stack {
n.x := 10;
}
}
|