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!cyclone02.ams2.highwinds-media.com!news.highwinds-media.com!npeersf01.ams.highwinds-media.com!newsfe30.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: newsfe30.ams2 1238662829 80.177.171.182 (Thu, 02 Apr 2009 09:00:29 UTC) NNTP-Posting-Date: Thu, 02 Apr 2009 09:00:29 UTC Date: Thu, 2 Apr 2009 10:00:16 +0100 Xref: g2news2.google.com comp.lang.ada:5369 Date: 2009-04-02T10:00:16+01:00 List-Id: In article , Tim Rowe writes >JP Thornley wrote: > >> The rule should look like: >> a_name(1): get_order(X) may_be_replaced_by fld_highest_valid_index(X). >> where 'a_name' can be any name you like. X will be treated as a >>wildcard that matches to anything in the VC. > >That works nicely, thanks. Although... > >> The justification for the rule is the code of the function Get_Order. >>It really would be nice to have a return annotation on the function >>but, as you have found, this isn't possible with private types. >> [Actually it is possible, but very longwinded and involves the >>additional definition of a proof function, so it isn't usually >>considered worthwhile for such simple code.] > >... I'll probably want to get around to that approach eventually. In >fact, sooner rather than later I think. Otherwise for some of the other >proof obligations it looks as if I'm going to need a lot of user rules >to tell the simplifier that various operations don't affect the results >of Get_Order. I had thought of proof functions but couldn't see how not >to move the same problem into the proof function. > >How long-winded is long-winded? Yes, information hiding is a great idea for structuring software but becomes something of a pain when it comes to proof - and you end up exposing various aspects of the hidden code. However I would never recommend degrading the software structure to make proof easier - at least for proof of absence of run-time error (proof of partial correctness may be a different matter). In this case you may need to add postconditions on various operations that update objects of the private type, to say that the result of Get_Order is unchanged by the operation, but this is probably better than the alternative - which is make the type visible. For proof of absence of run-time error it is normal practice only to add proof annotations in response to unprovable VCs, so you may find that only a few operations need a postcondition for unchanged Get_Order. On the function return annotation - you cannot avoid the use of a user rule here as function return annotations have no effect on the hypotheses of VCs generated subsequent to the function call. This is the big difference between function return annotations and procedure postconditions. The only thing that function return annotations do is provide the supporting argument for one or more rules about the result of the function (and which can be applied to the VCs subsequent to the function call as that call will appear in the VC). The 'long-winded justification' simply provides a supporting argument that is more rigorous than 'go and look at the code'. Phil -- JP Thornley