Re: What is SPARK about?

[Phil Thornley <phil.jpthornley@gmail.com>]

On 11 June, 21:32, Claude <claude.def...@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