Re: GNAT packages in Linux distributions

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

Le Thu, 27 May 2010 14:47:15 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> Notation is not such unimportant.
>
> And this is a bit more than just notation: You use different *tools* to
> compile the program-while-ignoring-all-annotations and to check the
> additional information provided by the annotations. This means, that
> psychologically the information in the annotations appears to be the  
> "less
> important" stuff.
Do not make this a rule, as this depends on one's expectations (so  
receptivity to that what looks like his/her expectations). One who wish  
and expect what belongs to these annotations, will see these as important  
things. One who does not expect these annotations and may perhaps even  
wish that would not exist (like a student working on an assignment) will  
see these as non so much important.

This is a matter of receptivity.

I was a bit wrong (did a shortcut) when I suggested “this is just  
annotation”, as I agree the form of an annotation is important for  
readability.

> E.g., a badly flawed SPARK program may still be compiled
> by an Ada compiler,
Yes

> but a syntactically incorrect Ada-program will be
> found flawed by the SPARK tools.
Not a rule, as not all notations oriented language may check every thing  
of the host language. SPARK does, but I'm pretty sure not all do (I think  
we were talking about the general case here, not only about the SPARK  
special case).



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