Groups > comp.lang.python > #19845

Re: [ANN] cdecimal-2.3 released

Path	csiph.com!x330-a1.tempe.blueboxinc.net!usenet.pasdenom.info!gegeweb.org!de-l.enfer-du-nord.net!feeder2.enfer-du-nord.net!tudelft.nl!txtfeed1.tudelft.nl!multikabel.net!newsfeed20.multikabel.net!news2.euro.net!newsgate.cistron.nl!newsgate.news.xs4all.nl!post.news.xs4all.nl!not-for-mail
Return-Path	<stefan-usenet@bytereef.org>
X-Original-To	python-list@python.org
Delivered-To	python-list@mail.python.org
X-Spam-Status	OK 0.023
X-Spam-Evidence	'H': 0.95; 'S': 0.00; 'subject:ANN': 0.02; 'subject:: [': 0.02; 'subject:released': 0.03; 'added,': 0.09; 'rounding': 0.09; 'auxiliary': 0.16; 'conformance': 0.16; 'lisp': 0.16; 'overflow': 0.16; 'valgrind': 0.16; 'subject:] ': 0.16; 'wrote:': 0.16; 'header:In-Reply-To:1': 0.22; 'wonder': 0.23; 'high.': 0.23; 'stefan': 0.24; 'tests': 0.25; 'paul': 0.27; 'bit': 0.28; 'work.': 0.28; 'received:78.46': 0.30; 'error': 0.30; 'quite': 0.31; 'correct': 0.31; 'header:User-Agent:1': 0.33; 'to:addr:python-list': 0.33; 'algorithms': 0.34; 'platforms.': 0.34; 'test': 0.35; 'charset:us-ascii': 0.36; 'run': 0.37; 'received:org': 0.37; 'some': 0.38; 'couple': 0.38; 'think': 0.38; 'should': 0.38; 'tool': 0.39; 'received:78': 0.39; 'might': 0.40; 'to:addr:python.org': 0.40; 'extremely': 0.40; 'worth': 0.61; 'full': 0.62; 'results': 0.64; 'policy.': 0.71; 'verified': 0.73; 'guaranteed': 0.77; 'verification': 0.78; 'confidence': 0.82; 'conservative': 0.84; 'subject:2.3': 0.84; 'url:fr': 0.96
Date	Fri, 3 Feb 2012 22:11:09 +0100
From	Stefan Krah <stefan-usenet@bytereef.org>
To	python-list@python.org
Subject	Re: [ANN] cdecimal-2.3 released
References	<mailman.5376.1328216447.27778.python-list@python.org> <7xfwespe1f.fsf@ruckus.brouhaha.com>
MIME-Version	1.0
Content-Type	text/plain; charset=us-ascii
Content-Disposition	inline
In-Reply-To	<7xfwespe1f.fsf@ruckus.brouhaha.com>
User-Agent	Mutt/1.5.18 (2008-05-17)
X-BeenThere	python-list@python.org
X-Mailman-Version	2.1.12
Precedence	list
List-Id	General discussion list for the Python programming language <python-list.python.org>
List-Unsubscribe	<http://mail.python.org/mailman/options/python-list>, <mailto:python-list-request@python.org?subject=unsubscribe>
List-Archive	<http://mail.python.org/pipermail/python-list>
List-Post	<mailto:python-list@python.org>
List-Help	<mailto:python-list-request@python.org?subject=help>
List-Subscribe	<http://mail.python.org/mailman/listinfo/python-list>, <mailto:python-list-request@python.org?subject=subscribe>
Newsgroups	comp.lang.python
Message-ID	<mailman.5422.1328303476.27778.python-list@python.org> (permalink)
Lines	31
NNTP-Posting-Host	2001:888:2000:d::a6
X-Trace	1328303476 news.xs4all.nl 6860 [2001:888:2000:d::a6]:52156
X-Complaints-To	abuse@xs4all.nl
Xref	x330-a1.tempe.blueboxinc.net comp.lang.python:19845

Show key headers only | 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