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.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no
	version=3.4.4
X-Google-Thread: 103376,1d1caf8fb79ff030
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.201.129 with SMTP id ka1mr4538118pbc.6.1330886583611;
        Sun, 04 Mar 2012 10:43:03 -0800 (PST)
Path: 
 h9ni39184pbe.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!txtfeed2.tudelft.nl!tudelft.nl!txtfeed1.tudelft.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!shaftesbury.zen.co.uk.POSTED!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK loop VCs that go "one beyond" the loop?
Date: Sun, 4 Mar 2012 18:43:02 -0000
Message-ID: <MPG.29bdc816fbebb1ae989692@news.zen.co.uk>
References: <aYCdndGkyL_dCc7S4p2dnAA@giganews.com>
Reply-To: phil.jpthornley@gmail.com
MIME-Version: 1.0
User-Agent: MicroPlanet-Gravity/3.0.4
Organization: Zen Internet
NNTP-Posting-Host: 322eefa8.news.zen.co.uk
X-Trace: 
 DXC=3G?kLolk3@jG<aQSeV28Klnok4Z\<mH4ihDU:2=XKPkhBkCKY;S]7W`=CLe5aAFkie514Ya;;:6oj
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-03-04T18:43:02+00:00
List-Id: <comp.lang.ada>

In article <aYCdndGkyL_dCc7S4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...
[...snipped...]

Peter,

I would like to give a more considered reply than I have time for just 
now, however:

I am fairly sure that what you need to add to the assertion is the 
result of the earlier check:
   Event_Array(I).Description_Size <= Description'Length

You may also need to state that the upper bound on J is not changed by 
the loop body:
   Event_Array = Event_Array%

Cheers,

Phil


> P.S. I posted a message earlier about discharging a post condition with 
> a quantified expression. I just want you (Phil) to know that I read your 
> message but I haven't had time to work with that example since. I did 
> get an insight about it, however, so I want to reflect on that insight 
> for a bit. I'll post again if I have more questions. Thanks for your help!

If there's too much code to post to news then feel free to mail it to me 
- the address is on the sparksure web site if you don't still have it.