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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham 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!feeder.news-service.com!85.214.198.2.MISMATCH!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail From: "J-P. Rosen" Newsgroups: comp.lang.ada Subject: Re: Categories for SPARK on Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome) Date: Fri, 20 Aug 2010 15:28:31 +0200 Organization: Adalog Message-ID: 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> Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Injection-Date: Fri, 20 Aug 2010 13:28:53 +0000 (UTC) Injection-Info: mx03.eternal-september.org; posting-host="Dn22F68J9CHYFQQlT81DGA"; logging-data="6032"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX198FuEKxO0uk9ubN4iQjPSy" User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; fr; rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2 In-Reply-To: Cancel-Lock: sha1:h63tDExI7yYK06JKHjfo00KktuQ= Xref: g2news1.google.com comp.lang.ada:13538 Date: 2010-08-20T15:28:31+02:00 List-Id: 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". > 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. > If it supports anybody, > then memory chips vendors. Then a dynamically typed language with its > "message not understood" would qualify for the same reasons as Eiffel. > Anybody can argue about what "formal verification" means, but the same is true of "strongly typed". Even in C, there are cases of code that does not compile because of type mismatches... It would make no sense to introduce a category "has Spark annotations". 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. -- --------------------------------------------------------- J-P. Rosen (rosen@adalog.fr) Visit Adalog's web site at http://www.adalog.fr