Declaration of function in precondition

Declaration of function in precondition

[Simon Wright]

I proposed this in answer to a question[1] on StackOverflow:

   package RingBuffer is
      function Is_Full return Boolean;
      procedure Push(value: T) with Pre => not Is_Full;
      function Pop return T;
   private
      buffer: array(0..size) of T;
      readptr: integer := 0;
      writeptr: integer := 1;
      function Is_Full return Boolean is (Readptr = Writeptr);
   end RingBuffer;

and it turns out that GNAT (GPL 2013, 4.9-20140119) is happy if I put
the spec of Is_Full after its use (but still in the visible part):

      procedure Push(value: T) with Pre => not Is_Full;
      function Is_Full return Boolean;

I can't see where in the ARM this is legalised?

[1] http://stackoverflow.com/questions/23203022/ada-aspects-which-are-private-to-a-package

Re: Declaration of function in precondition

[Adam Beneschan]

On Thursday, April 24, 2014 3:12:55 AM UTC-7, Simon Wright wrote:
> I proposed this in answer to a question[1] on StackOverflow:
> 
> 
> 
>    package RingBuffer is
>       function Is_Full return Boolean;
>       procedure Push(value: T) with Pre => not Is_Full;
>       function Pop return T;
>    private
>       buffer: array(0..size) of T;
>       readptr: integer := 0;
>       writeptr: integer := 1;
>       function Is_Full return Boolean is (Readptr = Writeptr);
>    end RingBuffer;
> 
> and it turns out that GNAT (GPL 2013, 4.9-20140119) is happy if I put
> the spec of Is_Full after its use (but still in the visible part):
> 
>       procedure Push(value: T) with Pre => not Is_Full;
>       function Is_Full return Boolean;
> 
> I can't see where in the ARM this is legalised?

13.1.1(11), I think.  But I'm not sure.

"The usage names in an aspect_definition are not resolved at the point of the associated declaration, but rather are resolved at the end of the immediately enclosing declaration list."

                            -- Adam

Re: Declaration of function in precondition

[Randy Brukardt]

"Adam Beneschan" <adambeneschan@gmail.com> wrote in message 
news:5a38852c-512e-43c4-9c02-cdcf105f0397@googlegroups.com...
> On Thursday, April 24, 2014 3:12:55 AM UTC-7, Simon Wright wrote:
>> I proposed this in answer to a question[1] on StackOverflow:
>>
>>
>>
>>    package RingBuffer is
>>       function Is_Full return Boolean;
>>       procedure Push(value: T) with Pre => not Is_Full;
>>       function Pop return T;
>>    private
>>       buffer: array(0..size) of T;
>>       readptr: integer := 0;
>>       writeptr: integer := 1;
>>       function Is_Full return Boolean is (Readptr = Writeptr);
>>    end RingBuffer;
>>
>> and it turns out that GNAT (GPL 2013, 4.9-20140119) is happy if I put
>> the spec of Is_Full after its use (but still in the visible part):
>>
>>       procedure Push(value: T) with Pre => not Is_Full;
>>       function Is_Full return Boolean;
>>
>> I can't see where in the ARM this is legalised?
>
> 13.1.1(11), I think.  But I'm not sure.
>
> "The usage names in an aspect_definition are not resolved at the point of 
> the associated declaration, but rather are resolved at the end of the 
> immediately enclosing declaration list."

Correct. In this case, aspect specifications are resolved at "private", so 
you can use anything in the visible part in them.

This property is necessary for some type-related aspects, else they would be 
useless:

    type Priv is private with Read => Read, Write => Write, Type_Invariant 
=> Is_Valid(Priv);

Since all of these need access to subprograms that have parameters of type 
Priv, and those *have* to follow the type declaration of Priv, none of these 
things could have been specified as aspects without this (admittedly 
strange) rule.

Most aspects are evaluated at the first freezing point of the associated 
entity (type in this case), so oddities are possible. There are some rules 
to prevent the worst ones -- but it's very unlikely that you'll ever run 
into them. After all, "the first freezing point" is something you worry 
about only if the compiler complains, and I recommend the same approach 
here. (Coincidentally, I was working on objectives and ACATS tests for those 
rules yesterday, so I'm more aware than usual about them.)

                                 Randy.