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

["Peter C. Chapin" <PChapin@vtc.vsc.edu>]

On 2012-03-20 14:18, Phil Thornley wrote:

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

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.

Peter