Re: Lost in translation (with SPARK user rules)

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

Le Wed, 26 May 2010 16:28:20 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> Yes. I think this could be a direction in which Ada should evolve. It
> should have a modular part equivalent to SPARK, which can be used with
> certain compilation units. So that the programmer could choose the level  
> of
> safety he is ready to invest into.

Please, tell more : you mean a kind of pragma or compiler option like the  
ones there is for runtime checks ?

By the way, that's an opportunity for two other ideas : why not integrate  
the SPARK language definition in the Ada standard ? We may have wordings  
in the Ada reference or the annotated reference, stating that is and that  
is allowed or disallowed with SPARK. And second thing, related to this  
latter : why not an ACAT tests suit targeting SPARK/Ada compilation  
capabilities beside of full Ada ? Actually, how can you test an compiler  
compliance with SPARK ? I feel you can do it only for full Ada.

> It would be nice to be able to start the project at some middle level (a
> bit higher than of present Ada, but lower than SPARK), and then gradually
> adjust it, as the project evolves.
Like ensuring it is written in a valid SPARK syntax before we know if this  
part will really be semantically checked or not ?

> Another 2 cents.
Re-no, re-was re-valuable


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