From: Maciej Sobczak <see.my.homepage@gmail.com>
Subject: Re: SPARK problem with unconstrained arrays
Date: Wed, 4 Mar 2015 14:31:47 -0800 (PST)
Date: 2015-03-04T14:31:47-08:00 [thread overview]
Message-ID: <01197172-98dd-4e30-ad37-494ded69bded@googlegroups.com> (raw)
In-Reply-To: <87sidkv49r.fsf@adaheads.sparre-andersen.dk>
> > 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
next prev parent reply other threads:[~2015-03-04 22:31 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2015-03-03 9:29 SPARK problem with unconstrained arrays Maciej Sobczak
2015-03-03 9:41 ` Maciej Sobczak
2015-03-04 21:31 ` Jacob Sparre Andersen
2015-03-04 22:31 ` Maciej Sobczak [this message]
2015-03-13 22:15 ` Shark8
2015-03-24 23:03 ` phil.clayton
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox