Re: On pragma Precondition etc.

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

mockturtle wrote:

> 
> 
> stefan-lu...@see-the.signature ha scritto:
> 
>> On Fri, 25 Jul 2008, Georg Bauhaus wrote:
>>
>> > We would have something like
>> >
>> >    function More(X, Y: Integer);
>> >    -- ...
>> >    pragma Precondition(More, X > 2 * Y);
>> >
>> >
>> >    function Less(X, Y: Integer);
>> >    -- ...
>> >    pragma Precondition(Less, X < 2 * Y);
>> >
>> > And now there is no doubt about the subprogram to which a
>> > Pre-/Postcondition belongs.  (A rule that a spec Pre-/Postcondition
>> > pragma must come right after its subprogram will establish
>> > consistency.)
>>
>> This seems to break with overloading of subprogram names. I seem to recall
>> that
>>   "pragma Inline(Foo)"
>> is asking to inlie *all* functions / procedures with the name "Foo". This
>> may be OK for inlining, but you definitively don't want to use the same
>> preconditions which happen to have the same way. Consider the following:
> 
> What about _allowing_ for the name of the procedure to appear in
> the pragma?  The true syntactic link would be given by the pragma
> position
> and the procedure name would act as a "double check" to be sure that
> things were not messed up.  Of course this does not save you if you
> permute the pragma of overloaded functions...
> 
> ---

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?