Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.python > #19845

Re: [ANN] cdecimal-2.3 released

Show all headers | View raw

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

Back to comp.lang.python | Previous | Next — Previous in thread | Find similar | Unroll thread

Thread

[ANN] cdecimal-2.3 released Stefan Krah <stefan@bytereef.org> - 2012-02-02 21:54 +0100
  Re: [ANN] cdecimal-2.3 released Paul Rubin <no.email@nospam.invalid> - 2012-02-02 23:33 -0800
    Re: [ANN] cdecimal-2.3 released Stefan Krah <stefan-usenet@bytereef.org> - 2012-02-03 22:11 +0100

csiph-web