* Re: SPARK: What does it prove?
2010-05-28 13:25 SPARK: What does it prove? Peter C. Chapin
@ 2010-05-28 13:55 ` Rod Chapman
2010-05-28 15:58 ` Peter C. Chapin
2010-05-29 14:42 ` Marco
2010-05-30 13:06 ` Yannick Duchêne (Hibou57)
` (2 subsequent siblings)
3 siblings, 2 replies; 11+ messages in thread
From: Rod Chapman @ 2010-05-28 13:55 UTC (permalink / raw)
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?
^ permalink raw reply [flat|nested] 11+ messages in thread* Re: SPARK: What does it prove?
2010-05-28 13:25 SPARK: What does it prove? Peter C. Chapin
2010-05-28 13:55 ` Rod Chapman
@ 2010-05-30 13:06 ` Yannick Duchêne (Hibou57)
2010-05-31 1:17 ` Yannick Duchêne (Hibou57)
2010-05-31 23:36 ` Jeffrey R. Carter
3 siblings, 0 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-05-30 13:06 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK: What does it prove?
2010-05-28 13:25 SPARK: What does it prove? Peter C. Chapin
2010-05-28 13:55 ` Rod Chapman
2010-05-30 13:06 ` Yannick Duchêne (Hibou57)
@ 2010-05-31 1:17 ` Yannick Duchêne (Hibou57)
2010-05-31 1:21 ` Yannick Duchêne (Hibou57)
2010-05-31 13:05 ` Phil Thornley
2010-05-31 23:36 ` Jeffrey R. Carter
3 siblings, 2 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-05-31 1:17 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK: What does it prove?
2010-05-28 13:25 SPARK: What does it prove? Peter C. Chapin
` (2 preceding siblings ...)
2010-05-31 1:17 ` Yannick Duchêne (Hibou57)
@ 2010-05-31 23:36 ` Jeffrey R. Carter
3 siblings, 0 replies; 11+ messages in thread
From: Jeffrey R. Carter @ 2010-05-31 23:36 UTC (permalink / raw)
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).
^ permalink raw reply [flat|nested] 11+ messages in thread