From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,ec6f74e58e86b38b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!news3.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!83.128.0.11.MISMATCH!news-out1.kabelfoon.nl!newsfeed.kabelfoon.nl!xindi.nntp.kabelfoon.nl!newsfeed00.sul.t-online.de!newsfeed01.sul.t-online.de!t-online.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Lost in translation (with SPARK user rules) Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com> <4bfd2d05$0$27598$ba4acef3@reader.news.orange.fr> Date: Wed, 26 May 2010 22:14:48 +0200 Message-ID: <1jo6gjejsy828$.e9dx6txqbazd$.dlg@40tude.net> NNTP-Posting-Date: 26 May 2010 22:14:45 CEST NNTP-Posting-Host: b0482ab1.newsspool3.arcor-online.net X-Trace: DXC=ZcIjm:WDRJJ@Y=h<_c3PkHMcF=Q^Z^V3H4Fo<]lROoRA8kF 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 > 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