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,ASCII Path: g2news1.google.com!postnews.google.com!z28g2000yqh.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:57:33 -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=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1282895853 9424 127.0.0.1 (27 Aug 2010 07:57:33 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 27 Aug 2010 07:57:33 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: z28g2000yqh.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:13772 Date: 2010-08-27T00:57:33-07:00 List-Id: On 26 Aug, 23:32, Simon Wright wrote: > Phil Thornley writes: > > 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 > > It took me a while to find them -- at http://rosettacode.org/wiki/Sorting= _algorithms/Bubble_sort#SPARK. Ooops, sorry about not including that. > > The first is simply shown to be type-safe. > > Is this the same as "guaranteed free of any run-time error"? Yes - the Wikipedia page on type safety (http://en.wikipedia.org/wiki/ Type_safety) says "In the context of static (compile-time) type systems, type safety usually involves (among other things) a guarantee that the eventual value of any expression will be a legitimate member of that expression's static type." I've always wanted a shorter phrase than "proof of absence of run-time error" and Rod used the phrase type-safe in his recent announcement about SPARKSkein. > What would non-SPARK code do to make it fail? Get one of the bounds on the inner loop wrong? Get the termination condition wrong for the outer loop and increment the pointer past the end? > > The second, with identical Ada code, proves that the output array is > > sorted. > > Are zero-length arrays forbidden in SPARK? Yes - any array must use a named index subtype, and null subtype ranges are forbidden (which can be checked by the Examiner because the bounds of subtype ranges must be static). > ... I ask because of > > =A0 =A0 =A0 --# check A'Last <=3D A'First -> A'Last =3D A'First; That's an example of a 'tactical' check annotation that helps with proing some of the VCs. (It converts a potential path into an infeasible one, which makes it a lot easier to prove the post- condition.) > (what's that -> ? I understood that the syntax was > =A0 =A0'check '). That's the SPARK implication operater. Cheers, Phil