Re: SPARK loop VCs that go "one beyond" the loop?

[Phil Thornley <phil.jpthornley@gmail.com>]

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.)