SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 12 May 2010 18:55 Hello, Short title, âSPARKâ, as short as a subset (joking) I wanted to start some SPARK related questions, ... âGNAT packages in Linuxâ kept apart. Well, sorry for that, my first question gonna be about license. The GPL applies to SPARK-GPL (oh? really?). How does it apply ? I'm dubious about it in this context, because using SPARK to check an implementation does not implies any kind of linking to any binary or library, and I did not see anywhere something stating there was license restrictions on the usage of SPARK annotations in Ada sources. What are the concrete restrictions so ? Hope this first question will get a short answer, so let us jump to the second question, which is intended to start with one major deal of SPARK for people who know/use Ada : Ada subset and restrictions (not to disclaim or disagree with, mostly to talk and understand more). The Praxis reference for SPARK-95 says : [Praxis SPARK95 3] > SPADE-Pascal was developed essentially by excising from > ISO-Pascal those features which were considered particularly > âdangerousâ, or which could give rise to intractable validation > problems - such as variant records, That said, variant record can be emulated by user or program too, as that's just what were doing many people when there was no language support for that. What is different when the Pascal or Ada variant record compared to a user or program doing explicitly the same ? May be the answer is just in one of the last three words : âexplicitlyâ ? Does this quotation from the Praxis's reference about SPARK suggests SPARK has some troubles with the implicit or the underlying ? If SPARK could know about a formalization of what's going on with variant records, as explicit as would be the same made by the user or program, would that solve the trick ? What would possibly make this difficult or non-trustable ?
From: Yannick Duchêne (Hibou57) on 12 May 2010 20:52 Le Thu, 13 May 2010 00:55:02 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Hope this first question will get a short answer, so let us jump to the > second question, which is intended to start with one major deal of SPARK > for people who know/use Ada : Ada subset and restrictions (not to > disclaim or disagree with, mostly to talk and understand more). An important quote every one should know about ; especially the last sentence: [Praxis SPARK 95 (5)] > Some readers may be dismayed to see so many features of Ada removed, > and feel that SPARK is âtoo smallâ. It is by no means the largest > subset of Ada which would be amenable to analysis by the techniques > employed in SPADE, but it is significantly larger than SPADE-Pascal, > which has been found adequate for a substantial number of > safety-critical projects. The additional features which appear in > SPARK (such as packages and private types) make programming simpler > and safer, rather than complicate the verification task. Of course, > the extent to which Ada must be simplified for high-integrity > programming will be a matter of opinion: our preoccupation with > simplicity is based on experience of what can be achieved with a > high degree of confidence in practice, rather than what can be > proved in principle. -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 12 May 2010 23:06 Some quick though to feed the talk and give interested parties an opportunity to take part. Although I can understand most of the restrictions SPARK applies (a big amount of them did not ever requires to use SPARK to be meaningful and beneficial and I do apply lot of them already), I still don't understand one : the restriction of not using derived type (except tagged type, which are supported by SPARK). What was the rational for that ? Functions may have legitimate side effects, like for memoisation. Memoisation is a kind of optimization and optimizations should be transparent to clients. SPARK would requires to split it into two parts: a kind of âprepare/computeâ procedure and a âget resultâ function ; the procedure being supposedly invoked prior to each function invokation. Did you ever face this ? Block statements are not allowed in SPARK. Let say a procedure can do the same. Was this only to have one-matter-one-feature (avoid to have both block-statement and procedure, and keep only one) for the sake of simplicity or was there some other reasons properly dealing with verifiability ? -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 13 May 2010 00:00 Le Thu, 13 May 2010 00:55:02 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > How does it apply ? I'm dubious about it in this context, because using > SPARK to check an implementation does not implies any kind of linking to > any binary or library, and I did not see anywhere something stating > there was license restrictions on the usage of SPARK annotations in Ada > sources. At least the package SPARK_IO on Windows is MGPL : [from SPARK_IO header] -- As a special exception, if other files instantiate generics from this unit, -- or you link this unit with other files to produce an executable, this unit -- does not by itself cause the resulting executable to be covered by the GNU -- General Public License. This exception does not however invalidate any other -- reasons why the executable file might be covered by the GNU Public License. -- pragma Asset ? Is that true ? Waaww... great
From: stefan-lucks on 13 May 2010 05:28
On Thu, 13 May 2010, Yannick Duch�ne (Hibou57) wrote: > Functions may have legitimate side effects, like for memoisation. Memoisation > is a kind of optimization and optimizations should be transparent to clients. > SPARK would requires to split it into two parts: a kind of �prepare/compute� > procedure and a �get result� function ; the procedure being supposedly invoked > prior to each function invokation. Did you ever face this ? When working with SPARK, it is difficult *not* to face that. E.g., usually, you would write a pseudorandom number generator as function Rnd return T is begin Global_State := f(Global_State); return g(Global_State); end; In SPARK, you have to replace the function RND by a procedure, which delivers the result as an out parameter. Very inconvenient! But reasonable: Note that the result from evaluating an expression such as "Rnd + Rnd**2" depends on the order of evaluation, which isn't specified in the Ada standard. If we write I for the initial global state, then "Rnd + Rnd**2" can either evaluate to f(g(I) + f(f(g(I)))**2, or to f(f(g(I))) + f(g(I))**2. Such an unspecified behaviour makes static analysis very difficult. In principle, you would have to consider all possible orders of evaluation and check if something is going wrong. That would be very hard for SPARK, and, with a few legitimate exceptions, such that pseodorandom numbers, this is bad programming style anyway. Thus, SPARK prohibits this. -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------ |