Dmitry Nadezhin wrote:
Joseph D. Darcy wrote:
Yes, porting FDLIBM to Java has been an oft-delayed "nice to have"
project of mine. It is not obvious from looking at my ceil/floor
code, but it started with the FDLIBM versions of those algorithms.
The tests are new and greatly outnumber the code changes, as it
typical in this line of work :-) I think getting an all-java
StrictMath library would be best done as a series of small batches so
floor/ceil could be a start.
Floating-point algorithms are difficult to test.
Maybe, the new StrictMath.java can be verified by formal methods (in
addition to tests) ?
We would be more confident, if we obtain machine-checked proof that
the result of method execution by JVM differs from exact mathematical
result no more than 1 ulp in for all Float/Double inputs.
I googled some papers on verification of floating-point:
http://www-lipn.univ-paris13.fr/CerPAN/files/ARITH.pdf
http://shemesh.larc.nasa.gov/fm/papers/Boldo-CR-2006-214298-Floating-Point.pdf
http://www.cl.cam.ac.uk/~jrh13/papers/fparith.pdf
What do you think about such perspective ?
The current specification of the "interesting" methods in StrictMath,
such as sin/cos, log, etc. are to use the FDLIBM algorithms. Another
approach would be to specify that "correctly rounded" algorithms be
used. Such a specification would constrain the result according to the
method's behavior (i.e. define a mathematically "correct" result) rather
than defining the correct result based on matching a particular
implementation. Developing and testing correctly rounded algorithms
remains a research area with Jean-Michel Muller and associates doing
good work.
That said, while there is certainly value in formal methods, I think
they would be overkill for the regression testing needs of the JDK.
-Joe
