Re: SPARK : surprising failure with implication

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

Le Wed, 02 Jun 2010 10:55:48 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> Disproving the antecedent from wrong consequent is not very common.
It is to me, and not only with SPARK rules, this is why I though to use it  
in this context.

Thanks to have pointed this may not seems common to every one, as I was  
not aware of this.

> None, except that what looks obvious for a man is not for a computer and
> conversely. (:-))
You are right Dmitry ;) That is a nice sentence in all of its  
interpretations.


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