Re: SPARK : third example for Roesetta - reviewers welcome

["Peter C. Chapin" <chapinp@acm.org>]

On 2010-08-17 05:15, Phil Thornley wrote:

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

I've noticed this as well and I agree that it is a good thing. Sometimes
I use SPARK to try an prove quite a bit. Sometimes I just try to prove
freedom from run time errors. Sometimes I just use the flow analysis and
stop there. All of these options get followed at different places in the
same program depending on time, effort required, criticality, etc.

I suppose it's the same with any kind of analysis tool and it's
reflective of the tool-like nature of SPARK.

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

That's interesting to know.

I can see why the group did not want standardize a safe subset. After
all many different subsets could be imagined and what constitutes "safe"
is going to depend on the application and on the analysis technology
available. As I understand it SPARK has evolved as analysis techniques
have improved. It will probably continue to do so. Other, similar
systems with slightly different needs could potentially exist using
different subsets as well.

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

I'm not really worried about it. Still it would be great if interest in
SPARK or SPARK-like systems became so widespread that people did start
worrying about it!

Peter