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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.236.220.74 with SMTP id n70mr7349891yhp.40.1425508308331;
 Wed, 04 Mar 2015 14:31:48 -0800 (PST)
X-Received: by 10.140.102.82 with SMTP id v76mr127202qge.25.1425508308044;
 Wed, 04 Mar 2015 14:31:48 -0800 (PST)
Path: 
 border2.nntp.dca1.giganews.com!nntp.giganews.com!w8no584888qac.0!news-out.google.com!qk8ni49442igc.0!nntp.google.com!w8no584884qac.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Wed, 4 Mar 2015 14:31:47 -0800 (PST)
In-Reply-To: <87sidkv49r.fsf@adaheads.sparre-andersen.dk>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=213.108.152.51;
 posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
NNTP-Posting-Host: 213.108.152.51
References: <56938449-64e8-4e9c-89ef-8d7fa914c9eb@googlegroups.com>
 <00de73ba-0430-4528-9f10-cf664a70fa02@googlegroups.com>
 <87sidkv49r.fsf@adaheads.sparre-andersen.dk>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <01197172-98dd-4e30-ad37-494ded69bded@googlegroups.com>
Subject: Re: SPARK problem with unconstrained arrays
From: Maciej Sobczak <see.my.homepage@gmail.com>
Injection-Date: Wed, 04 Mar 2015 22:31:48 +0000
Content-Type: text/plain; charset=ISO-8859-1
Xref: number.nntp.giganews.com comp.lang.ada:192417
Date: 2015-03-04T14:31:47-08:00
List-Id: <comp.lang.ada>

> >     procedure Find_Min (A : in My_Array; I : out Index)
> >         with Pre => A'First <= A'Last,
> >              -- ...
> 
> Wouldn't "A'Length >= 1" be more readable?

I would like to write:

not A'Empty

:-)

A'Length introduces new name and one constant into the whole mix, but indeed might be easier to read.

-- 
Maciej Sobczak * http://www.inspirel.com