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

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 20 Aug 2010 15:28:31 +0200, J-P. Rosen wrote:

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

Yes

1. Formal in the sense that there is a specification.
2. Static, that verification happens before run time.

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

They do, because correctness itself depends on the annotation. If you
change the annotation, the program may become incorrect. Dead code does not
have this property.

> It would make no sense to introduce a category "has Spark annotations".

Yes.

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

I thought about a specific approach to programming, as it was proposed by
Dijkstra, with designing both the program and a proof that certain
properties of the program hold. SPARK's annotations support this approach.
This is not specific to SPARK.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de