Re: Integrated theorem prover in compiler

torbenm@pc-003.diku.dk (Torben =?iso-8859-1?Q?=C6gidius?= Mogensen)
Thu, 20 Aug 2009 15:21:41 +0200

          From comp.compilers

Related articles
Integrated theorem prover in compiler cdegouw@gmail.com (- -) (2009-08-19)
Re: Integrated theorem prover in compiler bmd@cs.kuleuven.be (bart demoen) (2009-08-19)
Re: Integrated theorem prover in compiler walter@bytecraft.com (Walter Banks) (2009-08-19)
Re: Integrated theorem prover in compiler pertti.kellomaki@tut.fi (Pertti Kellomaki) (2009-08-20)
Re: Integrated theorem prover in compiler torbenm@pc-003.diku.dk (2009-08-20)
Re: Integrated theorem prover in compiler gneuner2@comcast.net (George Neuner) (2009-08-20)
Re: Integrated theorem prover in compiler bobduff@shell01.TheWorld.com (Robert A Duff) (2009-08-20)
Integrated theorem prover in compiler MSITARA@clemson.edu (Murali Sitaraman) (2009-10-16)
| List of all articles for this month |

From: torbenm@pc-003.diku.dk (Torben =?iso-8859-1?Q?=C6gidius?= Mogensen)
Newsgroups: comp.compilers
Date: Thu, 20 Aug 2009 15:21:41 +0200
Organization: Department of Computer Science, University of Copenhagen
References: 09-08-030
Keywords: theory, optimize
Posted-Date: 20 Aug 2009 10:26:24 EDT

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



Post a followup to this message

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