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