[ANN] cdecimal-2.3 released
stefan-usenet at bytereef.org
Fri Feb 3 16:11:09 EST 2012
Paul Rubin <no.email at nospam.invalid> wrote:
> > Both cdecimal and libmpdec have an extremely conservative release policy.
> > When new features are added, the complete test suite is run both with and
> > without Valgrind on many different platforms. With the added tests against
> > decNumber, this takes around 8 months on four cores.
> Wow. I wonder whether it's worth looking into some formal verification
> if the required level of confidence is that high.
Currently four of the main algorithms (newton-div, inv-sqrt, sqrt, log)
and a couple of auxiliary functions have proofs in ACL2. The results
are mechanically verified Lisp forms that are guaranteed to produce results
*within correct error bounds* in a conforming Lisp implementation.
Proving full conformance to the specification including all rounding
modes, Overflow etc. would be quite a bit of additional work.
For C, I think the why3 tool should be a good approach:
The verification of the L4 kernel allegedly took 30 man-years, so
it might take a while...
More information about the Python-list