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>
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

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