Re: Lost in translation (with SPARK user rules)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 26 May 2010 21:28:58 +0200, Yannick Duch�ne (Hibou57) wrote:

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

No run time checks, but an option to tell more about the contract, with
enforced static checks, that this indeed hold. If you have no time, no
guts, or when the algorithm does not allow certain proofs, you just do not
make promises you cannot keep and go further.

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

I think it should be more than just two levels. But yes, each language
construct and each library operation shall have a contract.

> Actually, how can you test an compiler  
> compliance with SPARK ? I feel you can do it only for full Ada.

Likely yes, because there exist legal Ada programs, such that no Ada
compiler could compile.

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

Rather by refining the contracts. When you feel that the implementation is
mature, you can add more promises to the contract of and see if they hold
(=provable). If they don't you could try to re-implement some parts of it.
When you feel that it takes too much time, is impossible to prove, you can
drop the idea to do it formally. You will sill have a gain of deeper
understanding how the thing works and could document why do you think it is
correct, even if that is not formally provable.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de