Frama-C news and ideas

To content | To menu | To search | Frama-C Home


If I told you that when n is a positive power of two and d an arbitrary number, both represented as double, the condition (n - 1) * d + d == n * d in strictly-IEEE-754-implementing C is always true, would you start looking for a counter-example, or start looking for a convincing argument that this property may hold?

If you started looking for counter-examples, would you start with the vicious values? Trying to see if NaN or +inf can be interpreted as “a positive power of two” or “an arbitrary number” represented “as double”? A subnormal value for d? A subnormal value such that n*d is normal? A subnormal value such that (n - 1) * d is subnormal and n * d is normal?

Or would you try your luck with ordinary values such as 0.1 for d and 4 for n?

This post is based on a remark by Stephen Canon. Also, I have discovered a truly remarkable proof of the property which this quick post is too small to contain.


1. On Tuesday, May 14 2013, 23:50 by Stephen Canon

I always like to work a few examples first with an open mind; hopefully they point me either toward a proof or toward a counterexample.

In this case, the first example I choose was n = 2**-64, which happens to provide a counter example (because n-1 = -1, so the LHS is just -d + d = 0, but the right side is exact; more generally this is often a great way to find counter-examples: look for cases where one expression is exact and the other is not, though this does fail sometimes).

2. On Tuesday, May 14 2013, 23:53 by Stephen Canon

If I assume you meant a *positive* power of two, this is a much more interesting post ...

3. On Wednesday, May 15 2013, 00:00 by pascal

Poor me! Yes, this was intended to be “a positive power of two”. The intention was not to leave any loophole, but the property and its truth value were only incidental anyway. I will nevertheless correct this in the text of the post.