Declaration of function in precondition

[Simon Wright <simon@pushface.org>]

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