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

Differences between 1.5 and version 1.6
Log of other versions for file 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