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!news3.google.com!feeder.news-service.com!newsfeed.straub-nv.de!newsfeed.utanet.at!newsfeed01.chello.at!newsfeed.arcor.de!newsspool3.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> <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>
 <i4lpco$d44$1@news.eternal-september.org>
Date: Fri, 20 Aug 2010 14:25:17 +0200
Message-ID: <gcggor638e9z$.avh74wi399su.dlg@40tude.net>
NNTP-Posting-Date: 20 Aug 2010 14:25:13 CEST
NNTP-Posting-Host: 2cbe45a0.newsspool3.arcor-online.net
X-Trace: 
 DXC=gP?`6Q9R[UJAa;:RKVJ>LEMcF=Q^Z^V3H4Fo<]lROoRA8kF<OcfhCOKkkbeVcE8H^C[6LHn;2LCVN[<mhadbfdUK[;PnV;D7g7Bi<nm^Pl^=JN
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:13537
Date: 2010-08-20T14:25:13+02:00
List-Id: <comp.lang.ada>

On Fri, 20 Aug 2010 13:36:40 +0200, J-P. Rosen wrote:

> Le 20/08/2010 12:24, Dmitry A. Kazakov a �crit :

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

But the definition does not hint what kind of properties have to be
analyzed (and when).

> [...]
>>> 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)"

You mean the case when the code "supporting analysis" is dead code! What
kind of "support" is to include unreachable code? 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.

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