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: 
 g2news2.google.com!news2.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!cyclone1.gnilink.net!gnilink.net!nx02.iad01.newshosting.com!newshosting.com!novia!novia!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: Mon, 06 Apr 2009 06:49:12 -0500
Date: Mon, 06 Apr 2009 12:49:07 +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>
 <y7ednbO7TLaJzEjUnZ2dnUVZ8sSdnZ2d@posted.plusnet>
 <vsCQtXDoDh1JJwZV@diphi.demon.co.uk>
In-Reply-To: <vsCQtXDoDh1JJwZV@diphi.demon.co.uk>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <xeWdnT1GbMelcUTUnZ2dnUVZ8t2WnZ2d@posted.plusnet>
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-affpQhS3j7ABtRi9rlhSBo89YHNDw3UvQsedk3wzPPAOhv+5IZvFMxZg0taKHYex/aJoDYYiEVX0NzB!wqGFnFIjt65GCgXjO/PaR2FR4Sj4XckT9Bb6/DebcFm+U1vbw054U/UBd5towm6ffzlbH2q3obj1!/rCfjISdvFZw
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: g2news2.google.com comp.lang.ada:5418
Date: 2009-04-06T12:49:07+01:00
List-Id: <comp.lang.ada>

JP Thornley wrote:

> An alternative that sometimes works when updating arrays is to move the
> update into a local operation (it's completely non-intuitive code but
> often creates easier proofs).


Correct on both counts -- it greatly simplifies the VCs (each one now 
reads quite naturally) and it is completely non-intuitive :-)

I'll go and scratch my head for a while to figure uoit how this works -- 
which I think mainly comes down to figuring out why the fields of the 
private type are visible for the postcondition of the local operation 
when they weren't visible for annotations of the enclosing operation.

Thanks for your help, anyway -- clearly I still have a long way to go, 
but I feel that with your (and Rod's) help I'm making good progress.