From: Maciej Sobczak <see.my.homepage@gmail.com>
Subject: Re: SPARK problem with unconstrained arrays
Date: Tue, 3 Mar 2015 01:41:33 -0800 (PST)
Date: 2015-03-03T01:41:33-08:00 [thread overview]
Message-ID: <00de73ba-0430-4528-9f10-cf664a70fa02@googlegroups.com> (raw)
In-Reply-To: <56938449-64e8-4e9c-89ef-8d7fa914c9eb@googlegroups.com>
> Adding this just before line 8 helps:
>
> pragma Assume (A'First in A'Range);
After some exploration I can answer my own question: empty slices.
Solution: add precondition to the Find_Min procedure:
procedure Find_Min (A : in My_Array; I : out Index)
with Pre => A'First <= A'Last,
-- ...
The earliest added value of formal methods (and SPARK in particular) is in showing us how much we assume of what might not be actually true...
--
Maciej Sobczak * http://www.inspirel.com/
next prev parent reply other threads:[~2015-03-03 9:41 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 [this message]
2015-03-04 21:31 ` Jacob Sparre Andersen
2015-03-04 22:31 ` Maciej Sobczak
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