"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.v87eozlaule2fv@douda-yannick...
Le Sun, 05 Feb 2012 07:29:21 +0100, Randy Brukardt <randy@rrsoftware.com>  a 
�crit:
>> A large part of the problem that I see with proof tools is that they 
>> often
>> require peeking into the body to verify calls. This is just plain wrong,
>> because it means that the proof has to be redone if the body changes. And 
>> it
>> also means that the body has to exist (and in a near-final form) before 
>> the proof can be valuable.
>
>Seems strange assertion.
>
>With SPARK, you prove the implementation is conforming to its

Sorry, I was talking about "some" proof tools, not any specific one. And 
recall that I was specifically answering a query about why seeing the body 
was not good enough. SPARK is *not* seeing the body, so none of what I said 
applies to it. But there are a lot of "correctness" tools out there that 
only work with complete source code.

                                 Randy.