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

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

On 2012-03-04 13:43, Phil Thornley wrote:

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

I tried changing the assertion to

   --# assert Event_Array(I).Description_Size <= Description'Length and
   --#        (J - 1) < Description'Length;

but that didn't help by itself. When I tried adding Event_Array = 
Event_Array% that didn't seem to do anything. I have a feeling that 
because Event_Array has mode 'in' the Examiner is already considering 
its constancy.

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.

Anyway, thanks for your hint.

Peter