diff options
author | 2011-07-05 18:22:41 -0700 | |
---|---|---|
committer | 2011-07-05 18:22:41 -0700 | |
commit | b5b29c378a82415e1d2b40528d06845f9c32d3ac (patch) | |
tree | 4c363bfef9f1712188e4838ed7dace4091330463 /Test/dafny0/ParseErrors.dfy | |
parent | b3713a4e1f7feb345d93825d094a31450202e40f (diff) |
Dafny: Updated regression tests to include chaining disjoint operators.
Diffstat (limited to 'Test/dafny0/ParseErrors.dfy')
-rw-r--r-- | Test/dafny0/ParseErrors.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy index d6f3005d..41df50eb 100644 --- a/Test/dafny0/ParseErrors.dfy +++ b/Test/dafny0/ParseErrors.dfy @@ -11,7 +11,7 @@ method TestChaining0(j: int, k: int, m: int) method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set<T>>)
requires s <= t <= u >= s+u; // error: cannot mix <= and >=
ensures s <= u;
- ensures s !! t !! u; // error: !! is not chaining (but it would be nice if it were)
+ ensures s !! t !! u; // valid, means pairwise disjoint
ensures x in s in SuperSet; // error: 'in' is not chaining
ensures x !in s in SuperSet; // error: 'in' is not chaining
ensures x in s !in SuperSet; // error: 'in' is not chaining
|