Re: Q: SPARK visibility rules and inherit annotations.

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

Le Wed, 19 May 2010 23:29:22 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> One thing I like about Ada in general is how you can express a design in
> package specifications and then let the compiler check a few things  
> about its
> consistency before embarking on the implementation. With SPARK that  
> effect is
> even greater. For example in my Cryptographic_Services package the  
> Examiner
> initially complained about how there was no way to initialize one of my
> private types.
I've noticed the same, it requires some good practice to be applied,  
someway comparable to what you could get with AdaControl and a good rules  
file (I mean AdaControl's rules). As an example, SPARK sees an error if  
you forget the give the name of procedure at its end statement.

While sometime, I would like to better understand some choices, like the  
one I've meet, which is that it does not accept nested package  
specifications, or, more important, why it don't wants “type ... is new  
...;”. If I could understand the rational behind this latter restriction,  
this could perhaps help me to redesign.