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,FREEMAIL_FROM
	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
Path: 
 g2news2.google.com!postnews.google.com!x6g2000vbg.googlegroups.com!not-for-mail
From: =?ISO-8859-1?Q?Hibou57_=28Yannick_Duch=EAne=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: Re: Ada vs Eiffel - Ada programmer approach
Date: Thu, 4 Jun 2009 00:30:16 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <a924d96e-17b8-4573-ae86-3ccc924d21c8@x6g2000vbg.googlegroups.com>
References: 
 <405b5054-4c8f-4e16-9ea8-503a9b9f976e@t21g2000yqi.googlegroups.com>
	<4A19765C.608@obry.net>
 <8105b65f-4de9-4653-b43a-d55ee33f072d@k2g2000yql.googlegroups.com>
NNTP-Posting-Host: 86.75.149.31
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1244100616 19069 127.0.0.1 (4 Jun 2009 07:30:16
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 4 Jun 2009 07:30:16 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: x6g2000vbg.googlegroups.com; posting-host=86.75.149.31;
	posting-account=vrfdLAoAAAAauX_3XwyXEwXCWN3A1l8D
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.1;
	fr),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6204
Date: 2009-06-04T00:30:16-07:00
List-Id: <comp.lang.ada>

On 26 mai, 15:37, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:
> [...] Ada's pragma Assert provides what I
> need in these (rare) cases =A0because I can put such pragmas in the
> middle of a subprogram, for example.
>
> --
> Ludovic Brenta.

This is not the same as Eiffel assertions. Eiffel's assertions are
aware of the invokation contexte. Let say you have a class C and a
method M and the class C has an invariant I. Then, if a client invoks
M, the invariant will be checked before M returns. That's Ok, this is
the same as with "in code assertions". But if M is invoked by anoher
method of the class, i.e. as an implementation method (this is very
common to use a public method for internal purpose), you will have
this : the client of C invok a method M2 which in turn will invok M
(the client may or may not know about it). In this context, the class
invariant will obviously be checked before returning from M2, but *it
will not be check before return from M*.

That is beceause M is allowed to left the class invariant in an
illegal state, as it may be the sole responsability of M2.

So, Eiffel's assertions are not the same as "in code assertions".
Eiffel's assertions are well formalized.