CVS difference for 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