Re: On pragma Precondition etc.

[stefan-lucks@see-the.signature]

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:

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

  function More(X, Y: Integer) return Boolean;
  pragma Precondition(More, (X>0) or (Y>0)); --2--

  function More(X, Y: Whatever) return Whatever; --3--

The intention is that precondition --1-- sticks to the function returning 
Integer and precondition --2-- sticks to the one returning Boolean -- not 
that both preconditions stick to both functions!

And neither precondition should stick to the function marked by --3--. 
Depending on the type Whatever, that shouldn't even compile ...

So the syntactical link between a subprogram declaration and its 
precondition cannot just depend on the subprogram name. But then, the 
function name actually becomes redundant, and the current GNAT convention 
appears to be the better one: 

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

  function More(X, Y: Integer) return Boolean;
  pragma Precondition((X>0) or (Y>0)); --2--

  function More(X, Y: Whatever) return Whatever; --3--

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

Ada is always a bit verbose, which often is good for readability. But this 
would throw a bit too much of redundant information at the reader. 

Stefan



-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------