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!border1.nntp.dca.giganews.com!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: Thu, 02 Apr 2009 18:58:12 -0500
Date: Fri, 03 Apr 2009 00:58:10 +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>
In-Reply-To: <XQOei4CZgN1JJw9Y@diphi.demon.co.uk>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <y7ednbO7TLaJzEjUnZ2dnUVZ8sSdnZ2d@posted.plusnet>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-5awg5J2d21qpobbLpEyS1A46LpB+Ncfsy/m10kqYK27i9ZqYYQdXUqd51U5306U6qegN5DxzIlhMuI1!ent4qjeGjC2W0UaJ0VX8aKaZnWAoWqQjqfjbk+TahH6NR5guNVHFSmABMGdqa7vBTe7AIWUezt0n!2MoxS8vIDyDp
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
X-Original-Bytes: 2462
Xref: g2news1.google.com comp.lang.ada:4410
Date: 2009-04-03T00:58:10+01:00
List-Id: <comp.lang.ada>

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).