diff options
author | rustanleino <unknown> | 2009-11-05 01:24:43 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2009-11-05 01:24:43 +0000 |
commit | 48a417d2201f5e4151b1575d4ec011343c69e389 (patch) | |
tree | cf9c5ac4f7ca2aeaf2586fad2f3d3906117cda44 /Test/VSI-Benchmarks/b7.dfy | |
parent | 13fcd7a9763591f82d75337a60aec10766b65d91 (diff) |
Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "!(x in S)".
Changed Dafny test files to use the new operator.
Included the file b8.dfy into the VSI-Benchmarks test harness.
Diffstat (limited to 'Test/VSI-Benchmarks/b7.dfy')
-rw-r--r-- | Test/VSI-Benchmarks/b7.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index 13a8ccd2..95267823 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -36,7 +36,7 @@ class Stream { function Valid():bool
reads this, footprint;
{
- !(null in footprint) && this in footprint && isOpen
+ null !in footprint && this in footprint && isOpen
}
method GetCount() returns (c:int)
@@ -152,7 +152,7 @@ class Client { var wr:= new Stream;
call wr.Create();
while (0<|q.contents|)
- invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && !(q in wr.footprint);
+ invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
decreases |q.contents|;
{
call ch:= q.Dequeue();
|