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: a07f3367d7,5add429c86f59001
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news4.google.com!feeder.news-service.com!newsfeed101.telia.com!nf02.dk.telia.net!news.tele.dk!news.tele.dk!small.news.tele.dk!bnewspeer01.bru.ops.eu.uu.net!bnewspeer00.bru.ops.eu.uu.net!emea.uu.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Tue, 26 May 2009 19:59:26 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Thunderbird 2.0.0.21 (Macintosh/20090302)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Ada vs Eiffel - Ada programmer approach
References: 
 <405b5054-4c8f-4e16-9ea8-503a9b9f976e@t21g2000yqi.googlegroups.com>
  <4A19765C.608@obry.net>
 <8105b65f-4de9-4653-b43a-d55ee33f072d@k2g2000yql.googlegroups.com>
 <130yh6dv3l1lf$.1729u4tpolgwi.dlg@40tude.net>
 <4a1c2652$0$30220$9b4e6d93@newsspool1.arcor-online.net>
 <1r1ho3wqsjncb.1p3p7qe2qcqmw.dlg@40tude.net>
In-Reply-To: <1r1ho3wqsjncb.1p3p7qe2qcqmw.dlg@40tude.net>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Message-ID: <4a1c2dfe$0$30236$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 26 May 2009 19:59:26 CEST
NNTP-Posting-Host: 19bc4a96.newsspool1.arcor-online.net
X-Trace: 
 DXC=OLH>:4@gG6^mG86`U=_nC_ic==]BZ:af^4Fo<]lROoRQ^YC2XCjHcbYhDM9OmT[e>\;9OJDO8_SKVNSZ1n^B98iZfFgLQF2HCPP
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news2.google.com comp.lang.ada:6024
Date: 2009-05-26T19:59:26+02:00
List-Id: <comp.lang.ada>

Dmitry A. Kazakov schrieb:

>>> Now, if Return_False is OK, then Is_OK returns True and then Return_False
>>> returns True and so it is not OK. So is it, or is it not?
>> Eiffel defines the conditions for when a contract's assertions
>> will be tested. In particular, not every call will
>> trigger the tests. ;-)
> 
> Certainly. They are tested when do not assert contracts. (:-))

Exactly.  That's an inside view of DbC modules.

>>  So the never ending loop above is
>> not a problem within the Eiffel DbC framework of definitions.
>> (The stack may overflow, though.)
> 
> There is no loop since "contract is satisfied" is not a variable. Otherwise
> you cannot design "by contract", obviously.

The Eiffel answer is that yes, you can do that because
in order to get anything done, assertion checking must
not happen at times.  That's a reasonable design, because
there is no practical alternative. ;-)


> Ada's static typing system and SPARK do it right.

SPARK imposes limitations that are not present when employing
DbC.  SPARK cannot replace DbC, or improve it, and vice versa,
basically because DbC (not used as static assertions only) and
SPARK are largely incommensurable.

This means that DbC and SPARK are both right:
You will --# hide certain uses of Ada constructs
in SPARK, for example.  Likewise, you will not
check all assertions in some situations when using
Eiffel DbC.