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

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

--- ai12s/ai12-0366-1.txt	2020/05/02 03:43:14	1.4
+++ ai12s/ai12-0366-1.txt	2020/05/05 02:23:19	1.5
@@ -1,4 +1,4 @@
-!standard A.5.6(0)                                   20-04-30  AI12-0366-1/03
+!standard A.5.6(0)                                   20-05-04  AI12-0366-1/04
 !standard A.5.7(0)
 !class Amendment 20-02-10
 !status Amendment 1-2012 20-04-30
@@ -57,6 +57,7 @@
 with Ada.Strings.Text_Buffers;
 package Ada.Numerics.Big_Numbers.Big_Integers
   with Preelaborate, Nonblocking, Global => null is
+
    type Big_Integer is private
      with Integer_Literal => From_String,
           Put_Image => Put_Image;
@@ -69,13 +70,9 @@
           Predicate_Failure => raise Program_Error;
 
    function "=" (L, R : Valid_Big_Integer) return Boolean;
-
    function "<" (L, R : Valid_Big_Integer) return Boolean;
-
    function "<=" (L, R : Valid_Big_Integer) return Boolean;
-
    function ">" (L, R : Valid_Big_Integer) return Boolean;
-
    function ">=" (L, R : Valid_Big_Integer) return Boolean;
 
    function To_Big_Integer (Arg : Integer) return Valid_Big_Integer;
@@ -88,8 +85,9 @@
      with Dyanmic_Predicate => (if Is_Valid (Big_Natural) then Big_Natural => 0),
           Predicate_Failure => raise Constraint_Error;
 
