Floating point comparison

[vprevosto]

The ACSL manual indicates that there are builtins operators for floating-point comparison (as opposed to the < et al. operators that take real arguments. However, the phrasing is quite ambiguous:

Special predicates are also available to express the comparison operators of float (resp. dou- ble) numbers as in C: \eq_float , \gt_float , \ge_float , \le_float , \lt_float , \ne_float (resp. for double).

Does that mean that we have an overloaded operator or two distinct operators?

• overloaded version:

  boolean \eq_float(float x, float y);
  boolean \eq_float(double x, double y);

• distinct operators version:

  boolean \eq_float(float x, float y);
  boolean \eq_double(double x, double y);

If the former, I'd suggest to find another name than \eq_float, \eq_ieee for instance (in the context of floating-point computation, which IEEE norm we are referring to should be quite clear), or \eq_fp.

[maroneze]

I would tend to consider the second option (distinct operators). Since there are already operators to distinguish between real and float, introducing implicit overloading between float and double seems to me somewhat unexpected.

Also, this would be inconsistent with the current naming of other operators: real_of_float and real_of_double are already different operators, as well as \round_float and \round_double. Either float should mean strictly 32-bit single-precision floats everywhere, or "floating-point" in general everywhere.

The only advantage of using float generically would be to avoid having a third predicate for long double. But since its support is very limited, it's maybe a blessing in disguise (i.e., if someone passes long doubles to operators expecting floats, it should currently fail instead of silently accepting them).

[vprevosto]

introducing implicit overloading between float and double seems to me somewhat unexpected.

Bad luck, there are already such operators (in particular \is_finite and friends) 😁

Also, this would be inconsistent with the current naming of other operators: real_of_float and real_of_double

This was also my first impression, but the situation is different: those two functions differ by their return type, hence can't be overloaded (overloading resolution is done on parameters' types).

That said, I'm playing devil's :imp: advocate here: I'd also tend to favor the two operators solution

[davidcok]

To add one other thought into this thread: I often like overloading because it makes it easier to change or templatize types (thinking C++ here). For example, suppose you give variable types using a typedef, e.g. typedef ... real_like; which can be float or double or long double. Then one can write real_like a,b,c; c = a+b; c = sin(a); ... \is_finite(a). In this context, being able to use overloaded functions such as \eq(a, b) would be an advantage and \eq_float would be a nuisance. C++'s type inference with 'auto' declarations also encourages overloaded functions.

[vprevosto]

I was about to say that in that particular case, the overloaded operator is ==, but this is not true (because of infinity and NaN as usual) as this operator takes reals. Still, with overloading, \eq(f,d) (where f is a float and d double) looks a bit problematic to me: f will be silently promoted to double, and the predicate may be false whereas \eq(f,(float)d) would be true by virtue of rounding, which in my opinion might be the source of subtle specification bugs.

[correnson]

It is still possible to recover both styles by using logical definitions. However, handling them natively would be preferable ! I would strongly suggest some systematic policy all over the standard.

Since we already have operators with overloading, and others with no-overloading, what about define both styles for every operators ? I mean:

• \op_t1( t1 , ... , t1 )
• \op_t2( t2 , ... , t2 )
• \op( t1 , ... , t1 ) (defined to be \op_t1)
• \op( t2 , ... , t2 ) (defined to be \op_t2)

This way, we stay backward-compatible and we may encourage the use of non-overloaded symbols to clarify specifications.

[vprevosto]

I agree with you that at this stage this looks like the most sensible option