Dmitry Nadezhin wrote:
> The current specification of the "interesting" methods in
StrictMath, such as sin/cos, log, > etc. are to use the FDLIBM
algorithms.
Thank you. I forgot about these lines in java.lang.StrictMath .
[snip]
As specification of java.lang.StrictMath is in terms of reference
fdlibm C library
and algorithms in new java.lang.StrictMath are expected similar to
fdlibm algorithms,
the task of formal verification becomes easier.
The comment 3 in fdlibm's readme file warns about
---
3. Compiler failure on non-standard code
Statements like
*(1+(int*)&t1) = 0;
are not standard C and cause some optimizing compilers (e.g. GCC)
to generate bad code under optimization. These cases
are to be addressed in the next release.
---
Nevertheless, I hope that for some additional assumptions about C
pointers, the meaning
of fdlibm C code can be used as the specification.
The C language does not really define an operational semantics for these
operations. In contrast, with the tighter specification of Java's
integral and floating-point types and expressions using those values, it
is really well-posed to discuss the meaning of Java versions of these
algorithms.
However, there is a question. Many methods of java.lang.StrictMath are
used in a reference implementation of java.lang.Math methods.
java.lang.Math specifies methods in terms of accuracy of the returned
result
and monotonicity of the methods.
Suppose that there is still a bug in fdlibm 5.3 and some fdlibm
function fails to
satisfy one ulp accuracy or monotonicity. What will be the
specification of
corresponding java.lang.StrictMath method in such a case ?
The FDLIBM functions are believed to follow the stated quality of
implementation criteria in java.lang.Math. When that turns out not to
be the case, there are a variety of remedies including fixing the bug in
FDLIBM. Fixing bugs I had independently found in pow and tan prompted
raising the required FDLIBM version from 5.2 to 5.3, see 5033578 "Java
should require use of latest fdlibm 5.3."
Cheers,
-Joe