--- ai12s/ai12-0366-1.txt 2020/05/05 02:23:19 1.5 +++ ai12s/ai12-0366-1.txt 2020/05/10 23:03:36 1.6 @@ -1,4 +1,4 @@ -!standard A.5.6(0) 20-05-04 AI12-0366-1/04 +!standard A.5.6(0) 20-04-30 AI12-0366-1/03 !standard A.5.7(0) !class Amendment 20-02-10 !status Amendment 1-2012 20-04-30 @@ -85,11 +85,10 @@ with Dyanmic_Predicate => (if Is_Valid (Big_Natural) then Big_Natural => 0), Predicate_Failure => raise Constraint_Error; - function In_Range (Arg : Big_Integer; - Low, High : Valid_Big_Integer) return Boolean is - (Is_Valid (Arg) and Low <= Arg and Arg <= High); + function In_Range (Arg, Low, High : Valid_Big_Integer) return Boolean is + (Low <= Arg and Arg <= High); - function To_Integer (Arg : Big_Integer) return Integer + function To_Integer (Arg : Valid_Big_Integer) return Integer with Pre => In_Range (Arg, Low => To_Big_Integer (Integer'First), High => To_Big_Integer (Integer'Last)) @@ -99,7 +98,7 @@ type Int is range <>; package Signed_Conversions is function To_Big_Integer (Arg : Int) return Valid_Big_Integer; - function From_Big_Integer (Arg : Big_Integer) return Int + function From_Big_Integer (Arg : Valid_Big_Integer) return Int with Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) @@ -110,7 +109,7 @@ type Int is mod <>; package Unsigned_Conversions is function To_Big_Integer (Arg : Int) return Valid_Big_Integer; - function From_Big_Integer (Arg : Big_Integer) return Int + function From_Big_Integer (Arg : Valid_Big_Integer) return Int with Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) @@ -205,18 +204,18 @@ function Numerator (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer - with Post => (if Arg = 0.0 then Numerator’Result = 0); + with Post => (if Arg = 0.0 then Numerator'Result = 0); AARM Reason: The postcondition of Numerator cannot be complete as it cannot mention Denominator. Since the postcondition of Denominator uses Numerator, - we would get an infinite mutual recursion of both postconditions are enabled. + we would get an infinite mutual recursion if both postconditions are enabled. The postcondition of Denominator serves as the postcondition for Numerator as well unless Arg = 0.0. function Denominator (Arg : Valid_Big_Real) return Big_Integers.Big_Positive with Post => - (if Arg = 0.0 then Denominator’Result = 1 + (if Arg = 0.0 then Denominator'Result = 1 else Big_Integers.Greatest_Common_Divisor (Numerator (Arg), Denominator'Result) = 1); function To_Big_Real (Arg : Big_Integers.Valid_Big_Integer) @@ -231,9 +230,8 @@ function ">" (L, R : Valid_Big_Real) return Boolean; function ">=" (L, R : Valid_Big_Real) return Boolean; - function In_Range (Arg : Big_Real; - Low, High : Valid_Big_Real) return Boolean is - (Is_Valid (Arg) and then Low <= Arg and then Arg <= High); + function In_Range (Arg, Low, High : Valid_Big_Real) return Boolean is + (Low <= Arg and Arg <= High); generic type Num is digits <>; @@ -342,7 +340,7 @@ @dinsc Dummy to force a conflict; the wording changes are in the conflict file. -!corrigendum A.5.5(0/5) +!corrigendum A.5.7(0/5) @dinsc Dummy to force a conflict; the wording changes are in the conflict file. @@ -1349,74 +1347,5 @@ 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"). ****************************************************************

Questions? Ask the ACAA Technical Agent