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.5 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM,STOX_REPLY_TYPE autolearn=no autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!goblin3!goblin.stu.neva.ru!news.netfront.net!not-for-mail From: "Phil Thornley" Newsgroups: comp.lang.ada Subject: Re: GNATProve - interactions between units Date: Sun, 25 Oct 2015 13:27:40 -0000 Organization: Netfront http://www.netfront.net/ Message-ID: References: <3c3ef412-4a5c-419f-a1c5-ae5e4fe4d0a9@googlegroups.com> NNTP-Posting-Host: 88.97.49.112 Mime-Version: 1.0 Content-Type: text/plain; format=flowed; charset="iso-8859-1"; reply-type=original Content-Transfer-Encoding: 7bit X-Trace: adenine.netfront.net 1445779664 63441 88.97.49.112 (25 Oct 2015 13:27:44 GMT) X-Complaints-To: news@netfront.net NNTP-Posting-Date: Sun, 25 Oct 2015 13:27:44 +0000 (UTC) In-Reply-To: <3c3ef412-4a5c-419f-a1c5-ae5e4fe4d0a9@googlegroups.com> X-Priority: 3 X-MSMail-Priority: Normal Importance: Normal X-Newsreader: Microsoft Windows Live Mail 16.4.3528.331 X-MimeOLE: Produced By Microsoft MimeOLE V16.4.3528.331 X-Antivirus: avast! (VPS 151025-2, 25/10/2015), Outbound message X-Antivirus-Status: Clean Xref: news.eternal-september.org comp.lang.ada:28046 Date: 2015-10-25T13:27:40+00:00 List-Id: > "Maciej Sobczak" wrote in message > news:3c3ef412-4a5c-419f-a1c5-ae5e4fe4d0a9@googlegroups.com... > Hi, > My understanding of SPARK rules is that it is possible to reason about the > correctness of the program by proving its units individually and the role > of package specifications and subprogram contracts is to isolate units > from each other in the sense that it is not necessary to look into other > units in order to declare the correctness of the unit being analyzed. > In other words, we can run GNATProve on each unit separately. > On the other hand, running GNATProve on all program units allows the tool > (apart from reusing the runtime infrastructure of the prover, which > amortizes the startup time over many units) to get more information about > how units use each other and from this additional information it can > discharge more VCs than would be possible otherwise. > If this is true, then running GNATProve on the whole program should > produce the same or *smaller* amount of undischarged VCs. > I have a project where the opposite can be observed - that is, individual > units prove clean, whereas the whole produces warning messages about range > checks. > Is it acceptable to consider this to be a tool bug? Or are there any flaws > in my reasoning above and in fact proving units separately is not > sufficient for analyzing correctness of the program as a whole? I will be very surprised if proof of an individual unit uses any information about the set of calls of that unit. It was certainly not true for the original SPARK and I haven't seen anything about the new version that suggests that it has changed. AFAIK, the only check that uses the whole program is the check that all objects are initialised before use. You can control the operation of GNATProve via the timeout/steps parameter and also by the proof strategy - using 'per_check' may fail to prove some VCs that are proved by the other strategies (see 6.2.2 of the User Guide). Cheers, Phil Thornley --- This email has been checked for viruses by Avast antivirus software. https://www.avast.com/antivirus --- news://freenews.netfront.net/ - complaints: news@netfront.net ---