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!k10g2000yqa.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK : third example for Roesetta - reviewers welcome
Date: Sun, 15 Aug 2010 21:29:24 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <99389e3d-17da-40a4-a25f-0bcfb1e7c104@k10g2000yqa.googlegroups.com>
References: <op.vhguffh3ule2fv@garhos>
 <87aaonlk1h.fsf@hugsarin.sparre-andersen.dk>
 <op.vhhxe1caxmjfy8@garhos> <i49mrv$19s4$1@adenine.netfront.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 1281932975 19768 127.0.0.1 (16 Aug 2010 04:29:35
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 16 Aug 2010 04:29:35 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: k10g2000yqa.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:13381
Date: 2010-08-15T21:29:24-07:00
List-Id: <comp.lang.ada>

On 15 Aug, 22:40, Jeffrey Carter <spam.jrcarter....@spam.not.acm.org>
wrote:
> On 08/15/2010 01:19 PM, Yannick Duch=EAne (Hibou57) wrote:
>
> > --# pre
> > --# (Source'Length =3D 0) or else
> > --# (for all I in Index_Type range Source'First .. Source'Last - 1
> > --# =3D> (Source (I) <=3D Source (I + 1)));
> > -- The array must be either empty or sorted from lower to higher.
>
> Is this correct? Consider the case where Source'Length =3D 1. In that cas=
e, the
> range in the "for all" is null; does that evaluate to True? If not, then =
it
> needs to be
>
> Source'Length < 2 or else (for all ...)

That's the correct way of saying that the array is ordered, and it
works fine for an array of Length 1 (or less).

The translation of that expression to FDL (the language SPARK uses for
all it's proof work) will be something like:
 for_all(i_ : integer, source__first <=3D i_ and i_ <=3D source__last - 1
            -> (element(source, [i_]) <=3D element(source, [i_ + 1]))) .
If source__first =3D source__last then the LHS of the implication is
False, and the implication itself is True.

> Even if it is correct as written, it may be misleading to non-Ada readers=
 (whom
> we want to impress on Rosetta) who might think it implies an out-of-range=
 access.

That's why I used the proof function 'Ordered' in my version of the
code.  To the casual reader it should look OK, and when you want to
get more formal then you define Ordered as exactly that expression
above.

Cheers,

Phil