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,103b49cd5a4719fd X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,CP1252 Path: g2news1.google.com!postnews.google.com!l6g2000yqb.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK - Bubble Sort on Rosetta Code Date: Fri, 27 Aug 2010 00:35:51 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <5688938b-2047-4fef-9ea2-730abb761d07@g17g2000yqe.googlegroups.com> NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1282894551 30712 127.0.0.1 (27 Aug 2010 07:35:51 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 27 Aug 2010 07:35:51 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: l6g2000yqb.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:13771 Date: 2010-08-27T00:35:51-07:00 List-Id: On 26 Aug, 22:40, Yannick Duch=EAne (Hibou57) wrote: > Le Thu, 26 Aug 2010 11:18:20 +0200, Phil Thornley =A0 > a =E9crit: > > > I've put some SPARK code for the Bubble Sort task on Rosetta Code and > > I would welcome opinions on whether they make a good showcase for > > SPARK > > Personal opinion: I still do not feel user rules are nice (and this case = =A0 > confirms my opinion to me). > But in the large, I agree, except with the length and the weight of user = =A0 > rules of the last examples compared to the source. But of the 11 rules for the last example, only two of them do not involve a proof function reference. If you have proof functions then you have to have proof rules for them. > Just a tiny detail and a less tiny > =93--# derives A from A;=94 may be clearer than =93--# derives A from *;= =94 My style is always to use '*' for self-dependency to give it a strong visual emphasis. Self-dependency is different as it can be created by the absence of code, whereas all other dependencies require the presence of code. > May be nice to say there are two level of usage of SPARK: proof of =A0 > semantic and proof of runtime-error free. It is implicit in the first cas= e =A0 > (as it talks about free of runtime error), but this may be nice to tell = =A0 > about it explicitly. That is essentially covered in the (fairly brief) description of SPARK in it's language page. > May be this would be better to state this in the page you created about = =A0 > the proof process. > > In the page The SPARK Proof Process > > =93The verification conditions generated depend on the annotations that h= ave =A0 > been specified in the SPARK source and the properties that they specify.= =94. > > This miss to tell about validation condition created based on the type = =A0 > system. This does not requires annotations. > > =93This normally proves 95-99% of all verification conditions.=94 > > This is more likely to be true only when only free-of-runtime-error is a = =A0 > concern. The distinction should be made here. I can see a couple of improvements to the wording here, so I'll think about these suggestions as well. Thanks, Phil