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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM 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!postnews.google.com!q22g2000yqm.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome Date: Tue, 17 Aug 2010 02:15:44 -0700 (PDT) Organization: http://groups.google.com Message-ID: 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> NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1282036544 21685 127.0.0.1 (17 Aug 2010 09:15:44 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 17 Aug 2010 09:15:44 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: q22g2000yqm.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:13449 Date: 2010-08-17T02:15:44-07:00 List-Id: On 17 Aug, 00:43, "Peter C. Chapin" wrote: > On 2010-08-16 18:38, Yannick Duch=EAne (Hibou57) wrote: > [...] > > For the time, unless some news comes in the place, I will end with this > > conclusion: SPARK's not a language, that's Praxis's tool. > > When people ask me what SPARK is about I tell them it's an annotated > subset of Ada together with a tool set that can be used for deep static > analysis of that annotated language. It seems to me that SPARK is both a > language and a tool. > > Perhaps this gets back to a question Phil raised: does it make sense on > Rosetta to differentiate between SPARK and SPARK+proofs? 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. [Which is a Very Good Thing(TM) - new users can start by ignoring proof completely. Then start proving that the code is type safe without having to even think about formal specifications - and complete their type safety proofs ranging from the completely informal (proof by review) up to the completely formal (check annotations, where they work, and the Proof Checker otherwise). Then move into the formal spec world of contracts expressed through pre and post conditions.] I'm going to try and come up with an explanation of SPARK for Rosetta Code that covers all the ground, but is as succinct as possible (so no- one should be holding their breath for that). I'll link out to detailed descriptions where possible. [...] > > By the way, if this is really a Praxis's tool as I suppose now, do I > > have to understand there will be always one single implementation of > > SPARK and a single provider in this area ? > > That's an interesting question. > > Oracle is suing Google over Google's use of Java in Android. I suppose > this is the nasty quagmire one gets into whenever one starts using > proprietary languages. Thankfully Ada has an international standard so > the Ada community can avoid some of that. 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. The tools are now GPL'ed, but the documentation is all copyright Altran-Praxis and the SPARK LRM is also Crown Copyright (probably after some early funding from the UK MoD). I don't know enough about these issues to say what effect that has on restricting other organisations' ability to develop new versions of the language and tools. > ... 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. Cheers, Phil