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: 103376,585fd78267abd80c
X-Google-Attributes: gid103376,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news4.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: "Alex R. Mosteo" <devnull@mailinator.com>
Newsgroups: comp.lang.ada
Subject: Re: On pragma Precondition etc.
Date: Mon, 28 Jul 2008 10:02:03 +0200
Message-ID: <6f5cknF9onjlU3@mid.individual.net>
References: <4889886d$0$18827$9b4e6d93@newsspool2.arcor-online.net>
 <Pine.LNX.4.64.0807251224010.10913@medsec1.medien.uni-weimar.de>
 <f9112d8f-1c5a-4533-88ed-b4c22d108ac8@q5g2000prf.googlegroups.com>
 <6etsi6F8mbmbU2@mid.individual.net>
 <4889bf57$0$9508$9b4e6d93@newsspool3.arcor-online.net>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7Bit
X-Trace: individual.net H2WbAipCeKJ/YYq7ixJY1gSSYWeTousbxOAXCwosqBkgSH418=
Cancel-Lock: sha1:6zbURJBjXI6ooqb+YCwP/Eq/JKs=
User-Agent: KNode/0.10.9
Xref: g2news1.google.com comp.lang.ada:1360
Date: 2008-07-28T10:02:03+02:00
List-Id: <comp.lang.ada>

Georg Bauhaus wrote:

> Alex R. Mosteo schrieb:
> 
>> Piling more suggestions: I understand the point of using pragmas by Gnat at
>> this stage, but if this is going to be standardized perhaps the syntax of a
>> declaration could be changed. For example:
>> 
>> function Foo (X, Y : Something) return Whatever with
>>   Precondition (Blah) and
>>   Postcondition (Urgh);
>> 
>> So now it is all a indivisible whole and the OP concern is gone.
>> 
>> I haven't seen Eiffel code. How do they do this?
> 
> feature Foo(X, Y : SOMETHING): WHATEVER is
> -- short comment
> require
> Precondition_Name: Blah
> do
> ...
> ensure
> Postcondition_Name: Urgh
> end
> 
> The Pre-/Postcondition_Name serves a purpose similar to the
> message parameter of Ada's pragmas.)
> 
> Eiffel's "contract view" of the class then hides the statements
> of Foo. So you get a "spec".
> 
> feature Foo(X, Y : SOMETHING): WHATEVER is
> -- short comment
> require
> Precondition_Name: Blah
> ensure
> Postcondition_Name: Urgh
> 
> 
> In addition, Eiffel's Pre-/Postcondition have inheritance rules
> for the conditions.  Another spot where Ada would to be more
> general.

Very interesting, thanks!