[ANN] cdecimal-2.3 released

Stefan Krah 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:

http://why3.lri.fr/


The verification of the L4 kernel allegedly took 30 man-years, so
it might take a while...


Stefan Krah






More information about the Python-list mailing list