Re: SPARK: What does it prove?

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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.