-   function In_Range (Arg, Low, High : Big_Integer) return Boolean is
-     (Low <= Arg and Arg <= High);
+   function In_Range (Arg : Big_Integer;
+                      Low, High : Valid_Big_Integer) return Boolean is
+     (Is_Valid (Arg) and Low <= Arg and Arg <= High);
 
    function To_Integer (Arg : Big_Integer) return Integer
      with Pre => In_Range (Arg,
@@ -100,29 +98,23 @@
    generic
       type Int is range <>;
    package Signed_Conversions is
-
-      function To_Big_Integer (Arg : Int) return Big_Integer;
-
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer;
       function From_Big_Integer (Arg : Big_Integer) return Int
         with Pre => In_Range (Arg,
                               Low  => To_Big_Integer (Int'First),
                               High => To_Big_Integer (Int'Last))
                      or else raise Constraint_Error;
-
    end Signed_Conversions;
 
    generic
       type Int is mod <>;
    package Unsigned_Conversions is
-
-      function To_Big_Integer (Arg : Int) return Big_Integer;
-
+      function To_Big_Integer (Arg : Int) return Valid_Big_Integer;
       function From_Big_Integer (Arg : Big_Integer) return Int
         with Pre => In_Range (Arg,
                               Low  => To_Big_Integer (Int'First),
                               High => To_Big_Integer (Int'Last))
                      or else raise Constraint_Error;
-
    end Unsigned_Conversions;
 
    function To_String (Arg   : Valid_Big_Integer;
@@ -134,31 +126,20 @@
 
    procedure Put_Image
      (Buffer : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
-      Arg    : Valid_Big_Integer);
+      Arg    : in Valid_Big_Integer);
 
    function "+" (L : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "-" (L : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
-
    function "**"
      (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer;
-
    function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer;
-
    function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer;
 
    function Greatest_Common_Divisor
@@ -166,9 +147,7 @@
      with Pre => (L /= 0 and R /= 0) or else raise Constraint_Error;
 
 private
-
    ... -- not specified by the language
-
 end Ada.Numerics.Big_Numbers.Big_Integers;
 
 Modify A.5.6(22/5):
@@ -185,24 +164,22 @@
   and writes the resulting value to the [stream using
   Wide_Wide_String'Write]{buffer using Text_Buffers.Put}.
 
-Modify A.5.6 (24/5-25/5):
+Modify A.5.6 (24/5-26/5) [reordering these paragraphs so the last paragraph
+is in the middle]:
 
   The type [Optional_]Big_Integer needs finalization (see 7.6).
 
-    Implementation Requirements
-
-  No storage associated with {a}[an Optional_]Big_Integer object shall be
-  lost upon assignment or scope exit.
-
-Modify A.5.6 (26/5) as follows, and move it to a Dynamic Semantics
-section, placed immediately after (24/5):
-
      {Dynamic Semantics}
 
   For purposes of determining whether predicate checks are performed as
   part of default initialization, the type [Optional_]Big_Integer [shall
   be]{is} considered to have a subcomponent that has a default_expression.
 
+    Implementation Requirements
+
+  No storage associated with {a}[an Optional_]Big_Integer object shall be
+  lost upon assignment or scope exit.
+
 Replace A.5.7 (2/5 to 19/5) with the following:
 
 with Ada.Numerics.Big_Numbers.Big_Integers; 
@@ -210,6 +187,7 @@
 with Ada.Strings.Text_Buffers;
 package Ada.Numerics.Big_Numbers.Big_Reals
   with Preelaborate, Nonblocking, Global => null is
+
    type Big_Real is private with
      Real_Literal => From_String,
      Put_Image    => Put_Image;
@@ -221,7 +199,7 @@
      with Dynamic_Predicate => Is_Valid (Valid_Big_Real),
           Predicate_Failure => raise Program_Error;
 
-   function "/" (Num, Den : Big_Integers.Big_Integer) return Valid_Big_Real;
+   function "/" (Num, Den : Big_Integers.Valid_Big_Integer) return Valid_Big_Real;
      with Pre =>  Den /= 0
                   or else raise Constraint_Error;
 
@@ -239,54 +217,44 @@
      (Arg : Valid_Big_Real) return Big_Integers.Big_Positive
      with Post =>
        (if Arg = 0.0 then Denominator’Result = 1 
-        else Greatest_Common_Divisor (Numerator (Arg), Denominator'Result) = 1);
+        else Big_Integers.Greatest_Common_Divisor (Numerator (Arg), Denominator'Result) = 1);
 
-   function To_Big_Real
-     (Arg : Big_Integers.Big_Integer)
-     return Valid_Big_Real is (Arg / 1);
+   function To_Big_Real (Arg : Big_Integers.Valid_Big_Integer)
+      return Valid_Big_Real is (Arg / 1);
 
    function To_Real (Arg : Integer) return Valid_Big_Real is
      (Big_Integers.To_Big_Integer (Arg) / 1);
 
    function "=" (L, R : Valid_Big_Real) return Boolean;
-
    function "<" (L, R : Valid_Big_Real) return Boolean;
-
    function "<=" (L, R : Valid_Big_Real) return Boolean;
-
    function ">" (L, R : Valid_Big_Real) return Boolean;
-
    function ">=" (L, R : Valid_Big_Real) return Boolean;
 
-   function In_Range (Arg, Low, High : Valid_Big_Real) return Boolean is
-     (Low <= Arg and then Arg <= High);
+   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);
 
    generic
       type Num is digits <>;
    package Float_Conversions is
-
       function To_Big_Real (Arg : Num) return Valid_Big_Real;
-
       function From_Big_Real (Arg : Valid_Big_Real) return Num
         with Pre => In_Range (Arg,
                               Low  => To_Big_Real (Num'First),
                               High => To_Big_Real (Num'Last))
                     or else raise Constraint_Error;
-
    end Float_Conversions;
 
    generic
       type Num is delta <>;
    package Fixed_Conversions is
-
       function To_Big_Real (Arg : Num) return Valid_Big_Real;
-
       function From_Big_Real (Arg : Valid_Big_Real) return Num
         with Pre => In_Range (Arg,
                               Low  => To_Big_Real (Num'First),
                               High => To_Big_Real (Num'Last))
                     or else raise Constraint_Error;
-
    end Fixed_Conversions;
 
    function To_String (Arg  : Valid_Big_Real;
@@ -305,34 +273,24 @@
 
    procedure Put_Image
      (Buffer : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
-      Arg    : Valid_Big_Real);
+      Arg    : in Valid_Big_Real);
 
    function "+" (L : Valid_Big_Real) return Valid_Big_Real;
-
    function "-" (L : Valid_Big_Real) return Valid_Big_Real;
-
    function "abs" (L : Valid_Big_Real) return Valid_Big_Real;
-
    function "+" (L, R : Valid_Big_Real) return Valid_Big_Real;
-
    function "-" (L, R : Valid_Big_Real) return Valid_Big_Real;
-
    function "*" (L, R : Valid_Big_Real) return Valid_Big_Real;
-
    function "/" (L, R : Valid_Big_Real) return Valid_Big_Real;
-
    function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real;
-
    function Min (L, R : Valid_Big_Real) return Valid_Big_Real;
-
    function Max (L, R : Valid_Big_Real) return Valid_Big_Real;
 
 private
    ...  --  not specified by the language
-
 end Ada.Numerics.Big_Numbers.Big_Reals;
 
-Modify 4.5.7 (20/5):
+Modify A.5.7 (20/5):
 
   To_String and From_String behave analogously to the Put and Get
   procedures defined in Text_IO.Float_IO (in particular, with respect to
@@ -342,26 +300,24 @@
   To_Quotient_String; Constraint_Error is propagated in error cases.
   Put_Image calls To_String,[ converts that String to a Wide_Wide_String
   using To_Wide_Wide_String,] and {writes} the resulting value to the
-  [stream] buffer using [Wide_Wide_String'Write]{Text_Buffers.Put}.
+  [stream] {buffer} using [Wide_Wide_String'Write]{Text_Buffers.Put}.
 
-Modify 4.5.7 (23/5 to 24/5):
+Modify A.5.7 (23/5 to 25/5): [reordering these paragraphs so the last paragraph
+is in the middle]:
 
   The type [Optional_]Big_Real needs finalization (see 7.6).
 
-     Implementation Requirements
-
-  No storage associated with {a}[an Optional_]Big_Real object shall be lost
-  upon assignment or scope exit.
-
-Modify 4.5.7 (25/5) as follows, and move it into a Dynamic Semantics
-section, placed immediately after (23/5):
-
     {Dynamic Semantics}
 
   For purposes of determining whether predicate checks are performed as
   part of default initialization, the type [Optional_]Big_Real [shall be]
   {is} considered to have a subcomponent that has a default_expression.
 
+     Implementation Requirements
+
+  No storage associated with {a}[an Optional_]Big_Real object shall be lost
+  upon assignment or scope exit.
+
 !discussion
 
 See the !proposal for most of the rationale.  We change the Global
@@ -381,15 +337,25 @@
 We changed the postcondition of Denominator to say something about the result
 when Arg = 0.0, and added a postcondition to Numerator to do the same.
 
+!corrigendum A.5.6(0/5)
+
+@dinsc
+Dummy to force a conflict; the wording changes are in the conflict file.
+
+!corrigendum A.5.5(0/5)
+
+@dinsc
+Dummy to force a conflict; the wording changes are in the conflict file.
+
 !ASIS
 
 Most likely, no ASIS support needed. (Unsure if the special semantics
-of Is_Valid are ).
+of Is_Valid requires any changes).
 
 !ACATS test
 
-ACATS B- and C-Tests are needed to check that the new capabilities are
-supported.
+ACATS B- and C-Tests are needed to check that the changes are
+supported (but mostly can be covered by tests for the original features).
 
 
 !appendix
@@ -1383,5 +1349,74 @@
 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