Re: Integrated theorem prover in compiler

- - <cdegouw@gmail.com> writes:


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


There is Spec#, a C# variant that statically checks assertions and for
null pointers etc. See
http://research.microsoft.com/en-us/projects/specsharp/




> 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


The assertions are not full specifications, so this is not fully
exploited. The assertions do provide the necessary preconditions for
using a function, though, so you can see this from the specification.


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


It can certainly eliminate certain runtime checks such as null pointer
checks and range checks, but this is hindered by compiling to .NET,
which enforces such checks at runtime. Eiffel-style runtime checking of
assertions is avoided, though.


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


Apart from (potentially) eliminating null-pointer checks and range
checks, I'm not sure to which extent this is exploited, but I can
imagine exploiting assertions in data flow analyses by, essentially,
using the assertions to filter the sets of values during analysis.


Torben

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