Re: SPARK understand me very well... me neither

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

Le Sat, 14 Aug 2010 23:50:08 +0200, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:
>> But what seems important to me and I would to underline, was also that
>> if I did not knew this was possible, this was because it was fr from my
>> mind. And this was far from my mind, because looking at it as-is, I
>> would have said “what does it prove ? what does it offer ?”. In short,
>> this looks like a bad logical interface to me.
>
> It doesn't prove anything, and it's not supposed to. It's a  
> precondition. It says, "This precondition must be true for this  
> operation to give correct results." It is the caller's duty to meet the  
> precondition.

Reading you again, I understand I did not choose the good words. I should  
have said “what does it defines ?” (like defining what a valid context is,  
in a concrete way). Otherwise yes, this does not have to prove anything,  
and this can't, because nothing is provable at this level.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.