On pragma Precondition etc.

[Georg Bauhaus <rm.tsoh.plus-bug.bauhaus@maps.futureapps.de>]

A question about syntax.

Thanks to GNAT 2008, there is now some initial support
for stating preconditions and postconditions of supprograms,
using pragma Pre-/Postcondition.
Randy Brukardt has presented more thoughts on this to
the Ada Comments mailing list; notably, by describing
means to express a type's invariant, T'Constraint.

(GNAT's pragmas can be used to state conditions right after
the spec of a subprogram, and also at the start of
declarations of a supbrogram body. Thus,

  procedure Foo(X, Y: Natural);
  pragma Precondition(X > Y);)

My question is about the syntactical link of a Pre-/Postcondition
to a subprogram declaration.  Using GNAT's approach, the link is
implicit:
A spec Pre-/Postcondition applies to the immediately preceding
subprogram declaration and to nothing else.

At first sight it seems natural to *not* name the subprogram in
the Pre-/Postcondition pragma.  You could refer the questioner
to the Department of Redundancy Department.
On the other hand, there are opportunities for code restructuring.
What happens to the Pre-/Postconditions then?  I suggest the they
can get mixed up.  For example, exchange the alphabetical
order of the following function declarations in a hurry,

   function More(X, Y: Integer);
   -- ...
   pragma Precondition(X > 2 * Y);


   function Less(X, Y: Integer);
   -- ...
   pragma Precondition(X < 2 * Y);


So I would contend the lack of a *local_name* parameter
in the pragmas Pre-/Postcondition.

The parameter could be like those of pragma No_Return or
pragma Inline, making the link to the subprogram explicit.

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

(On the Ada Comments list, there seems to have been some agreement
that there should be some syntax in the future, perhaps obsoleting
this discussion...)