SPARK: What does it prove?

SPARK: What does it prove?

[Peter C. Chapin]

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

Re: SPARK: What does it prove?

[Rod Chapman]

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?

Re: SPARK: What does it prove?

[Peter C. Chapin]

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

Re: SPARK: What does it prove?

[Marco]

On May 28, 6:55 am, Rod Chapman <roderick.chap...@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.

Re: SPARK: What does it prove?

[mockturtle]

On May 29, 4:42 pm, Marco <prenom_no...@yahoo.com> wrote:
> On May 28, 6:55 am, Rod Chapman <roderick.chap...@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...

Re: SPARK: What does it prove?

[BrianG]

mockturtle wrote:
> On May 29, 4:42 pm, Marco <prenom_no...@yahoo.com> wrote:
>> On May 28, 6:55 am, Rod Chapman <roderick.chap...@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...
Ditto, on both counts.

Re: SPARK: What does it prove?

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 15:25:50 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:

> 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! :)
You're welcome

> 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.
This leaves open the question of the interpretation, indeed (see later),  
and that is expected, nothing else can be expected.

> 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.
Formal semantics, that is, the same kind of logic SPARK already deals with  
;)

> It is my
> understanding that SPARK95 does not have a formal semantics.
Not the one of a programming language, which it is not (this is Ada's  
role, could it be a subset or not), while it still have a semantic :  
logic, boolean algebra, the atoms of complexity.

> 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?
May they did act like physicians instead of like mathematicians in this  
particular area. If they ever observe something going into a wrong  
direction, they will update some rules. If this is done as seriously as  
physicians do they own job, it is somewhat trustable.

> 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.
(see later)

> I guess this is why Praxis calls SPARK a semi-formal method.
Ouch, I did not read this. Semi-Formal ? Semi ?

> 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.
This seems to implies there is a way to do reliable without formal proofs.  
Is that true ?

> 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!
Good

> 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?)
Do you have a link please ? (providing this is not a paper article).

> 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:
Hoare would have loved it.

> 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.
OK, sorry, can't read this.

> 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?).
“Do any ?” : I believe if there is some, these are languages with very  
specific targets, like CPU design.

> It seems a shame, though, that Ada does not have one
> considering especially the way Ada is used.
Well, “shame” is a lot said.

So, after multiple “(see later)”, here is what I was to say : SPARK is a  
language. A language has a target domain (human languages too). To target  
its domain, it has some capabilities at expressing things about subjects  
of its domain, and it will always only talk about these subject, in its  
only possible terms.

Does what this language will say will makes sense ?

Surely, what the language will say will always be different than the  
subjects it will talk about, as it will always talk about it in some terms  
of interest : the target. The same could be said about any talks.

Now, SPARK is a metalanguage, that is, a language which tells about  
another language and its target is logic. It has and was given  
capabilities in logic, so it will talk about a program using logic  
lightings. Does it make sens ? Depends... if for you, an Ada application  
is mainly a matter of logic, this will, if this is not, then this will not.

If it is, then can add that the main target of SPARK is soundness, so it  
will talk about Ada application's soundness. That is all, and no less too.  
If something else is needed, then something else, or may be another  
formalism or another language will be needed.

Remains the question of possible weakness time-bombs in this heaven of  
soundness, and I feel this was your main question.

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

Re: SPARK: What does it prove?

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 15:25:50 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> 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.
The question, “what does it prove ?”, raise another corollary question,  
which is “what can it says ?” or “what can it talks about ?”.

I'm currently trying to make proofs on some binary stuffs, which has  
always seems obvious to me, and at the time of trying to prove it, I see I  
can't even prove the third of the initial postcondition I wanted my  
functions to have, because there are some I can't prove at all (I'm not  
talking about RTC, rather about postcondition expressing properties, and  
it is far less easy than proving RTC conditions).

If is funny to note that these difficulty are a consequence of SPARK tied  
to Ada. An example : Ada has modular type, but can't see modular types has  
polynomials, and the relevant modal, which could help, would be this one :  
polynomial. Has Ada don't has this, SPARK doesn't too.

Another things also : sometime, it is better to make proof on an abstract  
algorithm, which not efficient, and it is too much difficult to the same  
proof (prove postconditions from preconditions and the algorithm) with the  
efficient version. However, it would be more easy to demonstrate than the  
efficient algorithm is an equivalent transformation of the more abstract  
non-efficient one.

I mean, prove something on function F, demonstrate function G is  
equivalent to function F, so as legally assert the postconditions of F are  
also prove on G, because there was on F and G is equivalent to F.

This is another kind of thing SPARK cannot express or talk/say about.

This may be the start of some answers to the question “what can it proves  
?” or “what can't it proves ?”, which are similar questions.

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

Re: SPARK: What does it prove?

[Yannick Duchêne (Hibou57)]

Le Mon, 31 May 2010 03:17:32 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> If is funny to note that these difficulty are a consequence of SPARK  
> tied to Ada. An example : Ada has modular type, but can't see modular  
> types has polynomials, and the relevant modal, which could help, would  
> be this one : polynomial. Has Ada don't has this, SPARK doesn't too.
Typo errors : replace Has by As every where it is relevant.
Sorry, it seems when I am writing, I mostly write words as a whole instead  
of writing letters one by one, so it happens I replace a word by another.

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

Re: SPARK: What does it prove?

[Phil Thornley]

On 31 May, 02:17, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> Another things also : sometime, it is better to make proof on an abstract  
> algorithm, which not efficient, and it is too much difficult to the same  
> proof (prove postconditions from preconditions and the algorithm) with the  
> efficient version. However, it would be more easy to demonstrate than the  
> efficient algorithm is an equivalent transformation of the more abstract  
> non-efficient one.
>
> I mean, prove something on function F, demonstrate function G is  
> equivalent to function F, so as legally assert the postconditions of F are  
> also prove on G, because there was on F and G is equivalent to F.
>
> This is another kind of thing SPARK cannot express or talk/say about.

How about using proof abstraction?  Put one set of post-conditions
(for the inefficient version) on the spec and the other set (for the
efficient version) on the body.

Then the post-conditions on the body are proved from the code and the
post-conditions on the spec are proved by a user rule that is
justified by the 'offline' proof of equivalence of the two algorithms.

*** BUT *** the current GPL version (8.1.1) sometimes gets that post-
condition refinement VC wrong.  This only seems to happen when there
is a refined pre and post-condition on the body but no refined state
data, eg for private types, which is where I came across the problem.
(Notified to report@gnat.com on 9th February).

Cheers,

Phil

Re: SPARK: What does it prove?

[Jeffrey R. Carter]

On May 28, 6:25 am, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
>
> 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.
>
> 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.

I think you're mistaken: these applied only to Ada 80 (MIL-STD-1815).