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.4 required=5.0 tests=AC_FROM_MANY_DOTS,BAYES_00, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Received: by 10.182.153.169 with SMTP id vh9mr17370903obb.18.1445595920137; Fri, 23 Oct 2015 03:25:20 -0700 (PDT) X-Received: by 10.182.247.67 with SMTP id yc3mr262103obc.0.1445595920107; Fri, 23 Oct 2015 03:25:20 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!kq10no26578162igb.0!news-out.google.com!n2ni40942igy.0!nntp.google.com!kq10no26578157igb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 23 Oct 2015 03:25:19 -0700 (PDT) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=95.172.74.52; posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S NNTP-Posting-Host: 95.172.74.52 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <3c3ef412-4a5c-419f-a1c5-ae5e4fe4d0a9@googlegroups.com> Subject: GNATProve - interactions between units From: Maciej Sobczak Injection-Date: Fri, 23 Oct 2015 10:25:20 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:28039 Date: 2015-10-23T03:25:19-07:00 List-Id: 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 o= f 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 i= n 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 amortize= s 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 u= nits prove clean, whereas the whole produces warning messages about range c= hecks. 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 sufficien= t for analyzing correctness of the program as a whole? --=20 Maciej Sobczak * http://www.inspirel.com