CVS difference for ai12s/ai12-0366-1.txt
--- 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