Re: Question about out parameters of unconstrained array type.

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 12-02-26 14:25 , Alexander Senier wrote:
> On Sun, 26 Feb 2012 09:14:53 -0000
> Phil Thornley<phil.jpthornley@gmail.com>  wrote:
>
>> For your code above, if the cost of including the initialization of the
>> array is too high then the easiest way to remove the the error is
>> probably to add another parameter that is the length of the Description
>> string. Using Alexander's code:
>
> Can anybody comment on the legality of using attributes of an out parameter of
> an unconstrained (array) type in Ada? A brief skim through LRM could not
> enlighten me...

It is entirely legal. Before an object can be passed as a parameter, the 
object must exist; when the object exists, all its attributes are 
defined (and the object is constrained, of course).

As you, I did not find a specific statement about the attributes of 
"out" parameters in the LRM. But 3.6.2(5) says that A'Length is defined 
for any array object A. Since this rule makes no exception for objects 
that are "out" parameters, they too have a 'Length.

>
> If using 'Length (and other attributes) elsewhere than in a loop constraint
> actually is legal Ada, than this seems like an unnecessary limitation of SPARK
> that should be relaxed.

When I looked at SPARK a couple of years ago, I felt it had several such 
annoying and (at least seemingly) unnecessary limitations. As I recall, 
many limitations seemed to me to be relicts of the earlier Pascal-based 
SPARK ancestor, where the extension to Ada took the path of least 
effort, in the sense that SPARK allows simple Pascal-like Ada code while 
rejecting semantically equivalent but more Ada-like code.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .