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/b6.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/b6.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b6.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy index e5d061d2..f6e7879f 100644 --- a/Test/VSI-Benchmarks/b6.dfy +++ b/Test/VSI-Benchmarks/b6.dfy @@ -63,7 +63,7 @@ class Iterator { function Valid():bool
reads this, footprint;
{
- this in footprint && c!= null && -1<= pos && !(null in footprint)
+ this in footprint && c!= null && -1<= pos && null !in footprint
}
method Init(coll:Collection)
|