search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

introduce a \distinct operator #16

Open vprevosto opened 7 years ago

vprevosto commented 7 years ago

chains of != are explicitely forbidden. Would it make sense to consider that a != b != c means a!=b && a!=c && b!=c in the same spirit as the distinct operator of SMTLib?

Of course, != could not be mixed with any other operator.

davidcok commented 6 years ago

This would be a different chain than for other consecutive operators, which would mean a!= b && b != c. As consecutive operators are only used for predicates and already cause ambiguity problems, I'm not eager to expand their use. I'd prefer an explicit \distinct within ACSL.

vprevosto commented 6 years ago

Fair enough. \distinct has some uses, so I'm leaving the issue opened but will edit it in that direction