Re: Lost in translation (with SPARK user rules)

["Peter C. Chapin" <pcc482719@gmail.com>]

Yannick Duchêne (Hibou57) wrote:

> That is where I was not agree with a previous similar sentence from  
> someone else. I don't see a reason why only critical applications should  
> benefit of verifiability. This would not be a waste to apply standard  
> logic to program construction, and I even feel this should be an expected  
> minimum.

I think the reason is that it's hard. SPARK's restrictions exist, in part, to
create a language that can manipulated in a reasonably formal way using
current technology. As soon as you start adding back exceptions, dynamic
memory, recursion, etc, etc, it becomes very hard (beyond the state of the
art?) to say significant things statically in formal way. Yet those features
*are* very useful for many programs.

I know there has been a lot of work done in the field of static analysis and I
hope the field continues to advance. As it does, SPARK, or something like it,
may be able to take on some of the complicated features it currently avoids.
Also, depending on your needs, other kinds of static analysis might be useful
besides formally proving program properties. So what I'm saying is that it
may be premature to think about incorporating the SPARK sublanguage formally
into the Ada standard. SPARK is a tool... one of many. I look forward to even
better tools in the future!

For example take a look at this:

        http://www.adacore.com/home/products/codepeer/

I believe this tool works with full Ada and it sounds pretty neat. Disclaimer:
I haven't tried it.

Peter