* Question about out parameters of unconstrained array type.
@ 2012-02-25 15:19 Peter C. Chapin
2012-02-25 15:33 ` Dmitry A. Kazakov
2012-02-25 18:20 ` Phil Thornley
0 siblings, 2 replies; 15+ messages in thread
From: Peter C. Chapin @ 2012-02-25 15:19 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-25 15:19 Question about out parameters of unconstrained array type Peter C. Chapin
@ 2012-02-25 15:33 ` Dmitry A. Kazakov
2012-02-25 18:20 ` Phil Thornley
1 sibling, 0 replies; 15+ messages in thread
From: Dmitry A. Kazakov @ 2012-02-25 15:33 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-25 15:19 Question about out parameters of unconstrained array type Peter C. Chapin
2012-02-25 15:33 ` Dmitry A. Kazakov
@ 2012-02-25 18:20 ` Phil Thornley
2012-02-25 20:01 ` Simon Wright
` (2 more replies)
1 sibling, 3 replies; 15+ messages in thread
From: Phil Thornley @ 2012-02-25 18:20 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-25 18:20 ` Phil Thornley
@ 2012-02-25 20:01 ` Simon Wright
2012-02-25 22:44 ` Phil Thornley
2012-02-25 23:37 ` Alexander Senier
2012-02-26 1:16 ` Peter C. Chapin
2 siblings, 1 reply; 15+ messages in thread
From: Simon Wright @ 2012-02-25 20:01 UTC (permalink / raw)
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
?
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-25 20:01 ` Simon Wright
@ 2012-02-25 22:44 ` Phil Thornley
2012-02-27 13:48 ` Mark Lorenzen
0 siblings, 1 reply; 15+ messages in thread
From: Phil Thornley @ 2012-02-25 22:44 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-25 18:20 ` Phil Thornley
2012-02-25 20:01 ` Simon Wright
@ 2012-02-25 23:37 ` Alexander Senier
2012-02-26 1:16 ` Peter C. Chapin
2 siblings, 0 replies; 15+ messages in thread
From: Alexander Senier @ 2012-02-25 23:37 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-25 18:20 ` Phil Thornley
2012-02-25 20:01 ` Simon Wright
2012-02-25 23:37 ` Alexander Senier
@ 2012-02-26 1:16 ` Peter C. Chapin
2012-02-26 9:14 ` Phil Thornley
2 siblings, 1 reply; 15+ messages in thread
From: Peter C. Chapin @ 2012-02-26 1:16 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-26 1:16 ` Peter C. Chapin
@ 2012-02-26 9:14 ` Phil Thornley
2012-02-26 12:25 ` Alexander Senier
2012-02-26 15:29 ` Peter C. Chapin
0 siblings, 2 replies; 15+ messages in thread
From: Phil Thornley @ 2012-02-26 9:14 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-26 9:14 ` Phil Thornley
@ 2012-02-26 12:25 ` Alexander Senier
2012-02-26 13:20 ` Phil Thornley
` (2 more replies)
2012-02-26 15:29 ` Peter C. Chapin
1 sibling, 3 replies; 15+ messages in thread
From: Alexander Senier @ 2012-02-26 12:25 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-26 12:25 ` Alexander Senier
@ 2012-02-26 13:20 ` Phil Thornley
2012-02-26 14:25 ` Niklas Holsti
2012-02-26 17:32 ` Jeffrey Carter
2 siblings, 0 replies; 15+ messages in thread
From: Phil Thornley @ 2012-02-26 13:20 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-26 12:25 ` Alexander Senier
2012-02-26 13:20 ` Phil Thornley
@ 2012-02-26 14:25 ` Niklas Holsti
2012-02-26 17:32 ` Jeffrey Carter
2 siblings, 0 replies; 15+ messages in thread
From: Niklas Holsti @ 2012-02-26 14:25 UTC (permalink / raw)
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
. @ .
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-26 9:14 ` Phil Thornley
2012-02-26 12:25 ` Alexander Senier
@ 2012-02-26 15:29 ` Peter C. Chapin
1 sibling, 0 replies; 15+ messages in thread
From: Peter C. Chapin @ 2012-02-26 15:29 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-26 12:25 ` Alexander Senier
2012-02-26 13:20 ` Phil Thornley
2012-02-26 14:25 ` Niklas Holsti
@ 2012-02-26 17:32 ` Jeffrey Carter
2 siblings, 0 replies; 15+ messages in thread
From: Jeffrey Carter @ 2012-02-26 17:32 UTC (permalink / raw)
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 ---
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-25 22:44 ` Phil Thornley
@ 2012-02-27 13:48 ` Mark Lorenzen
2012-02-27 15:32 ` Phil Thornley
0 siblings, 1 reply; 15+ messages in thread
From: Mark Lorenzen @ 2012-02-27 13:48 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
* Re: Question about out parameters of unconstrained array type.
2012-02-27 13:48 ` Mark Lorenzen
@ 2012-02-27 15:32 ` Phil Thornley
0 siblings, 0 replies; 15+ messages in thread
From: Phil Thornley @ 2012-02-27 15:32 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 15+ messages in thread
end of thread, other threads:[~2012-02-27 15:32 UTC | newest]
Thread overview: 15+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-02-25 15:19 Question about out parameters of unconstrained array type Peter C. Chapin
2012-02-25 15:33 ` Dmitry A. Kazakov
2012-02-25 18:20 ` Phil Thornley
2012-02-25 20:01 ` Simon Wright
2012-02-25 22:44 ` Phil Thornley
2012-02-27 13:48 ` Mark Lorenzen
2012-02-27 15:32 ` Phil Thornley
2012-02-25 23:37 ` Alexander Senier
2012-02-26 1:16 ` Peter C. Chapin
2012-02-26 9:14 ` Phil Thornley
2012-02-26 12:25 ` Alexander Senier
2012-02-26 13:20 ` Phil Thornley
2012-02-26 14:25 ` Niklas Holsti
2012-02-26 17:32 ` Jeffrey Carter
2012-02-26 15:29 ` Peter C. Chapin
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox