Re: Q: SPARK visibility rules and inherit annotations.

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

Le Fri, 21 May 2010 12:42:53 +0200, Gavino <invalid@invalid.invalid> a  
écrit:
> Firstly, derived types can introduce overloaded enumeration literals,  
> which
> SPARK prohibits.
> Secondly, if the parent type is one declared immediately within the  
> visible
> part of a package, then certain subprograms declared there are implicitly
> declared for the derived type, again a form of overloading.
Yes, I forget about it, and especially about the first one (about  
enumeration literals).

This part of the one which is the most troublesome to me with SPARK, as I  
like to “type ... is new ...” some types are not be mixed and the  
interface defines special function when it is required. At least, when  
mixed is done, this is clearly visible and this is a clear indication on  
source review to look at it three times better than two.

Subtype is nice with SPARK, as validity conditions are checked. But if the  
source is to be as nice with and without SPARK, some troubles comes :  
subtype are not so much nice without SPARK. Ada with SPARK less needs  
derived types, and subtype is enough, but Ada without SPARK, needs derived  
types. So I can't have something which is good without SPARK too... or I  
have to make all numeric types independent, but doing so, I miss the  
expression of relations between these types.

Any way, thanks for your reply, which was the good one (this recalled me a  
detail I had forget, as I'm not really relying on it).

-- 
There is even better than a pragma Assert: a SPARK --# check.