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!a36g2000yqc.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK - Bubble Sort on Rosetta Code
Date: Fri, 27 Aug 2010 02:02:51 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <d7a4c582-4709-4067-b993-2ad231562004@a36g2000yqc.googlegroups.com>
References: 
 <5688938b-2047-4fef-9ea2-730abb761d07@g17g2000yqe.googlegroups.com>
 <m2r5hlatuf.fsf@pushface.org>
 <eefb617d-9b91-4569-9baf-9697ca455752@z28g2000yqh.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 1282899771 10441 127.0.0.1 (27 Aug 2010 09:02:51
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 27 Aug 2010 09:02:51 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: a36g2000yqc.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:13774
Date: 2010-08-27T02:02:51-07:00
List-Id: <comp.lang.ada>

On 27 Aug, 08:57, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> On 26 Aug, 23:32, Simon Wright <si...@pushface.org> wrote:> Phil Thornley=
 <phil.jpthorn...@gmail.com> writes:
> > =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0=
 =A0 =A0... 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.)

I thought about that a bit more and realised that it isn't necessary.
(Must have got left there from an earlier version of the code.)

So I've removed it from both of the versions it appeared in.

Cheers,

Phil