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? > 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... Curiously, Pierre -- [EMAIL PROTECTED] OpenPGP 0xD9D50D8A
signature.asc
Description: Digital signature
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
