On Mon, 2007-01-29 at 11:49 +0100, Pierre THIERRY wrote: > Scribit Jonathan S. Shapiro dies 28/01/2007 hora 19:18: > > There are two problems with the proof discharge story in general: > > > > 1. It requires whole-program analysis > > Why? The few things I learned so far about proof of programs lead me to > think that usually you discharge proofs about post-conditions based on > pre-conditions, and about pre-conditions being verified at call sites. > > Can't that be made function by function and module by module?
In this case, no. Demonstrating that "free" is safe requires showing that the pointer value is unreachable. This requires whole-program flow analysis. > > 2. It relies on having asked the right questions. > > Yes. As I was told, the hard thing is not to discharge proofs about > code, it's being able fo formally specify the expected semantic of the > code... -- Jonathan S. Shapiro, Ph.D. Managing Director The EROS Group, LLC +1 443 927 1719 x5100 _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
