Re: Silly and stupid post-condition or not ?

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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  
specification. So, obviously, if the implementation changes, then you have  
to prove it again, but just like you have to recompile it again.

No implementation is required to refer to a signature. SPARK will relies  
on the annotations associated with the signature every where a given  
subprogram is invoked. Just like Janus/Ada seems to compile, after what  
you explained elsewhere.

Or else I did not understand what you meant.

Were you thinking about automated and à‑posteriori analysis tools? This  
are not proof‑tools.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University