Re: ANN: Ada 2005 Math Extensions, 20100810 release

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

Le Fri, 13 Aug 2010 10:40:57 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> Do you mean the use case or the offending code? I cannot say for the  
> latter
> because I have no idea when it happens and if the code is legal [*]. The
> simplest possible use case is the diamond diagram of generic packages  
> [**]:
>
>   A
>  / \
> B  C
>  \ /
>   D
>
> In the specification of D you have to constrain B and C to the same A.

This may also occurs if you wanna do some Mixins. This was how I came to  
it the first if my mind is right.

> ** We were told how dreadful the diamond is, so bad that Ada may not  
> allow
> to have MI, but for sacred generics anything is perfectly OK!
Did not understood this sentence, at least the last “but for sacred  
generics anything is perfectly OK!”


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