Paul Rubin <no.email@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 -- http://mail.python.org/mailman/listinfo/python-list
