What is SPARK about?
in [ADA]
|
Prev: REMINDER: approaching deadline (June 25, 2010) for SIGAda 2010 submissions
Next: Processing array subsections, a newbie question.
From: Claude on 11 Jun 2010 16:32 Ada is a formal language to software engineering. What is SPARK about? I means since SPARK is restricted to the best of Ada, is SPARK better than Ada to resolving complex engineering applications, or SPARK a better choice than C/C++ to address leaner systems? (in terms of compliance to early drafts of DO-178C - certification levels C to A). Indeed, the successful applications of SPARK bring to results that are rather difficult to compare. The formal design of Tokeneer ID Station (TIS) shows the TIS system to be a purely sequential system. - (INFORMED design, at section 2.2, Identification of the SPARK boundary) We believe part of the success of proof on SHOLIS is due to the simple system architecture. Some large-scale SPARK reasoning are also needed, including support for abstract proof, before the technology can be extensively used at the highest level of large systems. - (Is Proof More Cost Effective Than Testing Section 8, Summary). Beyond any theory or academic project, 10 years later, from all the past SPARK projects experiences, does it happen that SPARK can address purely sequential systems or that SPARK can be extensively used at the highest level of large systems? Claude
From: Simon Wright on 11 Jun 2010 19:01 Claude <claude.defour(a)orange.fr> writes: > I means since SPARK is restricted to the best of Ada The SPARK toolset supports a subset of Ada that it can reason about. As the SPARK toolset has become more capable (ie, "we" have discovered ways of programming the machine to reason about more of Ada), so the supported subset has got larger to match. As an example, I'm pretty sure SPARK doesn't handle generics; so that rules out the Container library.
From: Yannick Duchêne (Hibou57) on 11 Jun 2010 19:17 Le Sat, 12 Jun 2010 01:01:51 +0200, Simon Wright <simon(a)pushface.org> a écrit: > As an example, I'm pretty sure SPARK doesn't handle generics; so that > rules out the Container library. I did not tried it yet, so I will not any about the present state (Iâve just noticed it support the syntax). What is sure, is that support (or better support) for generic is planed for the futur... and is already present in SPARK Pro (if I'm not wrong). -- 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 12 Jun 2010 04:30 On 11 June, 21:32, Claude <claude.def...(a)orange.fr> wrote: > Ada is a formal language to software engineering. > > What is SPARK about? SPARK is an annotated sublanguage of Ada, intended for use in high- integrity applications. An important property of the language is that it is unambiguous - every valid SPARK program, when compiled by a conforming Ada compiler, has one and only one meaning. Therefore it becomes practicable to reason about the behaviour of a SPARK program based solely on the analysis of the program text. > > I means since SPARK is restricted to the best of Ada, is SPARK better > than Ada to resolving complex engineering applications, or SPARK a > better choice than C/C++ to address leaner systems? (in terms of > compliance to early drafts of DO-178C - certification levels C to A). > > Indeed, the successful applications of SPARK bring to results that are > rather difficult to compare. > > The formal design of Tokeneer ID Station (TIS) shows the TIS system > to be a purely sequential system. - (INFORMED design, at section > 2.2, Identification of the SPARK boundary) Support for concurrent programs (RavenSPARK) was added in 2003. > > We believe part of the success of proof on SHOLIS is due to the > simple system architecture. > Some large-scale SPARK reasoning are also needed, including support > for abstract proof, before the technology can be extensively used at > the highest level of large systems. - (Is Proof More Cost Effective > Than Testing Section 8, Summary). Support for abstract proof was added in 2000. > > Beyond any theory or academic project, 10 years later, from all the > past SPARK projects experiences, does it happen that SPARK can > address purely sequential systems or that SPARK can be extensively > used at the highest level of large systems? An example of a large, concurrent SPARK program is iFACTS - described by the UK National Air Traffic Service as "the biggest change in air traffic control since radar". > > Claude Cheers, Phil
From: Peter C. Chapin on 12 Jun 2010 08:16
Yannick Duchêne (Hibou57) wrote: > I did not tried it yet, so I will not any about the present state (I've > just noticed it support the syntax). What is sure, is that support (or > better support) for generic is planed for the futur... and is already > present in SPARK Pro (if I'm not wrong). Aside from one special case, generics are not yet in SPARK Pro. I understand that some (reasonable) level of support for generics is planned for a future release, however. Disclaimer: I'm not an Altran Praxis employee. I only know what I've heard elsewhere. Peter |