--- ai12s/ai12-0005-1.txt 2020/09/04 03:47:34 1.38 +++ ai12s/ai12-0005-1.txt 2020/09/11 22:20:27 1.39 @@ -2278,7 +2278,181 @@ *************************************************************** -Editor's note (September 2, 2020): All of the items above this +!topic When is a big real valid? +!reference Ada 202x RM A.5.7(4/5) Draft 25 +!from Christoph Grein 20-06-04 +!discussion + +There is no statement about when a big real is valid. (23/5) says "The other +functions have their usual mathematical meanings." I do not know the usual +mathematical meaning of validity of a number. + +[BTW: Is there a general definition what a number is? Think of John Horton +Conway's definition of numbers starting with the empty set.] + +I can guess that a big real is valid if both numerator ad denominator are +valid big integers and the denominator is not 0. Is guessing another step +in the direction of Ada++? ;-) + +*************************************************************** + +!topic Big Integers typo +!reference Ada 202x RM A.5.6(9/5) Draft 25 +!from Christoph Grein 20-06-05 +!discussion + +subtype Big_Natural is Big_Integer + with Dynamic_Predicate => (if Is_Valid (Big_Natural) then Big_Natural [=>]{>=} 0), + Predicate_Failure => (raise Constraint_Error); + +BTW: As for big reals, it's not defined when a big integer is valid. + +Is validity defined implicitly via the operations with a result of +Valid_Big_Integer? I.e. a big integer is only valid if it is constructed +with any of these constructors? + +*************************************************************** + +From: Randy Brukardt +Sent: Wednesday, June 10, 2020 6:59 PM + +> subtype Big_Natural is Big_Integer +> with Dynamic_Predicate => (if Is_Valid (Big_Natural) then +Big_Natural [=>]{>=} 0), +> Predicate_Failure => (raise Constraint_Error); + +I fixed the typo in the working RM draft. + +> BTW: As for big reals, it's not defined when a big integer is valid. +> +> Is validity defined implicitly via the operations with a result of +>Valid_Big_Integer? I.e. a big integer is only valid if it is +>constructed with any of these constructors? + +The validity of a default-initialized Big_Integer or Big_Real is intentionally +left undefined. Some SPARK people said they needed it that way to use their +existing uninitialized object analysis. + +Honestly, why that is necessary escapes me. The original Big_Integer and +Big_Real definitions had a + Default_Initial_Condition => not Is_Valid (Big_Integer); which neatly +defines the validity for fully dynamic (that is, Ada) implementations. And +an implementation with static checks for uninitialized objects could ignore +that specification (since Is_Valid is already defined as intrinsic so that an +implementation could replace it completely with static checks). + +Anyway, given the need for compromise it's left undefined. + +*************************************************************** + +Summary of private discussion between Randy Brukardt, Steve Baird, and Tucker +Taft: + +Steve: For Big_Integers, we have an AARM note + This means that the elaboration of + Default_Initialized_Object : Valid_Big_Integer; + is required to propagate Program_Error. + +There is an analogous note for Big_Reals. + +What does that follow from? + +Tucker: The current situation is closely tied to what works for SPARK in +trying to map these directly to "mathematical" integers/rationals, so we need +to be sure we don't end up breaking that mapping. + +One of the goals was to catch use of uninitialized variables. If Is_Valid is +true by default, then you have to define what is the default value of a +Big_Real. I don't think we wanted to do that. So yes, Is_Valid is presumably +False by default, though there is no language-provided way to create an +uninitialized value except by declaring and not initializing a variable, so I +don't think you have to define what makes a Big_Real valid, other than being +initialized. + +Steve: For static analysis purposes, all that is really required is that a +default initialized big number (integer or real) is not known to be valid. It +doesn't have to be known to not be valid. + +So it might be ok to leave things as is (i.e., Is_Valid is unspecified after +default initialization), but then we ought to fix those AARM notes I mentioned +that state otherwise. + +Randy: At a minimum, something like "the result Is_Valid on a +default-initialized object of type Big_Real is unspecified" would seem to be +necessary. I suppose we could justify *that* as an AARM note (saying +something is unspecified doesn't really require being said explicitly!) + +Tucker: So we might change the current AARM note to say: + + The result of Is_Valid on a default-initialized object of type Big_Real is + unspecified, analogous to the value of a Valid attribute_reference applied + to a default-initialized object of a real type (see 13.9.2). The + language-provided functions in the Big_Reals package only return values for + which Is_Valid is certain to be True. + +*************************************************************** + +!topic Any two actions of the same logical thread of control[;] are sequential,... +!reference Ada 202x AARM9.10(13.a/5) +!from Christoph Grein 20-08-29 + +*************************************************************** + +From: Pascal Pignard +Sent: Wednesday, September 2, 2020 11:01 AM + +Here is one typo: a space is missing before "Declaring...": + +6.4.1 Parameter Associations + +19.k/5 {AI12-0074-1} {AI12-0159-1} {AI12-0377-1} {AI12-0378-1} + Corrigendum: Added rules to ensure that the value passed into an + out parameter for scalar types is well-defined in the case of a + view conversion. The new rules can be incompatible. For a view + conversion to an unrelated type with the Default_Value aspect + specified, the aspect is new in Ada 2012 so it should be unlikely + to occur in existing code. Declaring and passing a temporary rather + than a view conversion will eliminate the problem. + +*************************************************************** + +!topic function "@key{xor}" (Left, Right : Set) return Set + +!reference Ada 202x RM A.18.8(36/2) +!from Christoph Grein 07-09-29 +!discussion HTML version - Text within the string quotes is wrong, should be as in Ada 2012 TC1: +"<b>xor</b>" +(Must have been introduced with all these Pre and Post.) + +*************************************************************** + +From: Randy Brukardt +Sent: Wednesday, September 9, 2020 2:47 PM + +> (Must have been introduced with all these Pre and Post.) + +Nope. I noticed some "missing" indexing and put in the appropriate commands. +When I was almost done with Draft 26, I happened to notice that the index +entries were @key{xor}. The bolding command doesn't get interpreted in the +index commands; the commands had been left out on purpose. I removed the +indexing, but figured no one would notice errors in the index so I didn't +regenerate the draft (which would have required redoing several hours of +work) - it certainly would have been fixed the next time. + +Unfortunately, the failure also appears in the body of the RM. Had I noticed +that, I would have started over generating the draft (and spent quite a bit +of time swearing loudly :-). + +Anyway, it was fixed before the draft was even fully posted. It certainly +will be fixed next time. + +P.S. You're already the second person to complain, and I doubt that you will +be the last. It appears in all of the operators of A.18.8 and A.18.9, not just +the one mentioned. (Except one, which was a bug-within-the-bug.) + +*************************************************************** + +Editor's note (September 9, 2020): All of the items above this marker have been included in the working version of the AARM. ****************************************************************

Questions? Ask the ACAA Technical Agent