Re: SPARK: What does it prove?

[Rod Chapman <roderick.chapman@googlemail.com>]

On May 28, 2:25 pm, "Peter C. Chapin" <pcc482...@gmail.com> wrote:

> It is common to talk about SPARK proofs but of course what the Simplifier is
> actually proving are the verification conditions generated by the Examiner.
> Formally this leaves open the question of if those verification conditions
> have anything to do with reality or not. Ultimately, it seems to me, before
> one can formally prove anything about the behavior of a program one needs a
> formal semantics for the programming language in question. It is my
> understanding that SPARK95 does not have a formal semantics.

Well..not quite.  The VC generator was constructed and very much
based on the formal semantics for SPARK83 that was
contstructed in the mid-1990s.  We have _lots_ of confidence
that this semantics is completely upwards-compatible
and consistent with the canonical semantics of Ada95 and
this SPARK95 SPARK2005.

Unfortunately, we did not have the funding to keep
that SPARK83 semantics up to date with new features that
were added later like modular types from Ada95, but these
are a fairly modest extension to the language.

There are also lots of assumptions tha underlie any
"proof" of anything - in our case the integrity of the compiler,
linker and the rest of the build environment, the
implementation of the target processor itself and many
other things.  While these are valid concerns, these
assumptions really do seem to hold up in the "real world" - i.e.
with our customers using real commercial compilers, microprocessors
and so on.

In short: it seems to work.
 - Rod Chapman, SPARK Team, Praxis

PS...if the SPARK traffic here really does get annoyingly high,
then perhaps we should create comp.lang.ada.spark?