Re: On pragma Precondition etc.

[Robert A Duff <bobduff@shell01.TheWorld.com>]

stefan-lucks@see-the.signature writes:

> 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.

I don't think it's OK for pragma Inline (or Convention, or any of the
others).  The rules are confusing, especially the way they work with
renaming.

I think a better design would be to require every procedure to have a
unique name (plus, optionally, an overloaded name).

Syntax for pre/postconditions is a good idea, but for now it's a
GNAT-specific extension, so pragmas are better.

> An alternative would be to repeat the entire function declaration in the 
> pragma:
>
>   function More(X, Y: Integer) return Integer; 
>   pragma Precondition(function More(X,Y: Integer) return Integer, 
>                       X > 2 * Y); --1--

That's syntactically illegal.  The RM allows implementations to invent
pragmas, but does not allow them to modify the general syntax of
pragmas.

> would throw a bit too much of redundant information at the reader. 

Yeah, that too.

- Bob