On Mon, 15 May 2000 bdb-as-camluser@netcourrier.com wrote:
> Are there any languages in which the programmer can indicate proofs of
> safeness (regardless of fitness for a particular purpose) of the program
> he is writing, and let the compiler use these proofs?
You might want to take a look at work by George Necula for Proof Carrying
Code (PCC), in particular his Touchstone compiler.
One of the optimizations performed by the compiler is the removal of
null-pointer checks. In cases where the compiler does not have enough
local information to remove the check, a precondition can be written that
will be used during optimization.
More about the compiler and PCC in general can be found at his website:
http://www-nt.cs.berkeley.edu/home/necula/public_html/
Patrick Doane
This archive was generated by hypermail 2b29 : Tue May 16 2000 - 04:12:47 MET DST