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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,494ac732c5488b7f,start X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!novia!transit4.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail Message-Id: <4bffc379$0$2374$4d3efbfe@news.sover.net> From: "Peter C. Chapin" Subject: SPARK: What does it prove? Newsgroups: comp.lang.ada Date: Fri, 28 May 2010 09:25:50 -0400 User-Agent: KNode/0.10.9 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7Bit Organization: SoVerNet (sover.net) NNTP-Posting-Host: a28f2022.news.sover.net X-Trace: DXC=P:lM]KnJX4dDL5CI7;683jK6_LM2JZB_cQ^lNoJf[<7i:WUUlR<856o;lfCPS2>Zib^dm?m4@Y\4o X-Complaints-To: abuse@sover.net Xref: g2news2.google.com comp.lang.ada:12124 Date: 2010-05-28T09:25:50-04:00 List-Id: There has been a lot of discussion about SPARK on this group recently. That's great, but I hope those who are more interested in full Ada aren't getting annoyed! :) It is common to talk about SPARK proofs but of course what the Simplifier is actually proving are the verification conditions generated by the Examiner. Formally this leaves open the question of if those verification conditions have anything to do with reality or not. Ultimately, it seems to me, before one can formally prove anything about the behavior of a program one needs a formal semantics for the programming language in question. It is my understanding that SPARK95 does not have a formal semantics. Thus the Examiner is producing VCs based on the informal description of Ada in the reference manual. What if that information description is, as many such descriptions are, logically inconsistent or ambiguous? I realize that SPARK is intended to restrict the Ada language to remove ambiguity and implementation specific behavior, but is there a proof that it actually does? Without a formal semantics of SPARK, then it seems like the "proofs" produced by the tools are not really proving anything... in a mathematically rigorous sense at least. I guess this is why Praxis calls SPARK a semi-formal method. I understand that the real goals of SPARK are to help practitioners produce reliable software... not generate rigorous proofs just for the sake of doing so. To that end, following the informal specification of Ada in the reference manual seems perfectly reasonable. The features of Ada that SPARK retains are simple with (mostly) "obvious" semantics, so why quibble over every mathematical detail? I'm fine with that. The tools *do* help me write more reliable programs and that's great! Still it would be more satisfying if there was a formal semantics for SPARK to "back up" what the tools are doing. I actually read an article recently about programming language semantics that mentioned (is this true?) that one of the original requirements in the development of Ada was the production of a formal semantics for Ada. I even understand that there were two attempts to produce such a semantics. Here are those references: 1. V. Donezeau-Gouge, G. Kahn, and B. Lang. On the formal definition of Ada. In Semantics-Directed Compiler Generation, Lecture Notes in Computer Science, vol 94, pp 475-489, Springer, Berlin, 1980 2. D. Bjorner and O.N. Oest. Towards a Formal Description of Ada, Lecture Notes in Computer Science, vol 98, Springer, Berlin 1980. The article I'm reading is "Programming Language Description Languages" by Peter D. Moses in the book "Formal Methods: State of the Art and New Directions" edited by Paul P. Boca, Janathan P. Bowen, and Jawed I. Siddiqi, published by Springer, (C) 2010. I understand that the efforts above were incomplete and even then only apply to Ada 83. I also understand that few full scale languages have a formal semantics (do any?). It seems a shame, though, that Ada does not have one considering especially the way Ada is used. Peter