diff options
author | qadeer <unknown> | 2014-05-04 21:17:12 -0700 |
---|---|---|
committer | qadeer <unknown> | 2014-05-04 21:17:12 -0700 |
commit | 28d4e2ad2598ff377f121ff2a2a9b0794f386110 (patch) | |
tree | 5bd85a8938154aabf3eb80751c1f9dd54f980c31 /Test/og/parallel2.bpl | |
parent | 36e016acf963b7c19d59640b11b4a40f2072943e (diff) |
second checkpoint
Diffstat (limited to 'Test/og/parallel2.bpl')
-rw-r--r-- | Test/og/parallel2.bpl | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index 4a3c1849..1bce7c8a 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -27,7 +27,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid yield;
call Write(i, 42);
- call i := Yield(i);
+ call Yield(i);
assert {:phase 1} a[i] == 42;
}
@@ -41,11 +41,9 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid assert {:phase 1} a[i] == 42;
}
-procedure {:yields} {:phase 1} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
-ensures {:phase 1} i == i';
+procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int)
ensures {:phase 1} old(a)[i] == a[i];
{
- i := i';
yield;
assert {:phase 1} old(a)[i] == a[i];
}
\ No newline at end of file |