Re: Categories for SPARK on Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome)

["J-P. Rosen" <rosen@adalog.fr>]

Le 20/08/2010 14:25, Dmitry A. Kazakov a �crit :
>> No. As soon as you have address arithmetic, no semantic can be
>> guaranteed. Well, it depends on what you call "formally" TBH.
> 
> But the definition does not hint what kind of properties have to be
> analyzed (and when).
It's on purpose. A category should be broad enough. We can discuss
whether "static" should be put in, but I think it is important to keep
"formal".

> You mean the case when the code "supporting analysis" is dead code! What
> kind of "support" is to include unreachable code?
Of course. Spark's annotation have no effect on correct programs.

> If it supports anybody,
> then memory chips vendors. Then a dynamically typed language with its
> "message not understood" would qualify for the same reasons as Eiffel.
> 
Anybody can argue about what "formal verification" means, but the same
is true of "strongly typed". Even in C, there are cases of code that
does not compile because of type mismatches...

It would make no sense to introduce a category "has Spark annotations".
We need something broader. And a minimum of honesty is needed when
checking the box. The only issue is to make sure that the casual reader
understands that it means: "has special features directed specifically
to analysis". Could be "has assertions", but that seems too restrictive
to me. So please, if you have a better idea, I'd be delighted to hear
about it.

-- 
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr