diff options
Diffstat (limited to 'Chalice/tests/general-tests/counter.chalice')
| -rw-r--r-- | Chalice/tests/general-tests/counter.chalice | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Chalice/tests/general-tests/counter.chalice b/Chalice/tests/general-tests/counter.chalice index 828cf005..c15ed36b 100644 --- a/Chalice/tests/general-tests/counter.chalice +++ b/Chalice/tests/general-tests/counter.chalice @@ -53,9 +53,10 @@ class Program { }
method doRelease(c: Counter, i: int)
- requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && i<=c.value);
+ requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && c.value <= i);
lockchange c;
{
+ c.value := i+1
release c; // ok, because of atAcquire conjunct in the precondition
}
|