Integrated theorem prover in compiler

One of my colleagues brought this message to my attention. Those
interested in this topic might be interested in RESOLVE. RESOLVE is
an integrated specification and implementation language that lets you
specify, develop, compile and verify the kinds of generic components
you may write in Java, C#, or C++. It is in some sense a response to
Tony Hoare's grand challenge; see his article in October CACM for a
short summary.


RESOLVE is a sourceforge project. Please see
www.cs.clemson.edu/~resolve for a current version of RESOLVE verifier
and compiler (actually, a translator to Java). I expect that a web
version will be posted at the site for trying out the
compiler/verifier within the next week.


RESOLVE is very much a research effort involving Clemson, Ohio State,
and several other institutions. While the group has made decent
progress, plenty of research questions remain (including specification
and analysis of memory usage constraints). The technical reports at
the site have details. See the ones on Push-button Verification and
Verification Vision, for example.


Thanks for any feedback.


Three points wrt follow-up messages to the original posting:


Any mathematical theorem used by the RESOLVE verifier must have a
mechanically-derived or mechanically-checkable proof (in other words,
theorems are not accepted based on "social processes.")


A verifier merely proves that code is correct wrt stated
specifications, so as was rightly pointed out in a follow-up, there is
still the separate task of checking that the specifications do indeed
capture requirements. Also, testing will be necessary to validate
code against customer requirements.


RESOLVE language and verifier are designed to verify software one
component at a time in a modular fashion.


Murali
------
> In Eiffel it is possible to specify a function precondition,
> postcondition and loop invariants, but these are not statically
> checked by the compiler (at compile-time), but instead run-time. An
> exception is thrown if any assertion is violated, but of course this
> only shows that for _that particular execution_ no assertion was
> violated. I could not find any compiler that proofs correctness of a
> given function at compile-time. ...

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