--- ai12s/ai12-0366-1.txt 2020/03/07 03:03:15 1.2 +++ ai12s/ai12-0366-1.txt 2020/04/28 02:33:02 1.3 @@ -1,4 +1,4 @@ -!standard A.5.6(0) 20-02-10 AI12-0366-1/01 +!standard A.5.6(0) 20-04-26 AI12-0366-1/02 !standard A.5.7(0) !class Amendment 20-02-10 !status work item 20-02-10 @@ -10,20 +10,51 @@ !problem -After implementing and experimenting with Big_Integers and Big_Reals at -AdaCore both from an Ada usage point of view and from a SPARK usage point -of view, we came to the conclusion that the proposed API is unnecessarily -complex and confusing for users, and in addition not practical for use in -SPARK. +After implementing and experimenting with Big_Integers and Big_Reals at +AdaCore both from an Ada usage point of view and from a SPARK usage +point of view, we came to the conclusion that the proposed API is +unnecessarily complex and confusing for users. In addition, for SPARK +there is a desire to map these to mathematical integers/reals, and having an +explicit "invalid" representation prevents a natural mapping. !proposal -Change the package specification for Big_Integers to: +We propose to eliminate the ability to create an explicitly invalid +representation, and try to model Big_Integer more closely on Integer +(and Big_Real more closely on Float), where it is potentially invalid if +never initialized, but there is no way to generate an invalid value +other than by omitting initialization. As a result we dispense with the +word "Optional", though we preserve the way to check whether a +Big_Integer/Real Is_Valid. + +We originally intended to use Is_Valid directly in pre- and +postconditions to clarify where the parameters and the results are +expected to be valid. We ultimately declared a named subtype +Valid_Big_Integer/Real with a Dynamic_Predicate => Is_Valid +(Valid_Big_Integer/Real) and a Predicate_Failure => raise Program_Error, to +avoid having to repeat the "or else raise Program_Error" on every +appearance of Is_Valid. We were originally concerned that adding a named +subtype would make the package more complex without providing sufficient +benefit to the user, but having to repeat "or else raise Program_Error" +in every precondition seems to tip the scale toward the use of a +predicated subtype, and actually shortens and unclutters the final +package specification. + +We specify that the function Is_Valid has an Intrinsic calling +convention to prevent a call on it from being "hidden" from the compiler +by a level of indirection, so that it can be implemented by an attribute +in some contexts (e.g. 'Initialized in SPARK). -with Ada.Streams; +!wording +[Author's note: This includes the effect of AI12-0340-1; it changed +Put_Image to work on Text_Buffers.] + +Replace A.5.6 (2/5-21/5) with the following: + +with Ada.Strings.Text_Buffers; package Ada.Numerics.Big_Numbers.Big_Integers - with Preelaborate, Nonblocking + with Preelaborate, Nonblocking, Global => null is type Big_Integer is private with Integer_Literal => From_String, @@ -32,40 +63,38 @@ function Is_Valid (Arg : Big_Integer) return Boolean with Convention => Intrinsic; - function "=" (L, R : Big_Integer) return Boolean - with Pre => Is_Valid (L) and Is_Valid (R); + subtype Valid_Big_Integer is Integer + with Dynamic_Predicate => Is_Valid (Valid_Big_Integer), + Predicate_Failure => raise Program_Error; - function "<" (L, R : Big_Integer) return Boolean - with Pre => Is_Valid (L) and Is_Valid (R); + function "=" (L, R : Valid_Big_Integer) return Boolean; - function "<=" (L, R : Big_Integer) return Boolean - with Pre => Is_Valid (L) and Is_Valid (R); + function "<" (L, R : Valid_Big_Integer) return Boolean; - function ">" (L, R : Big_Integer) return Boolean - with Pre => Is_Valid (L) and Is_Valid (R); + function "<=" (L, R : Valid_Big_Integer) return Boolean; - function ">=" (L, R : Big_Integer) return Boolean - with Pre => Is_Valid (L) and Is_Valid (R); + function ">" (L, R : Valid_Big_Integer) return Boolean; - function To_Big_Integer (Arg : Integer) return Big_Integer; + function ">=" (L, R : Valid_Big_Integer) return Boolean; + + function To_Big_Integer (Arg : Integer) return Valid_Big_Integer; subtype Big_Positive is Big_Integer with Dynamic_Predicate => Big_Positive > 0, - Predicate_Failure => (raise Constraint_Error); + Predicate_Failure => raise Constraint_Error; subtype Big_Natural is Big_Integer with Dynamic_Predicate => Big_Natural >= 0, - Predicate_Failure => (raise Constraint_Error); + Predicate_Failure => raise Constraint_Error; function In_Range (Arg, Low, High : Big_Integer) return Boolean is - ((Low <= Arg) and (Arg <= High)) - with Pre => Is_Valid (Arg) and Is_Valid (Low) and Is_Valid (High); + (Low <= Arg and Arg <= High); function To_Integer (Arg : Big_Integer) return Integer with Pre => In_Range (Arg, Low => To_Big_Integer (Integer'First), High => To_Big_Integer (Integer'Last)) - or else (raise Constraint_Error); + or else raise Constraint_Error; generic type Int is range <>; @@ -77,7 +106,7 @@ with Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error); + or else raise Constraint_Error; end Signed_Conversions; @@ -91,62 +120,49 @@ with Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error); + or else raise Constraint_Error; end Unsigned_Conversions; - function To_String (Arg : Big_Integer; + function To_String (Arg : Valid_Big_Integer; Width : Field := 0; Base : Number_Base := 10) return String - with Pre => Is_Valid (Arg), - Post => To_String'Result'First = 1; + with => Post => To_String'Result'First = 1; - function From_String (Arg : String) return Big_Integer; + function From_String (Arg : String) return Valid_Big_Integer; procedure Put_Image - (Stream : not null access Ada.Streams.Root_Stream_Type'Class; - Arg : Big_Integer) - with Pre => Is_Valid (Arg); + (Buffer : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class; + Arg : Valid_Big_Integer); - function "+" (L : Big_Integer) return Big_Integer - with Pre => Is_Valid (L); + function "+" (L : Valid_Big_Integer) return Valid_Big_Integer; - function "-" (L : Big_Integer) return Big_Integer - with Pre => Is_Valid (L); + function "-" (L : Valid_Big_Integer) return Valid_Big_Integer; - function "abs" (L : Big_Integer) return Big_Integer - with Pre => Is_Valid (L); + function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer; - function "+" (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer; - function "-" (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer; - function "*" (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer; - function "/" (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer; - function "mod" (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer; - function "rem" (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer; - function "**" (L : Big_Integer; R : Natural) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function "**" + (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer; - function Min (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer; - function Max (L, R : Big_Integer) return Big_Integer - with Pre => Is_Valid (L) and Is_Valid (R); + function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer; function Greatest_Common_Divisor - (L, R : Big_Integer) return Big_Positive - with Pre => (L /= 0 and R /= 0) or else (raise Constraint_Error); + (L, R : Valid_Big_Integer) return Big_Positive + with Pre => (L /= 0 and R /= 0) or else raise Constraint_Error; private @@ -154,22 +170,216 @@ end Ada.Numerics.Big_Numbers.Big_Integers; +Modify A.5.6(22/5): -!wording + 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]{buffer using Text_Buffers.Put}. + +Modify A.5.6 (24/5-25/5): + + 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. + +Replace A.5.7 (2/5 to 19/5) with the following: + +with Ada.Numerics.Big_Numbers.Big_Integers; use all type Big_Integers; +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; + + function Is_Valid (Arg : Big_Real) return Boolean + with Convention => Intrinsic; + + subtype Valid_Big_Real is Big_Real + with Dynamic_Predicate => Is_Valid (Valid_Big_Real), + Predicate_Failure => raise Program_Error; + + function "/" (Num, Den : Big_Integers.Big_Integer) return Valid_Big_Real; + with Pre => Den /= 0 + or else raise Constraint_Error; + + function Numerator + (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer; + + function Denominator + (Arg : Valid_Big_Real) return Big_Integers.Big_Positive + with Post => + Arg = 0.0 or else + 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_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); + + 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; + Fore : Field := 2; + Aft : Field := 3; + Exp : Field := 0) return String + with Post => To_String'Result'First = 1; + + function From_String (Arg : String) return Valid_Big_Real; + + function To_Quotient_String (Arg : Valid_Big_Real) return String is + (Big_Integers.To_String (Numerator (Arg)) & " / " + & Big_Integers.To_String (Denominator (Arg))); + + function From_Quotient_String (Arg : String) return Valid_Big_Real; + + procedure Put_Image + (Buffer : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class; + Arg : 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): + + 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, and Exp 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 {writes} the resulting value to the + [stream] buffer using [Wide_Wide_String'Write]{Text_Buffers.Put}. + +Modify 4.5.7 (23/5 to 24/5): + + The type [Optional_]Big_Real needs finalization (see 7.6). -** TBD. + Implementation Requirements -[There are a number of other wording issues touched on in the e-mail -threads below that need to be relfected here (or somewhere). + 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. + !discussion -** TBD. +See the !proposal for most of the rationale. We change the Global +aspects to be simply "null", though the implementation is always +permitted to add back the "synchronized in out Big_Integers/Reals" if needed. +At least logically, there is no need for any side effects in any of the +operations. + +We add a "use all type Big_Integers.Big_Integer;" to the context clause +for Big_Reals to make the specification easier to read. It seems +unlikely that this will introduce any confusion or ambiguity. + +After changing the "shall be" to "is", we move the indications that +predicate checks are performed on default initialization to new +Dynamic Semantics sections, as that is where they seem to best belong. + +--- + +There was a request to change the postcondition of Demoninator to +say something about the result when Arg = 0.0. However, there seemed to +be no consensus for a change. !ASIS -[Not sure. It seems like some new capabilities might be needed, -but I didn't check - Editor.] +Most likely, no ASIS support needed. (Unsure if the special semantics +of Is_Valid are ). !ACATS test @@ -968,5 +1178,205 @@ If Ada could detect this sort of error (especially at compile-time, like SPARK does), then I wouldn't care as much, but it can't (and as noted above, it's impractical to do so now for scalars). + +**************************************************************** + +From: Christoph Grein +Sent: Saturday, April 4, 2020 1:53 PM + +!topic Wrong Postcondition +!reference Ada 202x RM A.5.7(8/5) Draft 24 +!from Christoph Grein 20-04-04 +!discussion + +function Denominator (Arg : Big_Real) return Big_Positive +with Post => + (Arg = 0.0) or else + (Big_Integers.Greatest_Common_Divisor + (Numerator (Arg), Denominator'Result) = 1); + +The argument Arg in the postcondition looks strange. Perhaps this is meant: + +(if Arg = 0.0 then Denominator'Result = 1) + +**************************************************************** + +From: Yannick Moy +Sent: Wednesday, April 8, 2020 2:58 PM + +I think the postcondition is correct. It says that in general Numerator and +Denominator should be coprime. This does not apply to the case where Arg is +0.0, hence the form of the postcondition. + +**************************************************************** + +From: Christoph Grein +Sent: Thursday, April 9, 2020 10:48 AM + +But this is exactly what my version says. Arg = 0.0 doesn't tell anything +about the denominator. It could be any Big_Pos, e.g. 100 then. But I'm sure +1 will be returned in this case. + +**************************************************************** + +From: Christoph Grein +Sent: Monday, April 20, 2020 12:19 PM + +Since there is silence: + +Am I the only one who thinks (Arg = 0.0) as a Post is utter nonsense? I try to +be polite... + +Denominator (0/12) with this Post can return anything, for instance +31415926535897, but I'm sure any sensible implementation will return 1. + +If anyone can prove to me that this follows from Arg=0.0, I'll keep silent +forever, I promise. + +**************************************************************** + +From: Christoph Grein +Sent: Monday, April 20, 2020 12:30 PM + +> Am I the only one who thinks (Arg = 0.0) as a Post is utter nonsense? I try +> to be polite... + +as written, the postcondition is an implication: + + if not (Arg = 0.0) then + (Big_Integers.Greatest_Common_Divisor + (Numerator (Arg), Denominator'Result) = 1) + +as any implication, it does not say anything about the case when the guard is false + +> Denominator (0/12) with this Post can return anything, for instance +> 31415926535897, but I'm sure any sensible implementation will return 1. +> +> If anyone can prove to me that this follows from Arg=0.0, I'll keep silent +> forever, I promise. + +It does not. I assume that the ARG did not mean here to write a complete +postcondition for this operation, just one that they felt was useful. It also +leaves to the implementation some flexibility in returning whatever for the +Denominator of real "0". + +**************************************************************** + +From: Christoph Grein +Sent: Monday, April 20, 2020 8:35 PM + +... +>as any implication, it does not say anything about the case when the guard +>is false + +I admit that this is logically equivalent to what is written, but it is more +intuitive in leaving the 0.0 case open. + +>It does not. I assume that the ARG did not mean here to write a complete +>postcondition for this operation, just one that they felt was useful. It +>also leaves to the implementation some flexibility in returning whatever +>for the Denominator of real "0". + +But why should ARG do so? 1 is the normal expected result. Anything else would +be very surprising. Note the Dewar rule. (At least an AARM note would be +appropriate in this case.) + +I note that the RM does not say big reals are held in reduced form +Big_Integers.Greatest_Common_Divisor (Numerator, Denominator) = 1. So 2/12 +and 1/6 would both be allowed internal representations, or I/(I*6) for any +big integer. But I presume Numerator (no Post) would return 1 and Denominator +(because of Post) must return 6; and 2/12=1/6 would return True. + +**************************************************************** + +From: Bob Duff +Sent: Tuesday, April 21, 2020 4:16 PM + +> It does not. I assume that the ARG did not mean here to write a complete +> postcondition for this operation, just one that they felt was useful. It +> also leaves to the implementation some flexibility in returning whatever +> for the Denominator of real "0". + +I agree with Christoph that this implementation freedom is undesirable. +The Post should specify both cases (Arg = zero and nonzero). + +For zero, Numerator should be 0 and Denominator should be 1. + +So the Post as written is not wrong, but incomplete. + +> But why should ARG do so? 1 is the normal expected result. Anything +> else would be very surprising. Note the Dewar rule. (At least an AARM +> note would be appropriate in this case.) +> +> I note that the RM does not say big reals are held in reduced form +> Big_Integers.Greatest_Common_Divisor (Numerator, Denominator) = 1. So +> 2/12 and 1/6 would both be allowed internal representations, or +> I/(I*6) for any big integer. + +Yes, but having implemented these things before, I'm pretty sure the internal +rep should use lowest terms. Otherwise numbers grow bigger and bigger as you +do computations. (I mean "bigger" as in "number of bits", not the magnitude +of the number. A small-magnitude number like 1/(10**1000) is "big" in terms +of number of bits stored.) + +And you have to be able to compute lowest terms anyway in order for "=" to get +the right answer. + +>...But I presume Numerator (no Post) would return 1 and Denominator +>(because of Post) must return 6; and 2/12=1/6 would return True. + +Yes, and the easiest and most efficient way to accomplish that is to always +store 1 and 6. + +**************************************************************** + +From: Randy Brukardt +Sent: Tuesday, April 21, 2020 5:16 PM + +... +> Yes, but having implemented these things before, I'm pretty sure the +> internal rep should use lowest terms. Otherwise numbers grow bigger +> and bigger as you do computations. (I mean "bigger" +> as in "number of bits", not the magnitude of the number. +> A small-magnitude number like 1/(10**1000) is "big" in terms of number +> of bits stored.) +> +> And you have to be able to compute lowest terms anyway in order for +> "=" to get the right answer. + +I'm unconvinced. Normalization to lowest terms is *very* expensive in general +(since it implies doing many trial divides, and divides are the most expensive +operations). Moreover, you never need it (you need to get the same denominator +for "=", not the lowest terms - that can be done by multiplying the numerator +and denominator by the same value). If your operation mix includes a lot of +math and just a few "=" operations, you may be better off only doing +normalization when you need it. + +(As I recall, the package used in Janus/Ada only normalizes away right-hand +zero bits [as that is relatively cheap] rather than full normalization. I'd +use that as the basis of any Bignum package for Janus/Ada, since I have no +interest in writing/debugging a lot of assembler code again.) + +> >...But I presume Numerator (no Post) would return 1 and Denominator +> >(because of Post) must return 6; and 2/12=1/6 would return True. +> +> Yes, and the easiest and most efficient way to accomplish that is to +> always store 1 and 6. + +Sure, because in this case you're dealing with extra 2s and detecting those +is cheap (test the bottom bit for zero). Detecting extra factors of 7 and +13 and 19 is not cheap. + +**************************************************************** + +From: Christoph Grein +Sent: Wednesday, April 22, 2020 1:13 PM + +As I said, the RM does not require the reduced form (I supposed something +like this as the reason: you need to get the same denominator for "=", not +the lowest terms - that can be done by multiplying the numerator and +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. ****************************************************************

Questions? Ask the ACAA Technical Agent