Re: SPARK : third example for Roesetta - reviewers welcome

[Phil Thornley <phil.jpthornley@gmail.com>]

On 17 Aug, 00:43, "Peter C. Chapin" <chap...@acm.org> wrote:
> On 2010-08-16 18:38, Yannick Duchêne (Hibou57) wrote:
>
[...]
> > For the time, unless some news comes in the place, I will end with this
> > conclusion: SPARK's not a language, that's Praxis's tool.
>
> When people ask me what SPARK is about I tell them it's an annotated
> subset of Ada together with a tool set that can be used for deep static
> analysis of that annotated language. It seems to me that SPARK is both a
> language and a tool.
>
> Perhaps this gets back to a question Phil raised: does it make sense on
> Rosetta to differentiate between SPARK and SPARK+proofs?
I've thought about that one a bit more and decided that it's probably
not a good idea - using SPARK is much more of a continuum of
approaches.
[Which is a Very Good Thing(TM) - new users can start by ignoring
proof completely.  Then start proving that the code is type safe
without having to even think about formal specifications - and
complete their type safety proofs ranging from the completely informal
(proof by review) up to the completely formal (check annotations,
where they work, and the Proof Checker otherwise).  Then move into the
formal spec world of contracts expressed through pre and post
conditions.]

I'm going to try and come up with an explanation of SPARK for Rosetta
Code that covers all the ground, but is as succinct as possible (so no-
one should be holding their breath for that).  I'll link out to
detailed descriptions where possible.

[...]
> > By the way, if this is really a Praxis's tool as I suppose now, do I
> > have to understand there will be always one single implementation of
> > SPARK and a single provider in this area ?
>
> That's an interesting question.
>
> Oracle is suing Google over Google's use of Java in Android. I suppose
> this is the nasty quagmire one gets into whenever one starts using
> proprietary languages. Thankfully Ada has an international standard so
> the Ada community can avoid some of that. However, there is no
> international standard for SPARK. At least not as far as I know.
That was one of the first questions that the Annex H Rapporteur Group
looked at when it was formed following the publication of the Ada95
standard.  Should the Group define a 'safe subset' for Ada and, if so,
should that subset be SPARK?  The Group fairly quickly decided against
defining a standard subset so the question about SPARK never arose.

The tools are now GPL'ed, but the documentation is all copyright
Altran-Praxis and the SPARK LRM is also Crown Copyright (probably
after some early funding from the UK MoD).  I don't know enough about
these issues to say what effect that has on restricting other
organisations' ability to develop new versions of the language and
tools.

> ... Will it become the Java of the formal methods community?
Not until Altran-Praxis start making a great deal more money out of it
than they do at present.

Cheers,

Phil