--- ai12s/ai12-0208-1.txt 2018/06/15 00:42:02 1.11 +++ ai12s/ai12-0208-1.txt 2018/12/07 03:03:40 1.12 @@ -1,4 +1,4 @@ -!standard A.5.5(0) 18-06-14 AI12-0208-1/04 +!standard A.5.5(0) 18-11-21 AI12-0208-1/05 !standard A.5.6(0) !standard A.5.7(0) !standard A.5.8(0) @@ -36,64 +36,54 @@ package Ada.Numerics.Big_Numbers with Pure, Nonblocking is - type Number is Interface; - - function "=" (L, R : Number) return Boolean is abstract; - function "<" (L, R : Number) return Boolean is abstract; - function "<=" (L, R : Number) return Boolean is abstract; - function ">" (L, R : Number) return Boolean is abstract; - function ">=" (L, R : Number) return Boolean is abstract; - - function To_String (Arg : Number) return String is abstract; - function From_String (Arg : String) return Number is abstract; - function "+" (Arg : Integer) return Number is abstract; - - function "-" (L : Number) return Number is abstract; - function "abs" (L : Number) return Number is abstract; - function "+" (L, R : Number) return Number is abstract; - function "-" (L, R : Number) return Number is abstract; - function "*" (L, R : Number) return Number is abstract; - function "/" (L, R : Number) return Number is abstract; - function Min (L, R : Number) return Number is abstract; - function Max (L, R : Number) return Number is abstract; + subtype Field is Integer range 0 .. implementation-defined; + subtype Number_Base is Integer range 2 .. 16; end Ada.Numerics.Big_Numbers; A.5.6 Big Integers The package Ada.Numerics.Big_Numbers.Big_Integers has the following definition: + with Ada.Streams; package Ada.Numerics.Big_Numbers.Big_Integers with Preelaborate, Nonblocking is - type Big_Integer is new Number with private with - Default_Initial_Condition => Big_Integer = 0, - Integer_Literal => From_String; - -[TBD: Remove Integer_Literal aspect spec if AI12-0249-1 not approved; -also replace "0" with "+0" in the default initial condition -and as needed in other conditions in order to get legal specs.] - - overriding function "=" (L, R : Big_Integer) return Boolean; - overriding function "<" (L, R : Big_Integer) return Boolean; - overriding function "<=" (L, R : Big_Integer) return Boolean; - overriding function ">" (L, R : Big_Integer) return Boolean; - overriding function ">=" (L, R : Big_Integer) return Boolean; + type Big_Integer is private with + Default_Initial_Condition => not Is_Valid (Big_Integer), + Integer_Literal => From_String, + Put_Image => Put_Image; + + function Is_Valid (Arg : Big_Integer) return Boolean; + + subtype Valid_Big_Integer is Big_Integer + with Dynamic_Predicate => Is_Valid (Valid_Big_Integer), + Predicate_Failure => (raise Constraint_Error); - overriding function "+" (Arg : Integer) return Big_Integer; - function To_Big_Integer (Arg : Integer) return Big_Integer renames "+"; + function Invalid return Big_Integer + with Post => not Is_Valid (Invalid'Result); - subtype Big_Positive is Big_Integer + 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 "+" (Arg : Integer) return Valid_Big_Integer; + function To_Big_Integer (Arg : Integer) return Valid_Big_Integer + renames "+"; + + subtype Big_Positive is Valid_Big_Integer with Dynamic_Predicate => Big_Positive > 0, Predicate_Failure => (raise Constraint_Error); - subtype Big_Natural is Big_Integer + subtype Big_Natural is Valid_Big_Integer with Dynamic_Predicate => Big_Natural >= 0, Predicate_Failure => (raise Constraint_Error); - function In_Range (Arg, Low, High : Big_Integer) return Boolean is + 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 => +Integer'First, High => +Integer'Last) @@ -102,8 +92,8 @@ generic type Int is range <>; package Signed_Conversions is - function To_Big_Integer (Arg : Int) return Big_Integer; - function From_Big_Integer (Arg : Big_Integer) return Int + function To_Big_Integer (Arg : Int) return Valid_Big_Integer; + 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)) @@ -113,49 +103,71 @@ generic type Int is mod <>; package Unsigned_Conversions is - function To_Big_Integer (Arg : Int) return Big_Integer; - function From_Big_Integer (Arg : Big_Integer) return Int + function To_Big_Integer (Arg : Int) return Valid_Big_Integer; + 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)) or else (raise Constraint_Error); end Unsigned_Conversions; - - overriding function To_String (Arg : Big_Integer) return String; - overriding function From_String (Arg : String) return Big_Integer; - overriding function "-" (L : Big_Integer) return Big_Integer; - overriding function "abs" (L : Big_Integer) return Big_Integer; - overriding function "+" (L, R : Big_Integer) return Big_Integer; - overriding function "-" (L, R : Big_Integer) return Big_Integer; - overriding function "*" (L, R : Big_Integer) return Big_Integer; - overriding function "/" (L, R : Big_Integer) return Big_Integer; - function "mod" (L, R : Big_Integer) return Big_Integer; - function "rem" (L, R : Big_Integer) return Big_Integer; - function "**" (L : Big_Integer; R : Natural) return Big_Integer; - overriding function Min (L, R : Big_Integer) return Big_Integer; - overriding function Max (L, R : Big_Integer) return Big_Integer; + function To_String (Arg : Valid_Big_Integer + Width : Field := 0; + Base : Number_Base := 10) return String + with Post => To_String'Result'First = 1; + function From_String (Arg : String; + Width : Field := 0) return Valid_Big_Integer; + + procedure Put_Image + (Arg : Valid_Big_Integer; + Stream : not null access Ada.Streams.Root_Stream_Type'Class); + + 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 - (L, R : Big_Integer) return Big_Integer with - Pre => (L /= 0 and R /= 0) or else (raise Constraint_Error), - Post => (Big_Integer'Result > 0); + (L, R : Valid_Big_Integer) return Big_Positive 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; -To_String and From_String behave like Integer'Image and Integer'Value except -that more digits are produced and accepted. [In particular, -the low bound of To_String'Result is 1, To_String'Result includes a leading -blank in the case of a nonnegative argument, and Constraint_Error is raised if -the argument to From_String is syntactically incorrect.] +To_String and From_String behave analogously to the Put and Get procedures +defined in Text_Io.Integer_IO (in particular, with respect to the +interpretation of the Width and Base parameters) except that +Constraint_Error, not Data_Error, is propagated in error cases +and the result of a call To_String with a Width parameter of 0 and +a nonnegative Arg parameter does not include a leading blank. +Put_Image calls To_String (passing in the default values for the Width and Base +parameters), prepends a leading blank if the argument is +nonnegative, converts that String to a Wide_Wide_String using +To_Wide_Wide_String, and writes the resulting value to the stream using +Wide_Wide_String'Write . The other functions have their usual mathematical meanings. -[TBD: GCD should return Big_Positive, not Big_Integer, if AI12-0243-1 -somehow allows this.] +Implementation Requirements + No storage associated with a Big_Integer object shall be lost upon + assignment or scope exit. + For purposes of determining whether predicate checks are performed + as part of default initialization, the type Big_Integer + shall be considered to have a subcomponent that has a default_expression. + + AARM Note: This means that the elaboration of + Default_Initialized_Object : Valid_Big_Integer; + is required to propagate Assertion_Error. A.5.7 Bounded Big Integers @@ -165,34 +177,26 @@ Numerics.Big_Numbers.Big_Integers, but with the difference that the maximum storage (and, consequently, the set of representable values) is bounded. -The generic package Ada.Numerics.Big_Numbers.Bounded_Big_Integers has the -following definition: +The declaration of the generic library package Big_Numbers.Bounded_Big_Integers +has the same contents and semantics as Big_Numbers.Big_Integer except: - generic - Capacity : Natural; - package Ada.Numerics.Big_Numbers.Bounded_Big_Integers - with Pure, Nonblocking - is - - <all the same visible declarations as those in Big_Numbers.Big_Integers, - including declaration of Bounded_Big_Integers.Big_Integer type; however - the partial view of Bounded_Big_Integers.Big_Integer type includes - a type invariant specification, - Type_Invariant => - In_Range (Bounded_Big_Integer, First, Last) - or else (raise Constraint_Error) - > - - function Last return Big_Integer is ((+256) ** Capacity); - function First return Big_Integer is (-Last); - private - ... -- not specified by the language - end Ada.Numerics.Big_Numbers.Bounded_Big_Integers; + - Bounded_Big_Integers is a generic package and takes a generic formal: + Capacity : Natural; -Each operation behaves like the corresponding Big_Numbers.Big_Integers -operation except that Constraint_Error is raised if a result R -would fail the test In_Range (R, First, Last). This includes the -streaming operations Big_Integer'Read and Big_Integer'Input. + - two additional visible expression functions are declared: + function Last return Valid_Big_Integer is ((+256) ** Capacity); + function First return Valid_Big_Integer is (-Last); + + - the partial view of Bounded_Big_Integers.Big_Integer includes + a type invariant specification, + Type_Invariant => + (if Is_Valid (Bounded_Big_Integer) then + In_Range (Bounded_Big_Integer, First, Last) + or else (raise Constraint_Error)) + +Each subprogram of an instance of Bounded_Big_Integers.Bounded_Big_Integer +behaves like the corresponding Big_Numbers.Big_Integers subprogram except +that type invariant checks are performed as described in 7.3.2. Implementation Requirements @@ -201,7 +205,8 @@ corresponding Input or Read operations of the Big_Integer type declared in either another instance of Bounded_Big_Integers or in the package Numerics.Big_Numbers.Big_Integers. [This is subject to the -preceding requirement that Constraint_Error is raised in some cases.] +preceding requirement that type invariant checks are performed, so +that Constraint_Error may be raised in some cases.] Implementation Advice @@ -225,10 +230,12 @@ package Ada.Numerics.Big_Numbers.Conversions with Preelaborate, Nonblocking is - function From_Unbounded - (Arg : Big_Integers.Big_Integer) return Bounded.Big_Integer; - function To_Unbounded - (Arg : Bounded.Big_Integer) return Big_Integers.Big_Integer; + function To_Bounded + (Arg : Big_Integers.Valid_Big_Integer) + return Bounded.Valid_Big_Integer; + function From_Bounded + (Arg : Bounded.Valid_Big_Integer) + return Big_Integers.Valid_Big_Integer; end Ada.Numerics.Big_Numbers.Conversions; A.5.8 Big Rationals @@ -236,59 +243,163 @@ The package Ada.Numerics.Big_Numbers.Big_Rationals has the following definition: with Ada.Numerics.Big_Numbers.Big_Integers; + with Ada.Streams; package Ada.Numerics.Big_Numbers.Big_Rationals with Preelaborate, Nonblocking is use Big_Integers; - type Big_Rational is new Number with private - Default_Initial_Condition => Big_Rational = 0.0, + type Big_Rational is private with + Default_Initial_Condition => not Is_Valid (Big_Rational), Real_Literal => From_String, - Type_Invariant => (Big_Rational = 0.0) or else + Put_Image => Put_Image, + Type_Invariant => + (not Is_Valid (Big_Rational)) or else + (Big_Rational = 0.0) or else (Greatest_Common_Divisor (Numerator (Big_Rational), Denominator (Big_Rational)) = 1); - function "/" (Num, Den : Big_Integer) return Big_Rational + function Is_Valid (Arg : Big_Rational) return Boolean; + + function Invalid return Big_Rational + with Post => not Is_Valid (Invalid'Result); + + subtype Valid_Big_Rational is Big_Rational + with Dynamic_Predicate => Is_Valid (Valid_Big_Rational), + Predicate_Failure => (raise Constraint_Error); + + function "/" (Num, Den : Valid_Big_Integer) return Valid_Big_Rational with Pre => (Den /= 0) or else (raise Constraint_Error); - function Numerator (Arg : Big_Rational) return Big_Integer; - function Denominator (Arg : Big_Rational) return Big_Positive; + function Numerator (Arg : Valid_Big_Rational) return Valid_Big_Integer; + function Denominator (Arg : Valid_Big_Rational) return Big_Positive; - overriding function "+" (Arg : Integer) return Big_Rational is + function "+" (Arg : Integer) return Valid_Big_Rational is ((+Arg) / 1); + + function To_Big_Rational (Arg : Integer) return Valid_Big_Rational + renames "+"; + + function "=" (L, R : Valid_Big_Rational) return Boolean; + function "<" (L, R : Valid_Big_Rational) return Boolean; + function "<=" (L, R : Valid_Big_Rational) return Boolean; + function ">" (L, R : Valid_Big_Rational) return Boolean; + function ">=" (L, R : Valid_Big_Rational) return Boolean; + + generic + type Num is digits <>; + package Float_Conversions is + function To_Big_Rational (Arg : Num) return Valid_Big_Rational; - function To_Big_Rational (Arg : Integer) return Big_Rational renames "+"; + function From_Big_Rational (Arg : Valid_Big_Rational) return Num + with Pre => In_Range (Arg, + Low => To_Big_Rational (Num'First), + High => To_Big_Rational (Num'Last)) + or else (raise Constraint_Error); + end Float_Conversions; - overriding function "=" (L, R : Big_Rational) return Boolean; - overriding function "<" (L, R : Big_Rational) return Boolean; - overriding function "<=" (L, R : Big_Rational) return Boolean; - overriding function ">" (L, R : Big_Rational) return Boolean; - overriding function ">=" (L, R : Big_Rational) return Boolean; + function To_String (Arg : Valid_Big_Rational; + Fore : Field := 2; + Aft : Field := 3; + Exp : Field := 0) return String + with Post => To_String'Result'First = 1; + function From_String (Arg : Valid_Big_Rational; + Width : Field := 0); - overriding function To_String (Arg : Big_Rational) return String is + function To_Quotient_String (Arg : Valid_Big_Rational) return String is (To_String (Numerator (Arg)) & " /" & To_String (Denominator (Arg))); - overriding function From_String (Arg : String) return Big_Rational; + function From_Quotient_String (Arg : String) return Valid_Big_Rational; - overriding function "-" (L : Big_Rational) return Big_Rational; - overriding function "abs" (L : Big_Rational) return Big_Rational; - overriding function "+" (L, R : Big_Rational) return Big_Rational; - overriding function "-" (L, R : Big_Rational) return Big_Rational; - overriding function "*" (L, R : Big_Rational) return Big_Rational; - overriding function "/" (L, R : Big_Rational) return Big_Rational; - function "**" (L : Big_Rational; R : Integer) return Big_Rational; - overriding function Min (L, R : Big_Rational) return Big_Rational; - overriding function Max (L, R : Big_Rational) return Big_Rational; + procedure Put_Image + (Arg : Valid_Big_Rational; + Stream : not null access Ada.Streams.Root_Stream_Type'Class); + + function "-" (L : Valid_Big_Rational) return Valid_Big_Rational; + function "abs" (L : Valid_Big_Rational) return Valid_Big_Rational; + function "+" (L, R : Valid_Big_Rational) return Valid_Big_Rational; + function "-" (L, R : Valid_Big_Rational) return Valid_Big_Rational; + function "*" (L, R : Valid_Big_Rational) return Valid_Big_Rational; + function "/" (L, R : Valid_Big_Rational) return Valid_Big_Rational; + function "**" (L : Valid_Big_Rational; R : Integer) + return Valid_Big_Rational; + function Min (L, R : Valid_Big_Rational) return Valid_Big_Rational; + function Max (L, R : Valid_Big_Rational) return Valid_Big_Rational; private ... -- not specified by the language end Ada.Numerics.Big_Numbers.Big_Rationals; -From_String implements the inverse function of To_String; Constraint_Error is -propagated in error cases. +To_String and From_String behave analogously to the Put and Get procedures +defined in Text_Io.Float_IO (in particular, with respect to the +interpretation of the Fore, Aft, Exp, and Width parameters), except that +Constraint_Error (not Data_Error) is propagated in error cases. +From_Quotient_String implements the inverse function of 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 +the resulting value to the stream using Wide_Wide_String'Write. + +To_Big_Rational is exact (i.e., the result represents exactly the same +mathematical value as the argument). From_Big_Rational is subject to +the same precision rules as a type conversion of a value of type T to +the target type Num, where T is a hypothetical floating point type whose +model numbers include all of the model numbers of Num as well as the +exact mathematical value of the argument. + +[TBD: Is Constraint_Error the exception we want on the Predicate_Failure +aspect specs for Valid_Big_Integer and Valid_Big_Rational?] +[TBD: do we want a Fixed_Conversions generic package analogous to +Float_Conversions?] +[TBD: the range check on From_Big_Rational is slightly too tight. +For example, + X : IEEE_Float32 := + IEEE_Float32 (IEEE_Float64'Succ (IEEE_Float64 (IEEE_Float32'Last))); +does not overflow but the corresponding conversion using From_Big_Rational +would fail the range check. Do we care?] + The other functions have their usual mathematical meanings. +Implementation Requirements + No storage associated with a Big_Rational object shall be lost upon + assignment or scope exit. + + For purposes of determining whether predicate checks are performed + as part of default initialization, the type Big_Rational + shall be considered to have a subcomponent that has a default_expression. + + AARM Note: This means that the elaboration of + Default_Initialized_Object : Valid_Big_Rational; + is required to propagate Assertion_Error. + AARM Note: No Bounded_Big_Rationals generic package is provided. +==== + +This section, or at least the AARM note, is intended to follow +the structure of the analogous wording for AI12-0112 (contracts for +containers). + +Add after 11.5(23): + +Big_Number_Check + +Perform the checks associated with Pre, Static_Predicate, Dynamic_Predicate, +or Type_Invariant aspect specifications occuring in the visible part of +package Ada.Big_Numbers or of any of its descendants. + +[TBD: Include Static_Predicate in this list just for completeness, even +though it happens that there are no Static_Predicate specifications in +these units?] + +AARM Reason: One could use the Assertion_Policy to eliminate such checks, +but that would require recompiling the Ada.Big_Numbers packages (the +assertion policy that determines whether the checks are made is that +used to compile the unit). In addition, we do not want to specify the +behavior of the Ada.Big_Numbers operations if a precondition or predicate +fails; that is different than the usual behavior of Assertion_Policy. +By using Suppress for this purpose, we make it clear that suppressing +a check that would have failed results in erroneous execution. + + !discussion ** None yet. @@ -3396,10 +3507,10 @@ From: Randy Brukardt Sent: Thursday, June 14, 2018 7:13 PM -> I think the attached is just the result of incorporating what we +> I think the attached is just the result of incorporating what we > discussed. -Looks good. I fixed a couple of typos (missing "-1" on AI numbers, missing +Looks good. I fixed a couple of typos (missing "-1" on AI numbers, missing ";" at the end of your new type invariant). Do we still need the text: @@ -3408,17 +3519,17 @@ (R = 0.0) or else (Greatest_Common_Divisor (Numerator (R), Denominator (R)) = 1). -since it is essentially just restating the Type_Invariant. (The spelling of +since it is essentially just restating the Type_Invariant. (The spelling of "satisfies" is interesting, too. ;-) -> The one exception is that I used a type invariant to express the idea -> that the GCD of the numerator and denominator of a non-zero big real +> The one exception is that I used a type invariant to express the idea +> that the GCD of the numerator and denominator of a non-zero big real > is always one. -You would use the least used of the contracts. ;-) I note that the new +You would use the least used of the contracts. ;-) I note that the new ObjectAda doesn't include Type_Invariants (and I don't have any plans to -implement them in Janus/Ada, either). But that's hardly a good reason to not -use something when it is appropriate. (I'd probably turn it into a +implement them in Janus/Ada, either). But that's hardly a good reason to not +use something when it is appropriate. (I'd probably turn it into a postcondition for Janus/Ada.) **************************************************************** @@ -3427,13 +3538,13 @@ Sent: Thursday, June 14, 2018 7:29 PM > Do we still need the text: -> -> Any Big_Rational result R returned by any of these functions +> +> Any Big_Rational result R returned by any of these functions > satisifies the condition > (R = 0.0) or else > (Greatest_Common_Divisor (Numerator (R), Denominator (R)) = 1). -> -> since it is essentially just restating the Type_Invariant. (The +> +> since it is essentially just restating the Type_Invariant. (The > spelling of "satisfies" is interesting, too.;-) Good point. I agree that we no longer need that text. @@ -3449,10 +3560,10 @@ ... > > You would use the least used of the contracts. -> +> > You should be thanking me for not using the "stable properties" stuff. -I was trying to figure out how to implement your type invariant with a +I was trying to figure out how to implement your type invariant with a stable property function, but that wouldn't work on the function results. Anyway, stable properties is extensively used in the containers contracts (AI12-0112-1), so I wouldn't mind in the least if you used it. @@ -3465,5 +3576,37 @@ > Good point. I agree that we no longer need that text. OK, I deleted it (making a new AI version). + +**************************************************************** + +From: Steve Baird +Sent: Wednesday, November 21, 2018 7:23 PM + +The attached is intended to incorporate the directions I received from the +group in Lisbon. [This is version /05 of the AI - Editor.] + +The big numeric types are no longer tagged. + +They default to an invalid value instead of to zero. + +Conversions to and from String look a lot more like the corresponding Text_IO +operations (with Width, Base, Fore, Aft, and Exp parameters). + +Each big number type gets a visible Put_Image aspect spec. + +Some name changes (To_Unbounded => From_Bounded, etc.). + +Also (not directed by group) the old To_String and From_String that +generated/consumed strings of the form + <numerator image> / <denominator image> are still around, but are now named + To_Quotient_String and From_Quotient_String These names, like any names, + are subject to discussion. + +Finally, a Big_Number_Check argument for pragma Suppress. + +As usual, thanks to Randy for preliminary review. + +Hopefully, all the right rules are in place for deciding when you get a +leading blank on the image of a positive integer. ****************************************************************

Questions? Ask the ACAA Technical Agent