Re: Declaration of function in precondition

[Adam Beneschan <adambeneschan@gmail.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."

                            -- Adam