Re: Integrated theorem prover in compiler

On Wed, 19 Aug 2009 01:57:57 -0700 (PDT), - - <cdegouw@gmail.com>
wrote:


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


That's because, in general, only pure functions can be effectively
proved. You can make certain assertions about imperative code, but
not nearly as many as pure functional or declarative code. Introducing
side effects such as persistent data structures and general I/O
further complicate proofs because the proof becomes dynamically
context dependent.




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


ESC/Java does not verify correctness as doing so requires knowledge of
the intended algorithm being implemented. Instead ESC/Java looks for
evidence of commonly made coding mistakes that are known to lead to
runtime errors.




>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


Assuming the code conforms to the specification ... which, for most
commonly used languages, is not a condition that can be automatically
verified.




>2) There is no need to check the assertions in a program at run-time
>anymore if they already have been checked statically


Assertions that depend on runtime values can't be 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)


You're forgetting that the assertion, being written separately from
the code, may be outdated, ill-fitted, or just plain wrong. This is
the equivalent of the compiler reading comments.


A better solution is to use a data type - either explicitly specified
or inferred by the compiler - that is restricted to the proper set of
values.


As for your example: using 1 byte for a 0..255 value could be much
slower than using a full sized machine word. Except in cases where
the size really matters - such as device register programming - it is
generally sufficient to define the value range or set and leave the
compiler to enforce the restriction however it pleases.




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




I'm not aware of any involving explicit theorem provers or assertions
as such, but the class of declarative languages - Prolog, Mercury, Oz,
etc. - have the property (to varying degrees) that the specification
of the problem solution is executable code. So, in essence, all you
ever write are assertions.


George

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