From: Peter C. Chapin on
There has been a lot of discussion about SPARK on this group recently. That's
great, but I hope those who are more interested in full Ada aren't getting
annoyed! :)

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. Thus the
Examiner is producing VCs based on the informal description of Ada in the
reference manual. What if that information description is, as many such
descriptions are, logically inconsistent or ambiguous? I realize that SPARK
is intended to restrict the Ada language to remove ambiguity and
implementation specific behavior, but is there a proof that it actually does?

Without a formal semantics of SPARK, then it seems like the "proofs" produced
by the tools are not really proving anything... in a mathematically rigorous
sense at least. I guess this is why Praxis calls SPARK a semi-formal method.

I understand that the real goals of SPARK are to help practitioners produce
reliable software... not generate rigorous proofs just for the sake of doing
so. To that end, following the informal specification of Ada in the reference
manual seems perfectly reasonable. The features of Ada that SPARK retains are
simple with (mostly) "obvious" semantics, so why quibble over every
mathematical detail? I'm fine with that. The tools *do* help me write more
reliable programs and that's great!

Still it would be more satisfying if there was a formal semantics for SPARK
to "back up" what the tools are doing. I actually read an article recently
about programming language semantics that mentioned (is this true?) that one
of the original requirements in the development of Ada was the production of
a formal semantics for Ada. I even understand that there were two attempts to
produce such a semantics. Here are those references:

1. V. Donezeau-Gouge, G. Kahn, and B. Lang. On the formal definition of Ada.
In Semantics-Directed Compiler Generation, Lecture Notes in Computer Science,
vol 94, pp 475-489, Springer, Berlin, 1980

2. D. Bjorner and O.N. Oest. Towards a Formal Description of Ada, Lecture
Notes in Computer Science, vol 98, Springer, Berlin 1980.

The article I'm reading is "Programming Language Description Languages" by
Peter D. Moses in the book "Formal Methods: State of the Art and New
Directions" edited by Paul P. Boca, Janathan P. Bowen, and Jawed I. Siddiqi,
published by Springer, (C) 2010.

I understand that the efforts above were incomplete and even then only apply
to Ada 83. I also understand that few full scale languages have a formal
semantics (do any?). It seems a shame, though, that Ada does not have one
considering especially the way Ada is used.

Peter

From: Rod Chapman on
On May 28, 2:25 pm, "Peter C. Chapin" <pcc482...(a)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?
From: Peter C. Chapin on
Rod Chapman wrote:

> 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.

That's interesting to know. Thanks.

> 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...

Yes, definitely. This was a point I tried to make in a different thread
related to testing SPARK programs (and the value of doing so). SPARK helps
show that the source code is in some sense correct, which is great, but
that's not the whole story.

> In short: it seems to work.

Absolutely. I hope you didn't take my post as a criticism of SPARK. If the
goal is to reduce errors in actual deployed programs, which at the end of the
day is the important thing it seems, then I agree that SPARK works!

Peter

From: Marco on
On May 28, 6:55 am, Rod Chapman <roderick.chap...(a)googlemail.com>
wrote:
>
> PS...if the SPARK traffic here really does get annoyingly high,
> then perhaps we should create comp.lang.ada.spark?

No - I enjoy the SPARK threads even though I am not using it (yet).
Traffic volume on this group is light and respectful.
From: mockturtle on
On May 29, 4:42 pm, Marco <prenom_no...(a)yahoo.com> wrote:
> On May 28, 6:55 am, Rod Chapman <roderick.chap...(a)googlemail.com>
> wrote:
>
>
>
> > PS...if the SPARK traffic here really does get annoyingly high,
> > then perhaps we should create comp.lang.ada.spark?
>
>  No - I enjoy the SPARK threads even though I am not using it (yet).
>  Traffic volume on this group is light and respectful.

+1 Marco just took the words out of my mouth (err.. keyboard? :-)
"yet" included...
 |  Next  |  Last
Pages: 1 2 3
Prev: SPARK and testing.
Next: SPARK and modular types