SPARK code samples
in [ADA]
|
Prev: Ada 2012: An Oops in the new Ada amendments ? (in 10.1.2 Context Clauses - With Clauses)
Next: Generic_Roots
From: (see below) on 11 Aug 2010 12:33 On 11/08/2010 17:07, in article fa1507ef-77a8-4a28-b271-2293c5115278(a)j8g2000yqd.googlegroups.com, "Mark Lorenzen" <mark.lorenzen(a)gmail.com> wrote: > On 11 Aug., 13:38, Ada novice <ycalleecha...(a)gmx.com> wrote: >> >> Thanks for this information. I'm interested to learn SPARK. If I >> understand correctly, SPARK aligns itself well with Ada 95 and not yet >> with Ada 05. Is this because of the strictness of SPARK to provide >> highly reliable codes and hence it contains only well-tested features >> (subset of Ada features)? It would be interesting to see some SPARK >> codes on the wiki page building over time. > > Not quite. SPARK is a proper subset of Ada and is amenable to static > analysis. This has (in principle) nothing to do with if an Ada feature > is well-tested or not. You should think of SPARK as a language in its > own right and not as a subset of some other language. Why? -- Bill Findlay <surname><forename> chez blueyonder.co.uk
From: Yannick Duchêne (Hibou57) on 11 Aug 2010 12:45 Le Wed, 11 Aug 2010 18:07:51 +0200, Mark Lorenzen <mark.lorenzen(a)gmail.com> a écrit: > Not quite. SPARK is a proper subset of Ada and is amenable to static > analysis. Yes > This has (in principle) nothing to do with if an Ada feature > is well-tested or not. SPARK is actually an Ada subset ;) And it elvoves toward more support of this or that Ada feature... while not all, and it will probably never support all, this one is true. > You should think of SPARK as a language in its > own right and not as a subset of some other language. From an abstract point of view, yes. There is SPARK and SPADE, and SPARK Examiner is based on SPADE Examiner (if I am not wrong... Rod will correct if needed). SPADE mainly came from Pascal, which was the first subsetted.. But SPARK is still based on Ada. There is SPARK no SPARK Modula, no SPARK Oberon and so on. > Although SPARK > constantly evolves it will never evolve into a language with the same > feature-set as Ada - no matter how well tested all Ada festures one > day will be. That precisely matter. If some feature are excluded, this is solely because they either does not enforce readability (overloading), are not predictable enough (while this depend on the state of the art) and could be in theory, but not practical or really workable way to do was found (if this end up into a SPARK which requires days to validate 10 lines, this is not good). Excluded features are excluded for some known reasons, most being documented in the SPARK Language Reference Manual. By the way, the SPARK Language Reference Manual stick to the one Ada : it use the same section numbering, naming, and so on. -- 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 11 Aug 2010 12:50 Le Wed, 11 Aug 2010 18:45:33 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > That precisely matter. If some feature are excluded, this is solely > because they either does not enforce readability (overloading), are not > predictable enough (while this depend on the state of the art) You may also add some requirements not really expressable in term features exclusion, and rather in terms of constructions, like the requirement to have a single exit point (multiple return statements are not allowed). This kind-of is not a feature matter, this is an execution flow matter. This kind of requirements are enforced by the SPARK grammar. -- 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: Ada novice on 11 Aug 2010 13:10 Thanks for all the discussions and clarifications guys. If there are novices like me :) out there wishing to get a simple yet good introduction to SPARK, I'd recommend this article: "When Computers Fly, It Has to Be Right: Using SPARK for Flight Control of Small Unmanned Aerial Vehicles" available at http://www.stsc.hill.af.mil/crosstalk/2006/09/0609swardgerkencasey.html YC
From: Mark Lorenzen on 11 Aug 2010 13:32
On 11 Aug., 18:33, "(see below)" <yaldni...(a)blueyonder.co.uk> wrote: > On 11/08/2010 17:07, in article > fa1507ef-77a8-4a28-b271-2293c5115...(a)j8g2000yqd.googlegroups.com, "Mark > > Lorenzen" <mark.loren...(a)gmail.com> wrote: > > On 11 Aug., 13:38, Ada novice <ycalleecha...(a)gmx.com> wrote: > > >> Thanks for this information. I'm interested to learn SPARK. If I > >> understand correctly, SPARK aligns itself well with Ada 95 and not yet > >> with Ada 05. Is this because of the strictness of SPARK to provide > >> highly reliable codes and hence it contains only well-tested features > >> (subset of Ada features)? It would be interesting to see some SPARK > >> codes on the wiki page building over time. > > > Not quite. SPARK is a proper subset of Ada and is amenable to static > > analysis. This has (in principle) nothing to do with if an Ada feature > > is well-tested or not. You should think of SPARK as a language in its > > own right and not as a subset of some other language. > > Why? > > -- > Bill Findlay > <surname><forename> chez blueyonder.co.uk I take it you refer to my last sentence. First of all because SPARK is not only a set of restrictions imposed on the Ada language, SPARK also mandates the use of annotations (and even more so if you want to prove program correctnes). As SPARK annotations are written as Ada comments, it is true that every SPARK program is also an Ada program and that may be why people often think of SPARK as "just" a subset of Ada [1]. I also think there is a risk of getting stuck with SPARK if you try to design a SPARK program with Ada in mind. You constantly bump into a useful feature of Ada that is not in SPARK (discriminated types, array slicing etc.) and you think "why the h... isn't that a part of SPARK when it's so easy to do in Ada?". So it's probably a way of tuning your mindset from "Ada with restrictions" into SPARK. [1] Purists may argue that even with the presence formal annotations, every SPARK program will be a member of the set of all Ada programs that include every permutation of every legal comment in every legal place. Or what? - Mark L |