Proof of contract correctness

[Michiel]

Hi,

I was wondering, are there currently any tools/compilers that attempt
to statically (not at runtime) prove the correctness of function
contracts (using, for example, Hoare logic / VDM)? I'm doing research
in that direction and I would like to know the state of the art in
this area. The Eiffel newsgroup seemed like a good place to ask.

Thanks in advance for your reply.

[Georg Bauhaus]

Michiel schrieb:

IIRC, there is software supporting the B Method. Might be in the
same direction.

[llothar]

Only tools i know are for Ada. Definetely nothing really serious
other then student work for Eiffel.

[Helmut]

Unfortunately non of the available Eiffel compilers try to prove
contracts.

The Eiffel Compiler tecomp has planned to provide a proving compiler.
There are already some white papers on the website (http://
tecomp.sourceforge.net -> internals -> verify sw), but nothing has
been implemented up to now.

[Rod Chapman]

You might want to take a look at SPARK, which
does static contract verification using Hoare-Logic and
Theorem Proving. GPL tools
are here at libre.adacore.com. A non-trivial example
is the Tokeneer system - also downloadable free
from www.adacore.com/tokeneer.
- Rod Chapman, SPARK Team, Praxis