Re: GNAT packages in Linux distributions

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

Le Wed, 12 May 2010 10:41:03 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> it lacks the option to specify (and verify, of course) variants for
> WHILE-loops (**). Eiffel supports such
> invariants.
I was to ask you if you were really sure, ... you've already requested for  
more comments in the P.S., so may not give me an answer.
Well, you may also see a loop as an abstraction surrounded by pre and post  
and requires the previous state in some the same as the new one after each  
iteration (just a beginner's two cents idea)

> P.S.:  I have worked a bit with SPARK, and I am currently trying to
>        improve my knowledge about it. While I do prefer static analysis
>        over Eiffels dynamic checking at run time, I still think Eiffel's
>        approach has its place. The constraints of SPARK as a programming
>        language are severe. (For me, the worst is the prohibition of
>        recursive subprograms.)
I'm just starting with SPARK, so I may be wrong : it seems to me recursion  
is allowed if the stack usage is bounded (keep in mind I may be wrong).

-- 
pragma Asset ? Is that true ? Waaww... great