From: Claude on
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
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
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
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
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