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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.albasani.net!news.roellig-ltd.de!open-news-network.org!cyclone03.ams2.highwinds-media.com!news.highwinds-media.com!voer-me.highwinds-media.com!post02.fr7!fx22.fr7.POSTED!not-for-mail From: Brian Drummond Subject: Re: I'm a noob here. Newsgroups: comp.lang.ada References: <2c400962-3a09-4da2-9f56-b4f1986b80f8@googlegroups.com> <42945a0c-e4ae-41ff-a2ce-d3faf41336ce@googlegroups.com> User-Agent: Pan/0.139 (Sexual Chocolate; GIT bf56508 git://git.gnome.org/pan2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Message-ID: NNTP-Posting-Host: 62.49.20.82 X-Complaints-To: abuse@demon.net X-Trace: 1399373273 62.49.20.82 (Tue, 06 May 2014 10:47:53 UTC) NNTP-Posting-Date: Tue, 06 May 2014 10:47:53 UTC Date: Tue, 06 May 2014 10:47:53 GMT X-Received-Body-CRC: 3934958552 X-Received-Bytes: 2189 Xref: news.eternal-september.org comp.lang.ada:19709 Date: 2014-05-06T10:47:53+00:00 List-Id: On Mon, 05 May 2014 05:43:50 -0700, Dan'l Miller wrote: > In brief, what the OP is asking is: precisely how does a SPARK compiler > actually utilize the meta-information annotations? E.g., precisely how > does a SPARK compiler make logical inferences regarding correctness of > Ada-subset source code to verify that the imperative code does what the > annotations have declared? There is no such thing as a "SPARK compiler" (at least yet). Every SPARK program is a valid Ada program (but not vice-versa) so SPARK is simply compiled with an Ada compiler. What the SPARK tools do is - not compilation - but proving the "correctness" of the program - for example, proving that any errors that could cause integer overflow are simply not present in the source code. Or, failing that, pointing out the unprovable parts so that either the proof can be completed, or the error preventing proof can be eliminated. A very large system is unlikely to be suitable for SPARK, but a good candidate for Ada. Where SPARK comes in is if you can design the system such that a relatively small kernel handles the most critical information (security, encryption, or arbitrary precision fixed point arithmetic) and cleanly interfaces to the rest of the system. That kernel can be formally proven using SPARK; the rest of the system is implemented in conventional Ada. - Brian