Re: Integrated theorem prover in compiler

- - <cdegouw@gmail.com> writes:


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


Other tools are SPARK (from Praxis) and Inspector (from SofCheck).


> Integration of a theorem prover in a compiler has numerous advantages:


0) It's more convenient than running a separate tool.


> 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


I don't see that. This seems the same, whether the proofs are done by a
separate tool, or integrated with the compiler.


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


Yes.


One possibility is to use something like SPARK to prove that assertions
are true, and then tell the compiler to suppress the run-time checks.


Anyway, many compilers do some small amount of this already. For
example, there's an implicit assertion that pointers are not null when
you dereference them:


        while X /= null then
                X := X.Next;
                ...


Many compilers can prove that X is not null in the loop,
and avoid a check.


As I said, "small amount".


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


Yes, but this seems essentially the same as point (2). If the compiler
can prove that such-and-such is true, then it can optimize based on that
fact.


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


Well, this particular example is easy. For example, in Ada, if you say:


        type T is range 0..255;
        X : T := 100;


then the compiler can easily know that X can be allocated 1 byte.
No fancy proofs necessary. Fancy proofs might be necessary to prove
that "X := X + 1;" doesn't cause trouble.


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


I don't buy that argument. In many cases, it's easier to check the
assertions (either at run time or statically) than to "compile" those
assertions into code that implements them. For example, consider a
square-root function. The requirement is that the result squared is
equal to the argument (plus-or-minus some epsilon). That's easy to
check, but hard to compile. The actual algorithm might be some
complicated loop that iterates toward the correct answer.


In other words, "Assert (Result*Result = Argument);" gives no hint to a
compiler how to efficiently produce Result, given Argument. "Just
compile the assertions" won't work in this case.


>... Also see
> http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf -John]


Yes, thanks for the link, that's worth reading.


- Bob

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