Question about out parameters of unconstrained array type.

Question about out parameters of unconstrained array type.

[Peter C. Chapin]

Consider a simple procedure

procedure P(S : out String) is
begin
    ...
end P;

Despite the fact that S behaves as if it is uninitialized my Ada 
compiler (GNAT GPL 2011) allows me to read certain attributes. For 
example if the body is

   for I in 1 .. S'Length loop ...

(never mind that I'm making a bad assumption about S'First being 1) I 
don't see any warning about reading an uninitialized value when I do 
S'Length. This is fine but I'm having trouble locating in the LRM where 
this behavior is explicitly said to be well defined. Is it well defined? 
Where does it say so?

The reason I'm asking is because SPARK does *not* like the usage of 
S'Length in my example above. I either have to 1) give the parameter 
mode in out or 2) initialize S inside the procedure before doing 
anything with it (for example with an aggregate). SPARK appears to 
behave as if the entire string is uninitialized upon entry into the 
procedure... even the attributes. I'm having trouble finding information 
about this in my SPARK references also.

Peter

Re: Question about out parameters of unconstrained array type.

[Dmitry A. Kazakov]

On Sat, 25 Feb 2012 10:19:02 -0500, Peter C. Chapin wrote:

> Consider a simple procedure
> 
> procedure P(S : out String) is
> begin
>     ...
> end P;
> 
> Despite the fact that S behaves as if it is uninitialized my Ada 
> compiler (GNAT GPL 2011) allows me to read certain attributes.

Uninitialized /= not constructed

> Is it well defined?

Yes, because the actual of S has all attributes set. Compare it with this:

declare
   S : String (1..20); -- S is uninitialized, but constructed
begin
   if S'Length > 0 then -- This is OK
 
> Where does it say so?

I don't know, but there is common sense: Ada's design is sane enough not to
allow existence of indefinite objects.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Question about out parameters of unconstrained array type.

[Phil Thornley]

In article <I8qdndMrnK9zZtXS4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...
> 
> Consider a simple procedure
> 
> procedure P(S : out String) is
> begin
>     ...
> end P;
> 
> Despite the fact that S behaves as if it is uninitialized my Ada 
> compiler (GNAT GPL 2011) allows me to read certain attributes. For 
> example if the body is
> 
>    for I in 1 .. S'Length loop ...
> 
> (never mind that I'm making a bad assumption about S'First being 1) I 
> don't see any warning about reading an uninitialized value when I do 
> S'Length. This is fine but I'm having trouble locating in the LRM where 
> this behavior is explicitly said to be well defined. Is it well defined? 
> Where does it say so?
> 
> The reason I'm asking is because SPARK does *not* like the usage of 
> S'Length in my example above.

I think that you may be misinterpreting the SPARK error message:

  15        for I in 1 .. S'Length loop
                     ^
***        Syntax Error      : reserved word "IN" cannot be followed by
           INTEGER_NUMBER here.

The error here is that the loop index has an anonymous subtype.

If you change this to:

   for I in Integer range 1 .. S'Length loop

