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!news4.google.com!feeder1-2.proxad.net!proxad.net!feeder1-1.proxad.net!feeder.news-service.com!cyclone03.ams2.highwinds-media.com!news.highwinds-media.com!npeersf01.ams.highwinds-media.com!newsfe26.ams2.POSTED!7564ea0f!not-for-mail Message-ID: From: JP Thornley Newsgroups: comp.lang.ada Subject: Re: Newbie question: SPARK verification condition on member of private record References: MIME-Version: 1.0 Content-Type: text/plain;charset=us-ascii;format=flowed User-Agent: Turnpike/6.07-S () NNTP-Posting-Host: 80.177.171.182 X-Complaints-To: abuse@demon.net X-Trace: newsfe26.ams2 1238685790 80.177.171.182 (Thu, 02 Apr 2009 15:23:10 UTC) NNTP-Posting-Date: Thu, 02 Apr 2009 15:23:10 UTC Date: Thu, 2 Apr 2009 16:22:01 +0100 Xref: g2news2.google.com comp.lang.ada:5374 Date: 2009-04-02T16:22:01+01:00 List-Id: In article , Tim Rowe writes >That's giving me conclusions to prove like: >H1: get_order(this) < 5000 . >H2: 1 - get_probability(this) >= event_conjunctions__get_probability( > conjunction) . >H3: fld_highest_valid_index(this) >= 1 . >H4: fld_highest_valid_index(this) <= 4999 . > -> >C1: get_order(upf_probability(upf_events(upf_highest_valid_index(this, > fld_highest_valid_index(this) + 1), update(fld_events(this), [ > fld_highest_valid_index(this) + 1], conjunction)), >fld_probability( > this) + event_conjunctions__get_probability(conjunction))) = > get_order(this) + 1 . > >That's one of the easier ones. The point is that upf_probability, >upf_events and update can't affect the result of get_order. Knowing >that I can reduce the espression to > get_order( > upf_highest_valid_index > ( > this, fld_highest_valid_index(this) + 1 > ) > ) = get_order(this) + 1 > >which I can prove easily enough, but the process seems error prone (as >I say, this is one of the simpler ones). If I /could/ give the tools >some hints to reduce it it would be a big help. Maybe I /should/ make >the record public! Well, it all depends on how much rigour you need. For a fully rigorous proof you have to use the Proof Checker on the generated VC as this will only let you eliminate upf_/update's if it is valid to do so. For a less rigorous proof you create one or more user rules that eliminate the upf_/updates and, if you feel the need, justify the rule by creating and proving the equivalent VC in the Proof Checker. 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. If the record had any more components I would recommend separating out the array and its index to their own record type, but that is probably overkill here. > > >If nothing else, I found an error in the postcondition by explaining >this ;-) 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). Phil -- JP Thornley