[bitc-dev] {,de}allocation

Pierre THIERRY nowhere.man at levallois.eu.org
Mon Jan 29 04:49:57 CST 2007

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

nowhere.man at levallois.eu.org
OpenPGP 0xD9D50D8A
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.coyotos.org/pipermail/bitc-dev/attachments/20070129/035efa63/attachment.bin 

More information about the bitc-dev mailing list