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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,494ac732c5488b7f X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 Path: g2news2.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: SPARK: What does it prove? Date: Sun, 30 May 2010 15:06:21 +0200 Organization: Ada At Home Message-ID: References: <4bffc379$0$2374$4d3efbfe@news.sover.net> NNTP-Posting-Host: qUfwAWuer84MZJ3PpksnTQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org X-Notice: Filtered by postfilter v. 0.8.2 User-Agent: Opera Mail/10.53 (Win32) Xref: g2news2.google.com comp.lang.ada:12163 Date: 2010-05-30T15:06:21+02:00 List-Id: Le Fri, 28 May 2010 15:25:50 +0200, Peter C. Chapin = a =C3=A9crit: > 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! :) You're welcome > 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. This leaves open the question of the interpretation, indeed (see later),= = and that is expected, nothing else can be expected. > 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. Formal semantics, that is, the same kind of logic SPARK already deals wi= th = ;) > It is my > understanding that SPARK95 does not have a formal semantics. Not the one of a programming language, which it is not (this is Ada's = role, could it be a subset or not), while it still have a semantic : = logic, boolean algebra, the atoms of complexity. > 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 suc= h > 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 actuall= y = > does? May they did act like physicians instead of like mathematicians in this = = particular area. If they ever observe something going into a wrong = direction, they will update some rules. If this is done as seriously as = = physicians do they own job, it is somewhat trustable. > 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. (see later) > I guess this is why Praxis calls SPARK a semi-formal method. Ouch, I did not read this. Semi-Formal ? Semi ? > 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. This seems to implies there is a way to do reliable without formal proof= s. = Is that true ? > To that end, following the informal specification of Ada in the refere= nce > 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! Good > 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?) Do you have a link please ? (providing this is not a paper article). > 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: Hoare would have loved it. > 1. V. Donezeau-Gouge, G. Kahn, and B. Lang. On the formal definition o= f = > 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, Lect= ure > 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. OK, sorry, can't read this. > 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 form= al > semantics (do any?). =E2=80=9CDo any ?=E2=80=9D : I believe if there is some, these are langu= ages with very = specific targets, like CPU design. > It seems a shame, though, that Ada does not have one > considering especially the way Ada is used. Well, =E2=80=9Cshame=E2=80=9D is a lot said. So, after multiple =E2=80=9C(see later)=E2=80=9D, here is what I was to = say : SPARK is a = language. A language has a target domain (human languages too). To targe= t = its domain, it has some capabilities at expressing things about subjects= = of its domain, and it will always only talk about these subject, in its = = only possible terms. Does what this language will say will makes sense ? Surely, what the language will say will always be different than the = subjects it will talk about, as it will always talk about it in some ter= ms = of interest : the target. The same could be said about any talks. Now, SPARK is a metalanguage, that is, a language which tells about = another language and its target is logic. It has and was given = capabilities in logic, so it will talk about a program using logic = lightings. Does it make sens ? Depends... if for you, an Ada application= = is mainly a matter of logic, this will, if this is not, then this will n= ot. If it is, then can add that the main target of SPARK is soundness, so it= = will talk about Ada application's soundness. That is all, and no less to= o. = If something else is needed, then something else, or may be another = formalism or another language will be needed. Remains the question of possible weakness time-bombs in this heaven of = soundness, and I feel this was your main question. -- = There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.