Integrated theorem prover in compiler

Hi,


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.


I have seen stand-alone tools that do statically verify correctness of
a function (for example: ESC/Java does (attempt to) verify correctness
of java code statically) but never integrated within a compiler
itself.


Integration of a theorem prover in a compiler has numerous advantages:
1) Users of the functions that have been verified only have to look at
the specification of the function, and not at the implementation for
an accurate description of what the function does
2) There is no need to check the assertions in a program at run-time
anymore if they already have been checked statically
3) There are many more opportunities to optimize code, since
assertions can be used to find out properties of the code the compiler
could otherwise never have found out (a simple example would be that
if the compiler knows an integer is always bounded between 0 and 255,
it just has to allocate 1 byte)


My question is: is there any compiler (for Eiffel, Java or any other
language) that statically checks assertions, and if so, does it
exploit any of the three advantages listed above?
[I'd be surprised. Theorem provers are slow, so for it to be at all
practical the compiler would have to cache its results so it could
skip the proofs it's already tried, and the proofs that are practical
tend to be trivial. I've always thought that the whole idea of
program proofs was backward--if you can describe the program's
behavior in the assertion language, skip the program and compile the
assertions. Also see
http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf -John]

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