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!news3.google.com!feeder.news-service.com!cyclone03.ams2.highwinds-media.com!news.highwinds-media.com!npeersf02.ams.highwinds-media.com!newsfe23.ams2.POSTED!7564ea0f!not-for-mail
Message-ID: <vsCQtXDoDh1JJwZV@diphi.demon.co.uk>
From: JP Thornley <jpt@diphi.demon.co.uk>
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>
MIME-Version: 1.0
Content-Type: text/plain;charset=us-ascii
User-Agent: Turnpike/6.07-S (<JB7liKIhasMYbQFOkfQcArwAzo>)
NNTP-Posting-Host: 80.177.171.182
X-Complaints-To: abuse@demon.net
X-Trace: newsfe23.ams2 1238765915 80.177.171.182 (Fri,
 03 Apr 2009 13:38:35 UTC)
NNTP-Posting-Date: Fri, 03 Apr 2009 13:38:35 UTC
Date: Fri, 3 Apr 2009 14:36:40 +0100
Xref: g2news2.google.com comp.lang.ada:5391
Date: 2009-04-03T14:36:40+01:00
List-Id: <comp.lang.ada>

In article <y7ednbO7TLaJzEjUnZ2dnUVZ8sSdnZ2d@posted.plusnet>, Tim Rowe
<spamtrap@tgrowe.plus.net> writes
>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.

Although you get some fearsome looking expressions sometimes, it is
often the case that a rule that proves a conclusion is much simpler.
If you want to send me some sparkable code to play with then use the
email address on www.sparksure.com.

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

If your code looks something like:
      This.Highest_Valid_Index => This.Highest_Valid_Index + 1;
      This.Events(This.Highest_Valid_Index) := Conjunction;

then add the following as a local procedure and call it in place of the
second statement above (it shouldn't cost anything in execution time as
the compiler should be able to inline it)

      procedure Set_Element
      --# global in out This;
      --#        in     Conjunction;
      --# derives This from *, Conjunction;
      --# post This.Probability = This~.Probability and
      --#      This.Highest_Valid_Index = This~.Highest_Valid_Index and
      --#      This.Events = This~.Events[New_Index => Conjunction];
      is
      begin
         This.Events(This.Highest_Valid_Index) := Conjunction;
      end Set_Element;
      pragma Inline(Set_Element);

you may find that any VCs left by the Simplifier are now easier to read.

Phil

-- 
JP Thornley