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.227.166 with SMTP id sb6mr1230645pbc.4.1332267496764;
        Tue, 20 Mar 2012 11:18:16 -0700 (PDT)
Path: 
 kz5ni13165pbc.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!news.stack.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!prichard.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: Tue, 20 Mar 2012 18:18:12 -0000
Message-ID: <MPG.29d2da3de11de090989696@news.zen.co.uk>
References: <aYCdndGkyL_dCc7S4p2dnAA@giganews.com>
 <MPG.29bdc816fbebb1ae989692@news.zen.co.uk>
 <vpqdnYMbkompW87S4p2dnAA@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: 0081ba0c.news.zen.co.uk
X-Trace: 
 DXC=O\eXjdBRc2:<XSEjV8EfN10g@SS;SF6n7ge[^m9THnR?O;g_DWVnoX3gPN:7kYdTY;_l94d][hC_9
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-03-20T18:18:12+00:00
List-Id: <comp.lang.ada>

In article <vpqdnYMbkompW87S4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu
says...

[snip]
> I did notice, however, that there was a hypothesis that talked about
> Event_Array(i__loop__2__entry). It seemed to me that the hypothesis was
> somewhat related to my conclusion so as a guess I tried
> 
> --# assert Event_Array(I).Description_Size <= Description'Length and --# I
> = I% and --# (J - 1) < Description'Length;
> 
> That worked! However, I'm still trying to understand the general principle
> that can guide me in these situations. I feel like I have to resort to
> semi-random attempts until I stumble into something that works.

Peter,

The clue to the fact that you needed to add I=I% is in the hypotheses.

I put enough code around the code in your initial post to get the VC that
you also posted.

Then, with the additional condition, there are two particular hypotheses:
H2:    fld_description_size(element(event_array, [i])) <=
          description__index__subtype__1__last .
H13:   loop__2__j < fld_description_size(element(event_array, [
          i__entry__loop__2])) .
where the conclusion is:
C1: loop__2__j < description__index__subtype__1__last .

so by including I=I% in the loop invariant (which becomes i=i__entry__loop__2 
in the VC) the conclusion is provable.

Cheers,

Phil

(You may well think that the way that VCs are presented makes it very 
difficult to spot this sort of thing. If this VC is read by VC_View then it 
becomes:

For path(s) from assertion of line 72 to assertion of line 72 
H1:    A - 1 < B__last .
H2:    fld_description_size(element(event_array, [i])) <= B__last .
H5:    A <= 128 .
H6:    A >= 1 .
H11:   element(fld_description_text(element(event_array, [i])), [A]) >= 0 .
H12:   element(fld_description_text(element(event_array, [i])), [A]) <= 255 .
H13:   A < fld_description_size(element(event_array, [i__entry__loop__2])) .
H22:   B__last >= 0 .
H23:   B__last <= 2147483647 .

C1:    A < B__last .

A       = loop__2__j
B__last = description__index__subtype__1__last

which makes it a bit easier to spot.)