From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,6d79efdb8dde2c5a
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!kanaga.switch.ch!switch.ch!news.belwue.de!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Categories for SPARK on Rosetta Code (Was: SPARK : third example
 for Roesetta - reviewers welcome)
Newsgroups: comp.lang.ada
User-Agent: 40tude_Dialog/2.0.15.1
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: 8bit
Reply-To: mailbox@dmitry-kazakov.de
Organization: cbb software GmbH
References: <op.vhguffh3ule2fv@garhos>
 <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com>
 <i49oif$1c85$1@adenine.netfront.net> <op.vhh3bwnwxmjfy8@garhos>
 <82mxsnuhbq.fsf@stephe-leake.org>
 <b08743ce-a85f-4962-8fbb-c2601b9cc4a1@x21g2000yqa.googlegroups.com>
 <op.vhjindufxmjfy8@garhos> <4c69a251$0$2371$4d3efbfe@news.sover.net>
 <op.vhjyi5kkxmjfy8@garhos> <4c69cd5f$0$2375$4d3efbfe@news.sover.net>
 <e614687a-58ce-499f-a6af-a5893cbdc812@q22g2000yqm.googlegroups.com>
 <1ddee5a6-fc25-4d23-bebd-3364923d0aa5@z10g2000yqb.googlegroups.com>
 <aihbzmy85j4v.163hyfnglvwus.dlg@40tude.net>
 <7cf71c68-4faf-4a7b-a350-405ff7f12ff9@z10g2000yqb.googlegroups.com>
 <4xb6sjkpzo1r$.138841gile5s0$.dlg@40tude.net>
 <87wrrnjf9f.fsf_-_@hugsarin.sparre-andersen.dk>
 <3ed38f7f-372d-422e-9bda-eca8a73d3f0d@x21g2000yqa.googlegroups.com>
 <i4lh4b$gqc$1@news.eternal-september.org>
 <1ncf62lqqj7ab$.1czxyaw96dl17.dlg@40tude.net>
 <i4ljfe$odg$1@news.eternal-september.org>
Date: Fri, 20 Aug 2010 12:24:19 +0200
Message-ID: <1y0wcz3etd5au.1kgyc5ls0w5kk$.dlg@40tude.net>
NNTP-Posting-Date: 20 Aug 2010 12:24:15 CEST
NNTP-Posting-Host: a1aa3c22.newsspool4.arcor-online.net
X-Trace: 
 DXC=;@RmA3a3B^k_0Po7BmQ3]l4IUK<Cl32<a4Fo<]lROoRa8kF<OcfhCOkk;l04HU8DNl[6LHn;2LCVn[<mhadbfdUk6W5>9SfENmicEOVClS:Sab
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:13535
Date: 2010-08-20T12:24:15+02:00
List-Id: <comp.lang.ada>

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