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.2 required=5.0 tests=BAYES_00,INVALID_MSGID,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
X-Google-Thread: f43e6,2c6139ce13be9980
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 1108a1,2c6139ce13be9980
X-Google-Attributes: gid1108a1,public
From: Ken Garlington <kennieg@flash.net>
Subject: Re: Safety-critical development in Ada and Eiffel
Date: 1997/08/23
Message-ID: <33FFA82E.54A8@flash.net>#1/1
X-Deja-AN: 268275645
References: <33E9ADE9.4709@flash.net> <EEsF5y.F5H@syd.csa.com.au>
 <JSA.97Aug12131358@alexandria.organon.com> <33F133D7.71AC@erols.com>
 <33F25933.7F83@flash.net> <33F30341.19F7DDE6@calfp.co.uk>
 <33F832E2.D5322D28@munich.netsurf.de> <33FA7611.4E16@flash.net>
 <33FB8974.97D4BA5D@munich.netsurf.de>
Organization: Flashnet Communications, http://www.flash.net
Reply-To: Ken.Garlington@computer.org
Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel
Date: 1997-08-23T00:00:00+00:00
List-Id: <comp.lang.ada>


Joachim Durchholz wrote:
> 
> The advantage of this being part of the language definition is that
> a) the conventions are the same for every shop (a mere comment
> convention might be different, creating incompatibilities not with the
> executable code but with the development environments)
> b) Eiffel can make use of executable assertions and compile them as
> run-time checks.
>
> [snip] 
>
> Eiffel assertions are not compiled if they take the form of a comment.

Then they aren't Eiffel assertions, per the definition you gave in (a)
and (b)!

> You can write something like
> 
>   feature sqrt (x: real): real is
>   require
>     nonnegative_argument: x >= 0
>   do
>     ... (lots of code omitted)
>   ensure
>     nonnegative_result: Result >= 0
>     maximum_precision: -- Every mantissa bit except the last is correct
>   end
> 
> The short tool will report this routine as
> 
>   feature sqrt (x: real): real is
>   require
>     nonnegative_argument: x >= 0
>   ensure
>     nonnegative_result: Result >= 0
>     maximum_precision: -- Every mantissa bit except the last is correct
>   end
> 
> so executable and non-executable assertions aren't handled any
> differently for documentation purposes.

Nor would they be handled any differently in Ada, etc.
To repeat: For those items in comments, what advantage does
Eiffel provide?

> 
> Regards,
> Joachim
> --
> Please don't send unsolicited ads.