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=0.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b0cbdc5a85122130 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.204.150.90 with SMTP id x26mr109914bkv.6.1330535681946; Wed, 29 Feb 2012 09:14:41 -0800 (PST) Path: t13ni84120bkb.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!news.stack.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!reader02.news.zen.co.uk.POSTED!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK question: discharging post-conditions. Date: Wed, 29 Feb 2012 17:14:35 -0000 Message-ID: References: Reply-To: phil.jpthornley@gmail.com MIME-Version: 1.0 User-Agent: MicroPlanet-Gravity/3.0.4 Organization: Zen Internet NNTP-Posting-Host: 01f4f821.news.zen.co.uk X-Trace: DXC=UgiV[ON4?bBa05NSdR58cIYjZGX^207PK` In article , PChapin@vtc.vsc.edu says... > > I'm experimenting with a small exercise and it's not working quite like > I expected. I could show my real code, but in the interest or brevity > I'll try to show the structure and hope that's enough to address my issue. > > I'm writing a simple sorting procedure that consists of a main loop. > Something like (not compilable): > > procedure Sort(Buffer : in out Buffer_Type) is > begin > for I in Index_Type range X .. Y loop > -- Do interesting stuff... > > --# assert [that the array is partially sorted] > end loop; > end Sort; > > Notice that the assertion is at the bottom of the loop. I'm wondering if > that's a problem for me. That shouldn't be a problem at all. The only requirement is that every path over the loop that does not exit the loop must meet an assertion somewhere. > The idea is that the first time through the > loop the assertion will be true. Furthermore if the assertion is true on > one pass it will be true on the next. This is fine. In fact, the VCs > associated with the assertion are proving (they are universally > quantified expressions and I'm using alt-ergo to deal with them; the > SPARK simplifier doesn't prove them). > > My problem is that the post-condition, which says that the array is > fully sorted, isn't being discharged. When I look at the post condition, > the hypotheses are rather trivial. I'm not sure exactly what you mean here - do you mean a postcondition that you have stated for the procedure or the conclusions on the VCs that are generated by the Examiner for the "For path(s) ... to finish" VCs? > They basically say that the first two > elements are in order and, oh yeah, every element of the array is in the > range of its subtype. That's it. Naturally that's not enough to prove > the conclusion. > > My question is: why isn't the information in the loop assertion making > it to the post-condition? The path quoted for the VC is "from assertion > of line [the assert I show above] to finish." Yet the asserted condition > is not mentioned in the VC's hypotheses. > > I think I'm misunderstanding something, but I don't recall this coming > up for me before. Any VC that is generated for a path starting from an assertion will (certainly "should") have hypotheses for the assertion. Are you looking at the VC generated by the Examiner (in the .vcg file) or a version of the VC that has been processed by one or more provers. If the latter then these tools have an unfortunate tendency to remove any hypothesis that they can reduce to True (since it clearly adds nothing to the rest of the hypotheses). Another reason for a prover removing a hypothesis is if it can show that it has no possible connection with any conclusion. If the values referenced in a hypothesis cannot be connected to any value in a conclusion via any other hypothesis then it might well be removed. To be any more definite we need to see the actual code, I'm afraid. Cheers, Phil