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

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

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

> Thanks for your comments. They are helpful, as always. The problem I'm 
> having, in general (no longer related to any specific VC), is that if 
> the loop assertion mentions the loop index variable there is a tendency 
> for SPARK to generate an unprovable VC of the form
> 
> Hx: loop__1__i <= some_array__index__subtype__1__last
> ...
> Cy: loop__1__i + 1 <= some_array__index__subtype__1__last
> 
> This is for the path from the assertion to the assertion and it's trying 
> to show that the loop index variable is always in bounds of some 
> array... even *after* the last iteration. This generally isn't true, but 
> it doesn't matter because there is no "next" iteration in that case.
> 
> If I write a loop assertion that doesn't mention the loop index variable 
> this problem doesn't arise, naturally. However, I can avoid it anyway by 
> doing... something... with that loop assertion. My problem is that I 
> haven't quite figured out what triggers VCs like the one above so I have 
> to kind of guess my way around how to avoid them.

I don't believe that the Examiner generates a path *to* the loop 
iteration for the last iteration - I can only imagine that there is 
something you are not seeing.

It's quite true that any VC that references the loop index will have 
your Hx above - because the loop index is within the bounds of its 
subtype at the start of the path.

However, for all paths from the assertion to the assertion, the Examiner 
will certainly generate a hypothesis that the loop index is strictly 
less than the final value of the loop range (assuming absence of 
'reverse' of course).

Therefore you have to look at what you know about the relative values of 
the last loop index value and 'Last of the array index subtype.

This is one part of what was required for the code in in your original 
post (Event_Array(I).Description_Size <= Description'Length) and you 
provided the other part.

This undoubtedly gets more involved when the last loop index value is an 
expression referencing one or more variables, but this shouldn't make 
any fundamental difference. (In this case it's sometimes helpful to 
temporarily introduce a local variable for the upper bound of the loop 
range.)

Cheers,

Phil