Version française
Home     About     Download     Resources     Contact us    
Browse thread
Re: RE: reference initialization
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Patrick M Doane <patrick@w...>
Subject: Re: RE: reference initialization
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