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: 103376,6d79efdb8dde2c5a X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!194.25.134.126.MISMATCH!newsfeed01.sul.t-online.de!t-online.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Categories for SPARK on Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome) 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: <82mxsnuhbq.fsf@stephe-leake.org> <4c69a251$0$2371$4d3efbfe@news.sover.net> <4c69cd5f$0$2375$4d3efbfe@news.sover.net> <1ddee5a6-fc25-4d23-bebd-3364923d0aa5@z10g2000yqb.googlegroups.com> <7cf71c68-4faf-4a7b-a350-405ff7f12ff9@z10g2000yqb.googlegroups.com> <4xb6sjkpzo1r$.138841gile5s0$.dlg@40tude.net> <87wrrnjf9f.fsf_-_@hugsarin.sparre-andersen.dk> <3ed38f7f-372d-422e-9bda-eca8a73d3f0d@x21g2000yqa.googlegroups.com> <1ncf62lqqj7ab$.1czxyaw96dl17.dlg@40tude.net> <1y0wcz3etd5au.1kgyc5ls0w5kk$.dlg@40tude.net> Date: Fri, 20 Aug 2010 16:05:01 +0200 Message-ID: NNTP-Posting-Date: 20 Aug 2010 16:04:57 CEST NNTP-Posting-Host: 7dfe3522.newsspool3.arcor-online.net X-Trace: DXC=b6]<0hjT=?Lj7E:bke<5HFMcF=Q^Z^V3H4Fo<]lROoRA8kFRT5KG[6LHn;2LCVN[ On Fri, 20 Aug 2010 15:28:31 +0200, J-P. Rosen wrote: > Le 20/08/2010 14:25, Dmitry A. Kazakov a �crit : >>> No. As soon as you have address arithmetic, no semantic can be >>> guaranteed. Well, it depends on what you call "formally" TBH. >> >> But the definition does not hint what kind of properties have to be >> analyzed (and when). > It's on purpose. A category should be broad enough. We can discuss > whether "static" should be put in, but I think it is important to keep > "formal". Yes 1. Formal in the sense that there is a specification. 2. Static, that verification happens before run time. >> You mean the case when the code "supporting analysis" is dead code! What >> kind of "support" is to include unreachable code? > Of course. Spark's annotation have no effect on correct programs. They do, because correctness itself depends on the annotation. If you change the annotation, the program may become incorrect. Dead code does not have this property. > It would make no sense to introduce a category "has Spark annotations". Yes. > We need something broader. And a minimum of honesty is needed when > checking the box. The only issue is to make sure that the casual reader > understands that it means: "has special features directed specifically > to analysis". Could be "has assertions", but that seems too restrictive > to me. So please, if you have a better idea, I'd be delighted to hear > about it. I thought about a specific approach to programming, as it was proposed by Dijkstra, with designing both the program and a proof that certain properties of the program hold. SPARK's annotations support this approach. This is not specific to SPARK. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de