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

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

roderick.chapman@googlemail.com wrote:
> I concur with Phil.  It's almost _always_ better to write
> aggregate expressions and use the array/record update notation
> in postconditions than using field-by-field assignments
> and equalities.
> 
> e.g.
> 
> Do write
> 
>  A := T'(X, Y, Z);
> 
> Don't write
> 
>  A.F1 := X;
>  A.F2 := Y;
>  A.F3 := Z;

Except in this case that makes the VCs a lot more complicated. You 
covered that by saying /almost/ always, of course.

> Also...for just
> 
>  A.F1 := X;
> 
> the correct post-condition would be
> 
>  --# post A = A~[F1 => X];

Except that in this case the type of A is private, so I can't (as far as 
I can tell) access its fields from a postcondition.