there is no syntax or semantic error reported. (You will get the usual 
flow error if you assign individual values of the string in the loop, 
but that's another problem all together.)

In fact the LRM states that this usage is permitted. See Section 4.1:
"... the name of an unconstrained array object (formal parameter) shall 
only appear in the following contexts:
   1  as the prefix of an attribute reference;
   2  ..."

Cheers,

Phil

Re: Question about out parameters of unconstrained array type.

[Simon Wright]

Phil Thornley <phil.jpthornley@gmail.com> writes:

> If you change this to:
>
>    for I in Integer range 1 .. S'Length loop
>
> there is no syntax or semantic error reported.

There should be, shouldn't there?  replace 1 by S'First.

Would SPARK accept

   for I in S'Range loop

?

Re: Question about out parameters of unconstrained array type.

[Phil Thornley]

In article <m2obsmk7hl.fsf@pushface.org>, simon@pushface.org says...
> 
> Phil Thornley <phil.jpthornley@gmail.com> writes:
> 
> > If you change this to:
> >
> >    for I in Integer range 1 .. S'Length loop
> >
> > there is no syntax or semantic error reported.
> 
> There should be, shouldn't there?  replace 1 by S'First.

That makes no difference - in SPARK all Strings are required to have an 
index starting at 1.

> 
> Would SPARK accept
> 
>    for I in S'Range loop
> 
> ?

No - the subtype of the loop index is still regarded as anonymous.

Cheers,

Phil

Re: Question about out parameters of unconstrained array type.

[Alexander Senier]

On Sat, 25 Feb 2012 18:20:42 -0000
Phil Thornley <phil.jpthornley@gmail.com> wrote:

> there is no syntax or semantic error reported. (You will get the usual 
> flow error if you assign individual values of the string in the loop, 
> but that's another problem all together.)
> 
> In fact the LRM states that this usage is permitted. See Section 4.1:
> "... the name of an unconstrained array object (formal parameter) shall 
> only appear in the following contexts:
>    1  as the prefix of an attribute reference;
>    2  ..."

As you say, using attributes of out parameters of an unconstrained array type
is no problem when used inside a loop iteration scheme in SPARK. However, it
seems to be when using the attribute elsewhere:

  1 package P is
  2    procedure Init (A : out String);
  3    --# derives A from ;
  4 end P;

  1 package body P is
  2    procedure Init (A : out String) is
  3    begin
  4       for I in Positive range A'First .. A'Last
  5       loop
  6          if A'Length > 42
  7          then
  8             A (I) := 'x';
  9          end if;
 10       end loop;
 11    end Init;
 12 end P;

The example yields the two expected flow errors you mention (line 8 and 11).
However, the use of A'Length in line 6 also lead to an (unexpected) flow error
(same for 'First and 'Last):

p.adb:6:13: Flow Error  20 - Expression contains reference(s) to variable A
which has an undefined value.

Regards
Alex

Re: Question about out parameters of unconstrained array type.

[Peter C. Chapin]

On 2012-02-25 13:20, Phil Thornley wrote:

> I think that you may be misinterpreting the SPARK error message:
>
>    15        for I in 1 .. S'Length loop
>                       ^
> ***        Syntax Error      : reserved word "IN" cannot be followed by
>             INTEGER_NUMBER here.
>
> The error here is that the loop index has an anonymous subtype.

I'm sorry to have distracted you with my silly error. That's what 
happens when one just types some code into a posting off the top of 
one's head.

My real code is more like this:

procedure Get_Event
    (Date        : in  Dates.Date;
     Description : out String;
     Status      : out Status_Type)
--# global in Event_Array;
--# derives Description from Event_Array, Date &
--#         Status      from Event_Array, Date;
is
    I : Event_Index_Type;
begin
    Status      := No_Event;
    Description := (others => ' ');   -- NOTE HERE [1]

    I := Event_Index_Type'First;
    loop
       -- Is this item in the event array the one we are looking for?
       if Event_Array(I).Date = Date then
          -- NOTE HERE [2]
          if Description'Length < Event_Array(I).Description_Size then
             Status := Description_Too_Long;
          else
             -- Copy Event_Array(I).Description_Text into Description
             Status := Success;
          end if;
          exit;
       end if;

       -- If not, then advance to the next item.
       exit when I = Event_Index_Type'Last;
       I := I + 1;
    end loop;
end Get_Event;

Without the initialization at [1] the use of Description'Length at [2] 
produces the error Alexander mentions: "Expression contains reference(s) 
to variable Description which has an undefined value."

However with the initialization at [1] this error goes away. Thus it 
appears that SPARK requires that the initial value be defined before it 
will let you use the attributes.

Peter

Re: Question about out parameters of unconstrained array type.

[Phil Thornley]

In article <4NedncPWdPN9GtTS4p2dnAA@giganews.com>, PChapin@vtc.vsc.edu 
says...

[...]
> I'm sorry to have distracted you with my silly error. That's what 
> happens when one just types some code into a posting off the top of 
> one's head.
> 
> My real code is more like this:
> 
> procedure Get_Event
>     (Date        : in  Dates.Date;
>      Description : out String;
>      Status      : out Status_Type)
> --# global in Event_Array;
> --# derives Description from Event_Array, Date &
> --#         Status      from Event_Array, Date;
> is
>     I : Event_Index_Type;
> begin
>     Status      := No_Event;
>     Description := (others => ' ');   -- NOTE HERE [1]
> 
>     I := Event_Index_Type'First;
>     loop
>        -- Is this item in the event array the one we are looking for?
>        if Event_Array(I).Date = Date then
>           -- NOTE HERE [2]
>           if Description'Length < Event_Array(I).Description_Size then
>              Status := Description_Too_Long;
>           else
>              -- Copy Event_Array(I).Description_Text into Description
>              Status := Success;
>           end if;
>           exit;
>        end if;
> 
>        -- If not, then advance to the next item.
>        exit when I = Event_Index_Type'Last;
>        I := I + 1;
>     end loop;
> end Get_Event;
> 
> Without the initialization at [1] the use of Description'Length at [2] 
> produces the error Alexander mentions: "Expression contains reference(s) 
> to variable Description which has an undefined value."
> 
> However with the initialization at [1] this error goes away. Thus it 
> appears that SPARK requires that the initial value be defined before it 
> will let you use the attributes.

So it appears that the treatment of Description'Length is different when 
it appears in the range constraint of a loop statement to anywhere else. 
(This isn't completely surprising as the loop constraint gets special 
treatment for other purposes.) It might be worth raising this with the 
SPARK team - if only to try to get an authorative statement of what the 
position actually is.

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:

package P is
   procedure Init (A : out String;
                   A_Last : in Integer);
   --# derives A from A_Last;
   --# pre A'Length = A_Last;
end P;

package body P is
   procedure Init (A : out String;
                   A_Last : in Integer) is
   begin
      for I in Positive range A'First .. A'Last
      loop
         if A_Last > 42
         then
            A (I) := 'x';
         end if;
      end loop;
   end Init;
end P;

(Note that it is valid to reference A'Length in the precondition.

Cheers,

Phil

Re: Question about out parameters of unconstrained array type.

[Alexander Senier]

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

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. For now, I would prefer accepting the resulting flow
error for several reasons:

* Default initialization may hide subsequent flow errors that would
  been spotted by the flow analysis otherwise (the coarse grained treatment
  of array makes that less important, though)

* As Phil said, (additional) default initialization may impose a significant
  performance overhead

* Passing in the upper bound of the array as a parameter IMHO makes the code
  less intuitive and readable than it could be - just to silence the flow
  analysis ;-(

Regards
Alex

Re: Question about out parameters of unconstrained array type.

[Phil Thornley]

In article <20120226132532.7fb8ec1b@t60>, mail@senier.net says...
> 
> 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...
> 
> 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. For now, I would prefer accepting the resulting flow
> error for several reasons:
> 
> * Default initialization may hide subsequent flow errors that would
>   been spotted by the flow analysis otherwise (the coarse grained treatment
>   of array makes that less important, though)
> 
> * As Phil said, (additional) default initialization may impose a significant
>   performance overhead
> 
> * Passing in the upper bound of the array as a parameter IMHO makes the code
>   less intuitive and readable than it could be - just to silence the flow
>   analysis ;-(
> 

I fully agree with all of this.

It looks as if the statement in Section 4.1 of the LRM:
"... the name of an unconstrained array object (formal parameter) shall 
only appear in the following contexts:
   1  as the prefix of an attribute reference;
   2  ..."
needs some qualification.

(I can't find anything in the release notes to suggest that this is 
already seem as a deficiency in the language or tool.)

Cheers,

Phil

Re: Question about out parameters of unconstrained array type.

[Niklas Holsti]

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

Re: Question about out parameters of unconstrained array type.

[Peter C. Chapin]

On 2012-02-26 04:14, Phil Thornley wrote:

> Note that it is valid to reference A'Length in the precondition.

Thanks.

The initialization doesn't bother me too much. I have to write something 
useful into every element of the out parameter anyway. In this 
particular case the "real" data might not be as long as the given array 
so just blanket initializing the whole array right up front is satisfactory.

I do see, however, how this issue might be seen as an unnecessary 
limitation of SPARK.

Peter

Re: Question about out parameters of unconstrained array type.

[Jeffrey Carter]

On 02/26/2012 05:25 AM, Alexander Senier wrote:
>
> 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...

ARM-83 6.2 (Formal Parameter Modes) has:

out      The  formal  parameter is a variable  and permits updating of the
           value of the associated actual parameter.

           The value  of  a scalar parameter that is not updated by the call
           is undefined  upon return;  the  same  holds for the  value  of a
           scalar subcomponent,  other  than a  discriminant.   Reading  the
           bounds and discriminants  of the  formal  parameter  and  of  its
           subcomponents is allowed,  but no other reading.

This explicitly allows reading the bounds of a mode-out formal array parameter 
(note that, in Ada 83, you could not read the value of a mode-out parameter, 
even after assigning to it). ARM-95 and later are more formal, and lack such a 
simple statement about reading attributes.

Whether 'Length counts as "bounds" is another matter; 'Length is 'Pos ('Last) - 
'Pos ('First) + 1, so I'd think it does.

-- 
Jeff Carter
"If you think you got a nasty taunting this time,
you ain't heard nothing yet!"
Monty Python and the Holy Grail
23

--- Posted via news://freenews.netfront.net/ - Complaints to news@netfront.net ---

Re: Question about out parameters of unconstrained array type.

[Mark Lorenzen]

On 25 Feb., 23:44, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> > Would SPARK accept
>
> >    for I in S'Range loop
>
> > ?
>
> No - the subtype of the loop index is still regarded as anonymous.

Phil

Do you know the rationale for this? Why can't the examiner just
generate hypotheses like

loop__1__i <= s__index__subtype__1__last
loop__1__i >= s__index__subtype__1__first

and then generate appropriate hypotheses regarding
s__index__subtype__1__last and s__index__subtype__1__first?

Regards

Mark L

Re: Question about out parameters of unconstrained array type.

[Phil Thornley]

In article <4e2c786f-8485-436f-b9c5-c8c19cf00805
@q12g2000yqg.googlegroups.com>, mark.lorenzen@gmail.com says...
> 
> On 25 Feb., 23:44, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> > > Would SPARK accept
> >
> > > ￜ ￜfor I in S'Range loop
> >
> > > ?
> >
> > No - the subtype of the loop index is still regarded as anonymous.
> 
> Phil
> 
> Do you know the rationale for this? Why can't the examiner just
> generate hypotheses like
> 
> loop__1__i <= s__index__subtype__1__last
> loop__1__i >= s__index__subtype__1__first
> 
> and then generate appropriate hypotheses regarding
> s__index__subtype__1__last and s__index__subtype__1__first?

Mark,

I don't know of any specific reasoning, but the rule that an explicit 
subtype mark must be given is a fundamental rule in the grammar, so I 
guess there would have to be a very substantial gain from modifying it 
before such a change was considered.

Cheers,

Phil