From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,e6cf7d66027047db
X-Google-Attributes: gid103376,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news1.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!bigfeed2.bellsouth.net!news.bellsouth.net!border2.nntp.dca.giganews.com!nntp.giganews.com!backlog2.nntp.dca.giganews.com!nntp.posted.plusnet!news.posted.plusnet.POSTED!not-for-mail
NNTP-Posting-Date: Fri, 03 Apr 2009 06:26:17 -0500
Date: Fri, 03 Apr 2009 12:26:14 +0100
From: Tim Rowe <spamtrap@tgrowe.plus.net>
User-Agent: Thunderbird 2.0.0.21 (Windows/20090302)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Newbie question: SPARK verification condition on member of
  private
 record
References: <jsudnfEigqAgX07UnZ2dnUVZ8ridnZ2d@posted.plusnet>
 	<cg$c+4BZb90JJwWv@diphi.demon.co.uk>
 <et6dnUO6O_dLYE7UnZ2dnUVZ8o-dnZ2d@posted.plusnet>
 	<IKw5EvCg6H1JJwey@diphi.demon.co.uk>
 <JKKdnWLcDdxDNUnUnZ2dnUVZ8sCWnZ2d@posted.plusnet>
 	<XQOei4CZgN1JJw9Y@diphi.demon.co.uk>
 <fda46992-7b1c-4b6c-a483-acd3b755748c@f19g2000vbf.googlegroups.com>
In-Reply-To: 
 <fda46992-7b1c-4b6c-a483-acd3b755748c@f19g2000vbf.googlegroups.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <9fGdnfSS-7PEb0jUnZ2dnUVZ8umdnZ2d@posted.plusnet>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-mt1/oPBwlrRK4KZ3h7TwIgmrmLG961z7jmTm/bHOp/IL6bF4YZOruAX58VS66xqWtvoyVIX50fTolga!SoRznK+Qt+aBM0optLAbWp4b6X0QPvzL+0VZnNJnh+ph8ropO7PQW6cMR2rk4aYTrRyYVXpE6qF6!LGXEvXINdGSn
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.39
Xref: g2news1.google.com comp.lang.ada:4413
Date: 2009-04-03T12:26:14+01:00
List-Id: <comp.lang.ada>

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.