Re: Newbie question: SPARK verification condition on member of private record

[Tim Rowe <spamtrap@tgrowe.plus.net>]

JP Thornley wrote:

> An alternative that sometimes works when updating arrays is to move the
> update into a local operation (it's completely non-intuitive code but
> often creates easier proofs).


Correct on both counts -- it greatly simplifies the VCs (each one now 
reads quite naturally) and it is completely non-intuitive :-)

I'll go and scratch my head for a while to figure uoit how this works -- 
which I think mainly comes down to figuring out why the fields of the 
private type are visible for the postcondition of the local operation 
when they weren't visible for annotations of the enclosing operation.

Thanks for your help, anyway -- clearly I still have a long way to go, 
but I feel that with your (and Rod's) help I'm making good progress.