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,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news2.google.com!postnews.google.com!g17g2000yqe.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: SPARK - Bubble Sort on Rosetta Code
Date: Thu, 26 Aug 2010 02:18:20 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <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
X-Trace: posting.google.com 1282814300 11384 127.0.0.1 (26 Aug 2010 09:18:20
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 26 Aug 2010 09:18:20 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: g17g2000yqe.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:13753
Date: 2010-08-26T02:18:20-07:00
List-Id: <comp.lang.ada>

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

I've used the Ada version on there as the starting point, with Integer
for the stored element and for the array index,

There are three versions:

The first is simply shown to be type-safe.

The second, with identical Ada code, proves that the output array is
sorted. This requires just two simple proof rules as the inner loop
scans the complete array for every pass of the outer loop.

The third version scans a reducing portion of the array in the inner
loop and this makes the proof quite a bit more complex. My main
concern is that the number of proof rules that this requires could
look rather frightening to a casual browser and do more harm than
good.

Cheers,

Phil