SPARK: What does it prove?
in [ADA]
|
Prev: SPARK and testing.
Next: SPARK and modular types
From: BrianG on 29 May 2010 21:06 mockturtle wrote: > On May 29, 4:42 pm, Marco <prenom_no...(a)yahoo.com> wrote: >> On May 28, 6:55 am, Rod Chapman <roderick.chap...(a)googlemail.com> >> wrote: >> >> >> >>> PS...if the SPARK traffic here really does get annoyingly high, >>> then perhaps we should create comp.lang.ada.spark? >> No - I enjoy the SPARK threads even though I am not using it (yet). >> Traffic volume on this group is light and respectful. > > +1 Marco just took the words out of my mouth (err.. keyboard? :-) > "yet" included... Ditto, on both counts.
From: Yannick Duchêne (Hibou57) on 30 May 2010 09:06 Le Fri, 28 May 2010 15:25:50 +0200, Peter C. Chapin <pcc482719(a)gmail.com> a écrit: > 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 with ;) > 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 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? 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 proofs. Is that true ? > 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! 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 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. 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 formal > semantics (do any?). âDo any ?â : I believe if there is some, these are languages 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, âshameâ is a lot said. So, after multiple â(see later)â, here is what I was to say : SPARK is a language. A language has a target domain (human languages too). To target 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 terms 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 not. 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 too. 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.
From: Yannick Duchêne (Hibou57) on 30 May 2010 21:17 Le Fri, 28 May 2010 15:25:50 +0200, Peter C. Chapin <pcc482719(a)gmail.com> a écrit: > 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. The question, âwhat does it prove ?â, raise another corollary question, which is âwhat can it says ?â or âwhat can it talks about ?â. I'm currently trying to make proofs on some binary stuffs, which has always seems obvious to me, and at the time of trying to prove it, I see I can't even prove the third of the initial postcondition I wanted my functions to have, because there are some I can't prove at all (I'm not talking about RTC, rather about postcondition expressing properties, and it is far less easy than proving RTC conditions). If is funny to note that these difficulty are a consequence of SPARK tied to Ada. An example : Ada has modular type, but can't see modular types has polynomials, and the relevant modal, which could help, would be this one : polynomial. Has Ada don't has this, SPARK doesn't too. Another things also : sometime, it is better to make proof on an abstract algorithm, which not efficient, and it is too much difficult to the same proof (prove postconditions from preconditions and the algorithm) with the efficient version. However, it would be more easy to demonstrate than the efficient algorithm is an equivalent transformation of the more abstract non-efficient one. I mean, prove something on function F, demonstrate function G is equivalent to function F, so as legally assert the postconditions of F are also prove on G, because there was on F and G is equivalent to F. This is another kind of thing SPARK cannot express or talk/say about. This may be the start of some answers to the question âwhat can it proves ?â or âwhat can't it proves ?â, which are similar questions. -- 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.
From: Yannick Duchêne (Hibou57) on 30 May 2010 21:21 Le Mon, 31 May 2010 03:17:32 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > If is funny to note that these difficulty are a consequence of SPARK > tied to Ada. An example : Ada has modular type, but can't see modular > types has polynomials, and the relevant modal, which could help, would > be this one : polynomial. Has Ada don't has this, SPARK doesn't too. Typo errors : replace Has by As every where it is relevant. Sorry, it seems when I am writing, I mostly write words as a whole instead of writing letters one by one, so it happens I replace a word by another.. -- 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.
From: Phil Thornley on 31 May 2010 09:05
On 31 May, 02:17, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: [...] > Another things also : sometime, it is better to make proof on an abstract > algorithm, which not efficient, and it is too much difficult to the same > proof (prove postconditions from preconditions and the algorithm) with the > efficient version. However, it would be more easy to demonstrate than the > efficient algorithm is an equivalent transformation of the more abstract > non-efficient one. > > I mean, prove something on function F, demonstrate function G is > equivalent to function F, so as legally assert the postconditions of F are > also prove on G, because there was on F and G is equivalent to F. > > This is another kind of thing SPARK cannot express or talk/say about. How about using proof abstraction? Put one set of post-conditions (for the inefficient version) on the spec and the other set (for the efficient version) on the body. Then the post-conditions on the body are proved from the code and the post-conditions on the spec are proved by a user rule that is justified by the 'offline' proof of equivalence of the two algorithms. *** BUT *** the current GPL version (8.1.1) sometimes gets that post- condition refinement VC wrong. This only seems to happen when there is a refined pre and post-condition on the body but no refined state data, eg for private types, which is where I came across the problem. (Notified to report(a)gnat.com on 9th February). Cheers, Phil |