Re: Testing strategy for compiler

Jean-Marc Bourguet <jm@bourguet.org>
21 Jun 2010 12:59:09 +0200

          From comp.compilers
Related articles
[3 earlier articles]
Re: Testing strategy for compiler ott@mirix.org (Matthias-Christian Ott) (2010-06-18)
Re: Testing strategy for compiler gene.ressler@gmail.com (Gene) (2010-06-18)
Re: Testing strategy for compiler gneuner2@comcast.net (George Neuner) (2010-06-18)
Re: Testing strategy for compiler gah@ugcs.caltech.edu (glen herrmannsfeldt) (2010-06-18)
Re: Testing strategy for compiler ott@mirix.org (Matthias-Christian Ott) (2010-06-19)
Re: Testing strategy for compiler gah@ugcs.caltech.edu (glen herrmannsfeldt) (2010-06-19)
Re: Testing strategy for compiler jm@bourguet.org (Jean-Marc Bourguet) (2010-06-21)
Re: Testing strategy for compiler dot@dotat.at (Tony Finch) (2010-06-21)
Re: Testing strategy for compiler gneuner2@comcast.net (George Neuner) (2010-06-21)
Re: Testing strategy for compiler news@cuboid.co.uk (Andy Walker) (2010-06-22)
Re: Testing strategy for compiler barry.j.kelly@gmail.com (Barry Kelly) (2010-06-22)
Re: Testing strategy for compiler gah@ugcs.caltech.edu (glen herrmannsfeldt) (2010-06-23)
| List of all articles for this month |
From: Jean-Marc Bourguet <jm@bourguet.org>
Newsgroups: comp.compilers
Date: 21 Jun 2010 12:59:09 +0200
Organization: Guest of ProXad - France
References: 10-06-037 10-06-044 10-06-050 10-06-052
Keywords: testing, theory
Posted-Date: 21 Jun 2010 11:02:26 EDT

Matthias-Christian Ott <ott@mirix.org> writes:


> [I would be astonished if anyone ever managed to do a mechanical proof of a
> non-trivial piece of a compiler. And even if they did, they'd still never
> know whether there were bugs in the formal description. -John]


There is some work at INRIA about this, see:
http://compcert.inria.fr/doc/index.html


From the introduction:


    Compcert is a compiler that generates PowerPC and ARM assembly code from
    Clight, a large subset of the C programming language. The particularity
    of this compiler is that it is written mostly within the specification
    language of the Coq proof assistant, and its correctness --- the fact
    that the generated assembly code is semantically equivalent to its source
    program --- was entirely proved within the Coq proof assistant.


I haven't yet found the time to found out what precisely was covered by
that.


Yours,


--
Jean-Marc


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.