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 11:55:43 +0200, J-P. Rosen wrote:

> Le 20/08/2010 11:23, Dmitry A. Kazakov a �crit :
>>> What about "supports formal analysis" ?
>> 
>> That provokes the question - analysis of what?
>> 
> Of the code, for sure ;-)

Doesn't C has code? Can't it be analyzed formally?

> If you mean: what kind of outcome from the analysis, I think it is
> better to leave it open. We don't want a special category for Spark
> where only Spark would get a mark.

Why not. I think that the category should indicate that the language
promotes static formal analysis as a necessary and integral part of
software design.

> The important parts here is "supports" (as opposed to "allows"), i.e.
> the language includes features intended only for formal analysis,
> without any effect on the generated code.
> 
> I guess Eiffel would qualify too.

Only because the keyword "static" was lost. Dynamic formal analysis is
certainly possible and useful too, but it relates to the language in the
same way morbid anatomy does to therapy.

BTW, "without any effect on the generated code" would disqualify Eiffel
anyway.

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