CVS difference for ai12s/ai12-0005-1.txt

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