Re: Is Aunit helpful?

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

Le Sun, 15 Aug 2010 23:47:21 +0200, Midoan <midoan.ses@gmail.com> a écrit:
> In practice, and for example, Ada 2012's post-conditions are unlikely to
> be used to capture the full effect of commercial, safety critical,
> code ... That, to our eyes, is a major weakness in specification based
> verification : the specification may say 'A' but the code may do 'A
> and B' ... and trying to model 'B' in the specification typically
> leads to  specifications as complex as the code!

Well, I like the idea of Ada 2012 pre-post (while still not tried) the Ada  
version of this (I did with the Eiffel one).

I already used this, with Eiffel, and my memory tells me I cannot remember  
any case where this really helped and fixing a bug (you will laugh, but  
even the SmallEiffel compiler source, was containing nothing that here and  
there some seed of toy contract-assertions, very poor use in SmallEiffel  
itself). Either the pre-post was erroneously expressed (and ended into  
signaling violation which was not error) or this was missing some  
important part which could then not be detected. Thus, I agree with you  
about the “weak”. I would even add “possibly wrong” (may be worse than  
weak).

 From there, I would like to get to three points.

1) After my experiences with Eiffel, pre-post could be either erroneous or  
missing something, for a simple reason: this is not statically checked,  
this is only runtime checked... so it is far too much easy to fail at  
design time! (event in a recursive design process, this does not really  
change anything) If this was statically checked, this would be deeply  
different. The weakness here is not due to pre-post concept, but rather to  
static check vs runtime check.

2) Your comment makes me think what you would better enjoy, would be  
reification. You would not have any more troubles with “said A but did A  
and B”, as A and B would have been produced during a process and would be  
under control of this process (there woul be an explicit track forth and  
back to and from this A and B).

3) About point #1, just wanted to say I don't want here to discourage  
people interested in pre-post introduced in Ada 2012, to use it. No-no-no,  
if they enjoy this, this is very good, and this will lead them to a good  
way. Just wanted to say what should not be hidden: this is weak, as this  
is more a step above comments. I was to say “this is just like  
comments”... but honestly, comment are not checked at all, so these  
pre-post may be viewed as “Better Comments”.

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