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

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

In article <aYCdndGkyL_dCc7S4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...
[...snipped...]

Peter,

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%

Cheers,

Phil


> P.S. I posted a message earlier about discharging a post condition with 
> a quantified expression. I just want you (Phil) to know that I read your 
> message but I haven't had time to work with that example since. I did 
> get an insight about it, however, so I want to reflect on that insight 
> for a bit. I'll post again if I have more questions. Thanks for your help!

If there's too much code to post to news then feel free to mail it to me 
- the address is on the sparksure web site if you don't still have it.