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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	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!news1.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!feeder.news-service.com!85.214.198.2.MISMATCH!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: "J-P. Rosen" <rosen@adalog.fr>
Newsgroups: comp.lang.ada
Subject: Re: Categories for SPARK on Rosetta Code (Was: SPARK : third example
 for Roesetta - reviewers welcome)
Date: Fri, 20 Aug 2010 13:36:40 +0200
Organization: Adalog
Message-ID: <i4lpco$d44$1@news.eternal-september.org>
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>
 <1y0wcz3etd5au.1kgyc5ls0w5kk$.dlg@40tude.net>
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 20 Aug 2010 11:36:56 +0000 (UTC)
Injection-Info: mx03.eternal-september.org;
 posting-host="Dn22F68J9CHYFQQlT81DGA";
	logging-data="13444"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/v0T71RCDF1E4jeUBp7/k3"
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; fr;
 rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2
In-Reply-To: <1y0wcz3etd5au.1kgyc5ls0w5kk$.dlg@40tude.net>
Cancel-Lock: sha1:OYPPYnvr4cHdUCkQnTsSXT9j9Xs=
Xref: g2news1.google.com comp.lang.ada:13536
Date: 2010-08-20T13:36:40+02:00
List-Id: <comp.lang.ada>

Le 20/08/2010 12:24, Dmitry A. Kazakov a �crit :
> 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?
Sure, it's even close to machine code ;-)

> Can't it be analyzed formally?
No. As soon as you have address arithmetic, no semantic can be
guaranteed. Well, it depends on what you call "formally" TBH.

[...]
>> 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.
> 
I thought about that after I sent the message. I really meant "without
any semantic effect on the generated code (in the absence of violations)"

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