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,da5197b9dca0ed40
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news1.google.com!news.glorb.com!transit3.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail
Message-Id: <4c14e5dc$0$2382$4d3efbfe@news.sover.net>
From: "Peter C. Chapin" <pcc482719@gmail.com>
Subject: Re: Processing array subsections, a newbie question.
Newsgroups: comp.lang.ada
Date: Sun, 13 Jun 2010 10:09:18 -0400
References: <4c13db30$0$2391$4d3efbfe@news.sover.net>
 <8739wsottd.fsf@ludovic-brenta.org> <87jc41FftrU1@mid.individual.net>
User-Agent: KNode/0.10.9
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7Bit
Organization: SoVerNet (sover.net)
NNTP-Posting-Host: 1e5216c9.news.sover.net
X-Trace: 
 DXC=2Mi>3@BVoKKSHGN<7KP`INK6_LM2JZB_CJ5R`gYClY@N:WUUlR<856OaYdb@>clhYNkTXQbV>kf3O
X-Complaints-To: abuse@sover.net
Xref: g2news2.google.com comp.lang.ada:12648
Date: 2010-06-13T10:09:18-04:00
List-Id: <comp.lang.ada>

Niklas Holsti wrote:

> Constraint_Error would be raised only if Index_Lst = Natural'Last after 
> Do_Something. By subtyping the index type of Buffer you could ensure 
> that Buffer'Last < Natural'Last, which would avoid the risk of 
> Constraint_Error. (Perhaps this is the ungainly work-around that you 
> mention.)

In fact that is exactly what I'm doing now. I'm not sure if "ungainly" is the
right word to use but my concern is that now I'm using a variable to index
the array that has a subtype that can, in principle, extend outside of the
array. I haven't yet tried to prove my program free of run time errors using
SPARK but I anticipate that doing so will be harder than it might otherwise
be because of this situation. My experience with SPARK so far is that it is
very desirable to express precise intentions with one's subtypes.

On the other hand the code fragment I showed before won't prove at all, of
course, since it could in fact raise Constraint_Error. The early loop exit
approach might be workable for me. I didn't really think of that. I might
have to reorganize a few things, but I'm used to that!

Thanks for the suggestion.

Peter