SPARK: What does it prove?
in [ADA]
|
Prev: SPARK and testing.
Next: SPARK and modular types
From: Peter C. Chapin on 28 May 2010 09:25 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
From: Rod Chapman on 28 May 2010 09:55 On May 28, 2:25 pm, "Peter C. Chapin" <pcc482...(a)gmail.com> wrote: > 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. Well..not quite. The VC generator was constructed and very much based on the formal semantics for SPARK83 that was contstructed in the mid-1990s. We have _lots_ of confidence that this semantics is completely upwards-compatible and consistent with the canonical semantics of Ada95 and this SPARK95 SPARK2005. Unfortunately, we did not have the funding to keep that SPARK83 semantics up to date with new features that were added later like modular types from Ada95, but these are a fairly modest extension to the language. There are also lots of assumptions tha underlie any "proof" of anything - in our case the integrity of the compiler, linker and the rest of the build environment, the implementation of the target processor itself and many other things. While these are valid concerns, these assumptions really do seem to hold up in the "real world" - i.e. with our customers using real commercial compilers, microprocessors and so on. In short: it seems to work. - Rod Chapman, SPARK Team, Praxis PS...if the SPARK traffic here really does get annoyingly high, then perhaps we should create comp.lang.ada.spark?
From: Peter C. Chapin on 28 May 2010 11:58 Rod Chapman wrote: > Well..not quite. The VC generator was constructed and very much > based on the formal semantics for SPARK83 that was > contstructed in the mid-1990s. We have _lots_ of confidence > that this semantics is completely upwards-compatible > and consistent with the canonical semantics of Ada95 and > this SPARK95 SPARK2005. That's interesting to know. Thanks. > There are also lots of assumptions tha underlie any > "proof" of anything - in our case the integrity of the compiler, > linker and the rest of the build environment... Yes, definitely. This was a point I tried to make in a different thread related to testing SPARK programs (and the value of doing so). SPARK helps show that the source code is in some sense correct, which is great, but that's not the whole story. > In short: it seems to work. Absolutely. I hope you didn't take my post as a criticism of SPARK. If the goal is to reduce errors in actual deployed programs, which at the end of the day is the important thing it seems, then I agree that SPARK works! Peter
From: Marco on 29 May 2010 10:42 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.
From: mockturtle on 29 May 2010 15:02
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... |