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-7-bit Path: g2news1.google.com!news1.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!198.186.194.249.MISMATCH!transit3.readnews.com!transit4.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail Date: Tue, 17 Aug 2010 06:32:16 -0400 From: "Peter C. Chapin" User-Agent: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.2.8) Gecko/20100802 Lightning/1.0b2 Thunderbird/3.1.2 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome References: <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com> <82mxsnuhbq.fsf@stephe-leake.org> <4c69a251$0$2371$4d3efbfe@news.sover.net> <4c69cd5f$0$2375$4d3efbfe@news.sover.net> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Message-ID: <4c6a6555$0$2382$4d3efbfe@news.sover.net> Organization: SoVerNet (sover.net) NNTP-Posting-Host: ba27b651.news.sover.net X-Trace: DXC=:VGWBQEEndS54WfImF>H4_K6_LM2JZB_SJ5R`gYClY@^:WUUlR<856_W;K?C6Qm:dVFgUi4^KFKdR X-Complaints-To: abuse@sover.net Xref: g2news1.google.com comp.lang.ada:13452 Date: 2010-08-17T06:32:16-04:00 List-Id: On 2010-08-17 05:15, Phil Thornley wrote: > I've thought about that one a bit more and decided that it's probably > not a good idea - using SPARK is much more of a continuum of > approaches. I've noticed this as well and I agree that it is a good thing. Sometimes I use SPARK to try an prove quite a bit. Sometimes I just try to prove freedom from run time errors. Sometimes I just use the flow analysis and stop there. All of these options get followed at different places in the same program depending on time, effort required, criticality, etc. I suppose it's the same with any kind of analysis tool and it's reflective of the tool-like nature of SPARK. >> However, there is no >> international standard for SPARK. At least not as far as I know. > > That was one of the first questions that the Annex H Rapporteur Group > looked at when it was formed following the publication of the Ada95 > standard. Should the Group define a 'safe subset' for Ada and, if so, > should that subset be SPARK? The Group fairly quickly decided against > defining a standard subset so the question about SPARK never arose. That's interesting to know. I can see why the group did not want standardize a safe subset. After all many different subsets could be imagined and what constitutes "safe" is going to depend on the application and on the analysis technology available. As I understand it SPARK has evolved as analysis techniques have improved. It will probably continue to do so. Other, similar systems with slightly different needs could potentially exist using different subsets as well. >> ... Will it become the Java of the formal methods community? > > Not until Altran-Praxis start making a great deal more money out of it > than they do at present. I'm not really worried about it. Still it would be great if interest in SPARK or SPARK-like systems became so widespread that people did start worrying about it! Peter