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

[roderick.chapman@googlemail.com]

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;

Also...for just

 A.F1 := X;

the correct post-condition would be

 --# post A = A~[F1 => X];

which defines the final value of the whole object, rather than

 --# post A.F1 = X;

which defines the final value of A.F1 but leaves the other
2 fields unspecified.  Further explanation of all this in the
"Generation of VCs" manual.

 - Rod Chapman, SPARK Team