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

Differences between 1.6 and version 1.7
Log of other versions for file ai12s/ai12-0366-1.txt

--- ai12s/ai12-0366-1.txt	2020/05/10 23:03:36	1.6
+++ ai12s/ai12-0366-1.txt	2020/05/16 04:39:24	1.7
@@ -1,4 +1,4 @@
-!standard A.5.6(0)                                   20-04-30  AI12-0366-1/03
+!standard A.5.6(0)                                   20-05-05  AI12-0366-1/04
 !standard A.5.7(0)
 !class Amendment 20-02-10
 !status Amendment 1-2012 20-04-30
@@ -1347,5 +1347,426 @@
 denominator by the same value). Only for calculating Numerator and 
 Denominator it must be computed. Thus I favor a complete Post. And 
 implementing 0/10**10000 as 0/1 won't be costly.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, May 4, 2020  9:21 PM
+
+In working on putting this AI into the draft Standard (remember that we 
+approved it during the meeting last Wednesday), I noticed a few additional
+issues. None of them are particularly problematical; the first might need a
+bit of input from some SPARK people (there being two possible fixes and I 
+don't know if there is a preference for one of them vis-a-vis SPARK).
+
+---
+
+[1] We have:
+   function In_Range (Arg, Low, High : Big_Integer) return Boolean is
+     (Low <= Arg and Arg <= High);
+
+The expression here will raise Program_Error if any of the arguments are 
+invalid ("<=" requires valid arguments). However, this predicate function is
+used in preconditions (specifically, in From_Big_Integer and To_Integer) where
+it is expected to return False for values of Arg that are out of range, 
+including those that are invalid.
+
+It's also weird that we're not making explicit the implicit requirement that 
+Low and High are valid. (Integer ranges are always valid in Ada, it seems 
+appropriate to make the same requirement here.) This isn't *wrong* per-se, as 
+the expression itself would raise Program_Error in the same way, but it likely
+to be confusing to a reader.
+
+So I recommend using the following instead:
+
+   function In_Range (Arg : Big_Integer;
+                      Low, High : Valid_Big_Integer) return Boolean is
+     (Is_Valid (Arg) and then Low <= Arg and then Arg <= High);
+
+Note that I had to change "and" to "and then" so that we don't call the 
+relational operators if Arg is not valid. I could have left the second "and" 
+with some additional parens, but that just seemed to make it harder to read.
+
+An alternative would be to make From_Big_Integer, To_Integer, and In_Range 
+only allow valid values (that is, only take Valid_Big_Integer arguments), but 
+that's a substantially bigger change from what was approved, and it makes 
+In_Range slightly more fragile. It also would change the exception raised from 
+Constraint_Error to Program_Error for To_Integer and From_Big_Integer. [I have 
+no idea which makes more sense for SPARK, and I don't think the exception 
+raised is important in these cases.]
+
+[2] The following also requires the arguments to be valid; for Den that's 
+hidden in the precondition and it isn't checked at all for Num:
+
+   function "/" (Num, Den : Big_Integers.Big_Integer) return Valid_Big_Real;
+     with Pre =>  Den /= 0
+                  or else raise Constraint_Error;
+
+So I changed this to:
+
+   function "/" (Num, Den : Big_Integers.Valid_Big_Integer) return Valid_Big_Real;
+     with Pre =>  Den /= 0
+                  or else raise Constraint_Error;
+
+[3] There was a lot of blank lines added and subtracted. The spacing should be 
+similar to that of Standard (see A.1) and System.Storage_Elements (see 13.7.1).
+I adjusted the spacing in order to stay consistent with the layout of numeric 
+types in the Standard.
+
+[4] Put_Image needs mode "in" for the second parameter; procedures always give 
+the mode in the Standard (functions do not, since it almost always is "in").
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, May 5, 2020  7:50 AM
+
+> [1] We have:
+>   function In_Range (Arg, Low, High : Big_Integer) return Boolean is
+>     (Low <= Arg and Arg <= High);
+> 
+> The expression here will raise Program_Error if any of the arguments 
+> are invalid ("<=" requires valid arguments). However, this predicate 
+> function is used in preconditions (specifically, in From_Big_Integer 
+> and To_Integer) where it is expected to return False for values of Arg 
+> that are out of range, including those that are invalid.
+
+Actually, it is fine if it raises the "right" exception, namely Program_Error.
+This is not like something used in a predicate aspect, where we need to be 
+sure it returns True or False, and never raises an exception.
+
+Did you get all of Arnaud's last-minute fixes here?  I think we agreed to 
+change almost everything to Valid_Big_Integer.
+
+> It's also weird that we're not making explicit the implicit 
+> requirement that Low and High are valid. (Integer ranges are always 
+> valid in Ada, it seems appropriate to make the same requirement here.) 
+> This isn't *wrong* per-se, as the expression itself would raise 
+> Program_Error in the same way, but it likely to be confusing to a reader.
+
+This was my presuming that because there were validity checks already on all 
+of the operators, we didn't have to repeat them.  I could go either way.
+ 
+> So I recommend using the following instead:
+> 
+>   function In_Range (Arg : Big_Integer;
+>                      Low, High : Valid_Big_Integer) return Boolean is
+>     (Is_Valid (Arg) and then Low <= Arg and then Arg <= High);
+
+Or just use Arg: Valid_Big_Integer.  Having to use Is_Valid explicitly seems 
+to defeat the purpose somewhat of having the predicate.  I don't see a need 
+for In_Range to return False on invalid inputs.  In fact, I suspect that 
+makes it harder for SPARK.
+ 
+> Note that I had to change "and" to "and then" so that we don't call 
+> the relational operators if Arg is not valid. I could have left the 
+> second "and" with some additional parens, but that just seemed to make 
+> it harder to read.
+> 
+> An alternative would be to make From_Big_Integer, To_Integer, and 
+> In_Range only allow valid values (that is, only take Valid_Big_Integer 
+> arguments), but that's a substantially bigger change from what was 
+> approved, and it makes In_Range slightly more fragile.
+
+I think that is preferable.
+
+> It also would change the exception raised from Constraint_Error to 
+> Program_Error for To_Integer and From_Big_Integer. [I have no idea 
+> which makes more sense for SPARK, and I don't think the exception 
+> raised is important in these cases.]
+
+I presume you mean To_Big_Integer, and in that case we want Valid_Big_Integer 
+as the result subtype.
+
+I believe we want Program_Error for any case of an invalid Big_Integer, and 
+Constraint_Error only if we have a valid big integer which is outside a pair
+of valid big-integer bounds.
+
+So I would sprinkle Valid_Big_Integer liberally, and not put any explicit 
+"Is_Valid" into Is_Range.  My goal was that the *only* language-defined 
+function that should be allowed to take an invalid big integer should be 
+Is_Valid.  Everything else should raise Program_Error.
+
+> [2] The following also requires the arguments to be valid; for Den 
+> that's hidden in the precondition and it isn't checked at all for Num:
+> 
+>   function "/" (Num, Den : Big_Integers.Big_Integer) return Valid_Big_Real;
+>     with Pre =>  Den /= 0
+>                  or else raise Constraint_Error;
+> 
+> So I changed this to:
+> 
+>   function "/" (Num, Den : Big_Integers.Valid_Big_Integer) return 
+>      Valid_Big_Real;
+>     with Pre =>  Den /= 0
+>                  or else raise Constraint_Error;
+
+Agreed.
+
+> 
+> [3] There was a lot of blank lines added and subtracted. The spacing 
+> should be similar to that of Standard (see A.1) and 
+> System.Storage_Elements (see 13.7.1).
+> I adjusted the spacing in order to stay consistent with the layout of 
+> numeric types in the Standard.
+
+Ok.
+
+> 
+> [4] Put_Image needs mode "in" for the second parameter; procedures 
+> always give the mode in the Standard (functions do not, since it 
+> almost always is "in").
+
+Ok.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, May 5, 2020  2:35 PM
+
+>> [1] We have:
+>>   function In_Range (Arg, Low, High : Big_Integer) return Boolean is
+>>     (Low <= Arg and Arg <= High);
+>> 
+>> The expression here will raise Program_Error if any of the arguments are
+>> invalid ("<=" requires valid arguments). However, this predicate function 
+>> is used in preconditions (specifically, in From_Big_Integer and To_Integer)
+>> where it is expected to return False for values of Arg that are out of 
+>> range, including those that are invalid.
+
+>Actually, it is fine if it raises the "right" exception, namely Program_Error.
+>This is not like something used in a predicate aspect, where we need to be 
+>sure it returns True or False, and never raises an exception.
+
+In_Range is similar to a membership operation, and we had a lot of issues 
+because we didn't want predicates to raise exceptions in memberships. It seems
+to me that the same applies to this operation. You're probably right that it 
+doesn't matter in a precondition, but having to protect it in a normal if 
+statement seems like extra work:
+
+      if In_Range (...) then -- Shouldn't raise any exception assuming the range is OK.
+
+I don't feel very strongly about this, but my experience has been that any 
+time you have a function returning a Boolean that fails somehow rather than 
+returning True or False, you regret it. I just had a case like this in the 
+Janus/Ada code: I changed Is_Ptr (Not_A_Type) to cause an internal error, but
+that caused so many issues (especially with error handling and other 
+preconditions) that I changed it back.
+
+> Did you get all of Arnaud's last-minute fixes here?  I think we agreed to change 
+> almost everything to Valid_Big_Integer.
+
+I think so. Those mostly changed the result of To_Big_Integer, no parameters 
+were involved.
+
+>> It's also weird that we're not making explicit the implicit requirement that
+>> Low and High are valid. (Integer ranges are always valid in Ada, it seems 
+>> appropriate to make the same requirement here.) This isn't *wrong* per-se,
+>> as the expression itself would raise Program_Error in the same way, but it
+>> likely to be confusing to a reader.
+
+>This was my presuming that because there were validity checks already on all 
+>of the operators, we didn't have to repeat them.  I could go either way.
+
+I think its confusing to not include the extra 6 characters to say that the 
+value needs to be valid. Otherwise, one wonders why this function is different
+from the others.
+
+> So I recommend using the following instead:
+> 
+>   function In_Range (Arg : Big_Integer;
+>                      Low, High : Valid_Big_Integer) return Boolean is
+>     (Is_Valid (Arg) and then Low <= Arg and then Arg <= High);
+
+>Or just use Arg: Valid_Big_Integer.  Having to use Is_Valid explicitly seems 
+>to defeat the purpose somewhat of having the predicate.  I don't see a need 
+>for In_Range to return False on invalid inputs.  In fact, I suspect that 
+>makes it harder for SPARK.
+
+The last here was my question. As noted above, it's better if it returns False 
+on invalid inputs, since this is like a membership test and those should never 
+raise exceptions. But I don't want to make something unnecessarily hard for 
+SPARK.
+
+>> It also would change the exception raised from
+>> Constraint_Error to Program_Error for To_Integer and From_Big_Integer. [I 
+>> have no idea which makes more sense for SPARK, and I don't think the exception 
+>> raised is important in these cases.]
+
+>I presume you mean To_Big_Integer, and in that case we want Valid_Big_Integer 
+>as the result subtype.
+
+No, I mean From_Big_Integer, which takes a Big_Integer (not Valid_Big_Integer) 
+parameter. 
+
+>I believe we want Program_Error for any case of an invalid Big_Integer, and 
+>Constraint_Error only if we have a valid big integer which is outside a pair 
+>of valid big-integer bounds.
+
+That's fine, we could change To_Integer and the two From_Big_Integers to take 
+Valid_Big_Integer. That would be more consistent. 
+
+>So I would sprinkle Valid_Big_Integer liberally, and not put any explicit 
+>"Is_Valid" into Is_Range.  My goal was that the *only* language-defined 
+>function that should be allowed to take an invalid big integer should be 
+>Is_Valid.  Everything else should raise Program_Error.
+
+Even a range membership test? That's unlike the work we did for predicates. 
+
+Note that
+    if A in Valid_Big_Integer then -- never raises an exception, even if A is invalid
+
+while you're suggesting that
+    in In_Range (A, 1, 10) then -- raises Program_Error if A is invalid
+
+Doesn't seem right to me.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, May 5, 2020  2:51 PM
+
+...
+>In_Range is similar to a membership operation, and we had a lot of issues 
+>because we didn't want predicates to raise exceptions in memberships. It 
+>seems to me that the same applies to this operation. You're probably right
+>that it doesn't matter in a precondition, but having to protect it in a 
+>normal if statement seems like extra work:
+>
+>    if In_Range (...) then -- Shouldn't raise any exception assuming the range is OK.
+>
+>I don't feel very strongly about this, but my experience has been that any 
+>time you have a function returning a Boolean that fails somehow rather than
+>returning True or False, you regret it. I just had a case like this in the 
+>Janus/Ada code: I changed Is_Ptr (Not_A_Type) to cause an internal error, 
+>but that caused so many issues (especially with error handling and other 
+>preconditions) that I changed it back.
+
+But there are three inputs to In_Range, and having to put Is_Valid on all of 
+them seems silly.  I would argue all of the inputs should simply be 
+Valid_Big_Integer, and not worry about it.  Even a "normal" integer membership 
+test can raise Program_Error in Ada, if the compiler can determine the operand 
+is uninitialized.  The only thing that is safe on an uninitialized scalar is 
+'Valid, and I would argue that Is_Valid should be the only function that 
+should be allowed to take an uninitialized Big_Integer.
+
+...
+>>This was my presuming that because there were validity checks already on all 
+>>of the operators, we didn't have to repeat them.  I could go either way.
+
+>I think its confusing to not include the extra 6 characters to say that the 
+>value needs to be valid. Otherwise, one wonders why this function is 
+>different from the others.
+
+Agreed.  Slather "Valid_" in front of all of the Big_Integer operands and 
+results.
+
+...
+>The last here was my question. As noted above, it's better if it returns 
+>False on invalid inputs, since this is like a membership test and those 
+>should never raise exceptions. But I don't want to make something 
+>unnecessarily hard for SPARK.
+
+Put "Valid_" everywhere, and don't allow any function to even be called if it 
+has an uninitialized Big_Integer.
+
+>>> It also would change the exception raised from
+>>> Constraint_Error to Program_Error for To_Integer and From_Big_Integer. [I have 
+>>> no idea which makes more sense for SPARK, and I don't think the exception 
+>>> raised is important in these cases.]
+
+>>I presume you mean To_Big_Integer, and in that case we want Valid_Big_Integer as 
+>>the result subtype.
+
+>No, I mean From_Big_Integer, which takes a Big_Integer (not Valid_Big_Integer) 
+>parameter.
+
+You wrote "To_Integer" and there is no such function.  I presume you meant 
+"To_Big_Integer" when you wrote "To_Integer".
+
+>>So I would sprinkle Valid_Big_Integer liberally, and not put any explicit 
+>>"Is_Valid" into Is_Range.  My goal was that the *only* language-defined 
+>>function that should be allowed to take an invalid big integer should be 
+>>Is_Valid.  Everything else should raise Program_Error.
+
+>Even a range membership test? That's unlike the work we did for predicates. 
+
+Be that as it may, it is a function, and it should require all operands to be 
+initialized before it is called.
+
+>Note that
+>    if A in Valid_Big_Integer then -- never raises an exception, even if A is invalid
+>
+>while you're suggesting that
+>    in In_Range (A, 1, 10) then -- raises Program_Error if A is invalid
+
+Yes, but there are three Big_Integer operands to In_Range.
+
+>Doesn't seem right to me.
+
+I don't see the problem.  As mentioned, a membership test like 
+"if X in 1..10 then ..." can raise Program_Error if X is uninitialized.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, May 5, 2020  2:57 PM
+
+The point is that it is not meaningful to ask if something is in a particular 
+range if it isn't initialized.
+
+On the other hand, asking first if something is initialized, and only *then* 
+asking if it is in a particular range makes sense.  And that is exactly what 
+it means by putting Valid_Big_Integer on all operands to In_Range.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, May 5, 2020  3:45 PM
+
+...
+>>I think its confusing to not include the extra 6 characters to say that the
+>>value needs to be valid. Otherwise, one wonders why this function is 
+>>different from the others.
+
+>Agreed.  Slather "Valid_" in front of all of the Big_Integer operands and 
+>results.
+
+OK by me. Will do.
+
+
+...
+>> No, I mean From_Big_Integer, which takes a Big_Integer (not 
+>>Valid_Big_Integer) parameter.
+
+>You wrote "To_Integer" and there is no such function.  I presume you meant 
+>"To_Big_Integer" when you wrote "To_Integer"
+
+Umm, there is in AI12-0366-1 -- it's directly below In_Range.
+
+  function To_Integer (Arg : Big_Integer) return Integer ...
+...
+>>Note that
+>>    if A in Valid_Big_Integer then -- never raises an exception, even if A is invalid
+>>
+>>while you're suggesting that
+>>    in In_Range (A, 1, 10) then -- raises Program_Error if A is invalid
+
+>Yes, but there are three Big_Integer operands to In_Range.
+
+The range has to be valid (as with all ranges), but not the argument. 
+
+>>Doesn't seem right to me.
+>
+>I don't see the problem.  As mentioned, a membership test like "if X in 1..10 
+>then ..." can raise Program_Error if X is uninitialized.
+
+It would be a rather unfriendly compiler (and expensive at runtime) to do that 
+for an Integer, since every value of Integer'Base is valid. The permission 
+exists for signalling NaNs and bad enumeration representations, neither of 
+which are very likely to occur in practice.
+
+Anyway, I don't care enough to argue, there are worse problems with this spec 
+foisted on us by SPARK.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent