Re: On pragma Precondition etc.

["Alex R. Mosteo" <devnull@mailinator.com>]

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!