diff options
| author |  Jason Koenig <unknown> | 2011-07-05 18:22:41 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-05 18:22:41 -0700 |
| commit | 1a2271a8bc81a8ff96b033c3911cb80db6832dc1 (patch) | |
| tree | 047bae5a72cc41d1f8287d0664dc623f48332a9f /Test/dafny0/ParseErrors.dfy | |
| parent | 3cb199c1157ab54025cc49558d58c57fc35d6a01 (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
|