Re: Lost in translation (with SPARK user rules)

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

Le Thu, 27 May 2010 20:34:52 +0200, Pascal Obry <pascal@obry.net> a écrit:

> Peter,
>
>> I do agree certainly that SPARK is not for everything. The code I'm  
>> working on
>> is (potentially) security sensitive so the extra effort of working with  
>> SPARK
>> seems worthwhile. My test harness, on the other hand, is likely to be  
>> in full
>> Ada.
>
> Just curious, why do you feel that you still need to write tests after
> having run successfully the SPARK proof checker?
>
> Pascal.
Good question Pascal,

May be because that's a tradition, may be because some inside voices tell  
you you're bad if you don't run test, or may be due to the lack of  
understanding that test are done when there is no way to prove anything  
(that is, tests would be a fall-back).

Peter, I'm not telling that's you though, I'm just telling that testing is  
so much genetically inlaid in the computer culture, that doing without it,  
would be somewhat frightening, just like the first time one learn to swim  
or to ride a bicycle (waw, do I really have to stand up on this thing  
which not even able to stand up by itself ?)

But may be there is another reason : logic.

That is a question I have in mind since I've recently discovered (well,  
really started with) SPARK : one may prove something, while he/she may not  
really know what he/she is proving. You may prove some specifications (I  
mean pre/post, not runtime error safety), but what if this specifications  
does not express what he/she supposed these expressed ?

One component of the chain may still be a source of matters : the one from  
a though to a specification.

I agree testing is a least a bit needed for that. However, this is not to  
be driven as the other kind of testing, which is very different, I mean  
the one which is driven when nothing else can be done (or no body wanted  
to do something else).


-- 
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.