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

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

JP Thornley wrote:

> The usual recommendation for updating records is to assign an aggregate 
> rather than individual components (this gets rid of all the 
> upf_/update's), but the need to update an element of the array makes it 
> more awkward in this case.

Yes, an aggregate assignment followed by the update of the array makes 
for a much worse set of things to prove.

> That's a lot easier than the usual way (banging head against desk until 
> you eventually realise that it's not a problem with the tools).

But less entertaining for bystanders.

In fact, in this case I wouldn't have noticed anything wrong. When 
specifying that all original members of the array would be unchanged, I 
accidentally appended a tilde to "This" on /both/ sides of the identity, 
so it was trivially true. It would probably have vanished in the 
simplifier, and I wouldn't have known anything was wrong. Thank goodness 
for peer review and testing in the Real World! (And the low likelihood 
of a typing error in the annotation aligning with a corresponding error 
in code).