!standard A.5.6(0) 20-02-10 AI12-0366-1/01 !standard A.5.7(0) !class Amendment 20-02-10 !status work item 20-02-10 !status received 20-01-02 !priority Low !difficulty Easy !subject Changes to Big_Integer and Big_Real !summary !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. !proposal Change the package specification for Big_Integers to: with Ada.Streams; package Ada.Numerics.Big_Numbers.Big_Integers with Preelaborate, Nonblocking is type Big_Integer is private with Integer_Literal => From_String, Put_Image => Put_Image; 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); function "<" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function "<=" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function ">" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function ">=" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function To_Big_Integer (Arg : Integer) return Big_Integer; subtype Big_Positive is Big_Integer with Dynamic_Predicate => Big_Positive > 0, Predicate_Failure => (raise Constraint_Error); subtype Big_Natural is Big_Integer with Dynamic_Predicate => Big_Natural >= 0, 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); 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); 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 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 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 : Big_Integer; Width : Field := 0; Base : Number_Base := 10) return String with Pre => Is_Valid (Arg), Post => To_String'Result'First = 1; function From_String (Arg : String) return Big_Integer; procedure Put_Image (Stream : not null access Ada.Streams.Root_Stream_Type'Class; Arg : Big_Integer) with Pre => Is_Valid (Arg); function "+" (L : Big_Integer) return Big_Integer with Pre => Is_Valid (L); function "-" (L : Big_Integer) return Big_Integer with Pre => Is_Valid (L); function "abs" (L : Big_Integer) return Big_Integer with Pre => Is_Valid (L); function "+" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "-" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "*" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "/" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "mod" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "rem" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "**" (L : Big_Integer; R : Natural) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function Min (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function Max (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function Greatest_Common_Divisor (L, R : 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; !wording ** TBD. [There are a number of other wording issues touched on in the e-mail threads below that need to be relfected here (or somewhere). !discussion ** TBD. !ASIS [Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.] !ACATS test ACATS B- and C-Tests are needed to check that the new capabilities are supported. !appendix From: Tucker Taft Sent: Monday, December 2, 2019 8:18 AM Bob Duff noticed that we used a "shall" where we should simply be saying "is", in A.5.6(26/5): (26/5) 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. If we agree with this change, then the paragraph should be moved to "static semantics" from its current location in "implementation requirements." **************************************************************** From: Randy Brukardt Sent: Monday, December 2, 2019 9:38 PM > Bob Duff noticed that we used a "shall" where we should simply be > saying "is", in A.5.6(26/5): > > (26/5) 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. A.5.7(25.5) has similar wording. > If we agree with this change, then the paragraph should be moved to > "static semantics" from its current location in "implementation > requirements." I'm not certain I agree with this. I looked up all of the uses of "for the purpose of" in the RM, and it is in many sections but I didn't find any in "static semantics". (I saw "Legality Rules", "Metrics", and "Post-Compilation Rules" along with "Implementation Requirements"). The closest similar case is A(3.1/4), which is in Implementation Requirements. (But it's not that similar; I do note that it uses "is".) There are more uses of "for the purposes of", but again the majority of those are in Legality Rules or Dynamic Semantics. There are also some non-normative uses. There are a handful in "Static Semantics" sections: There are some associated with language-defined packages, but for those the entire definition is in "Static Semantics". 3.9.3(12.3/3) is in "Static Semantics", but it starts "For the purposes of dynamic semantics...". Bizarre! 3.3(23.11/5) is in "Static Semantics", but it is part of the definition of "known to be constrained". A rather different case. 6.3.1(24.1/2) is in "Static Semantics", but it is part of the definition of "known to be constrained". A rather different case. 10.2.1(15.3/2) is in "Static Semantics", but it is part of the preceding rule rather than standing alone. 12.6(9.1/3) is in "Static Semantics", but it is connected by "then" to preceding text (it also does not stand alone). 13.10(3) is in "Static Semantics", but it is connected by "except" to preceding text (a very different meaning). Conclusion: I can't find anything very similar in the Standard to this wording. There's an argument for leaving it in "Implementation Requirements" and an argument for moving it to "Static Semantics". There's no argument for using "shall", however. **************************************************************** From: Tucker Taft Sent: Tuesday, December 3, 2019 9:09 AM It could be in dynamic semantics instead. Either makes more sense than being an implementation requirement. **************************************************************** From: Tucker Taft Sent: Tuesday, December 10, 2019 1:08 PM The GNAT folks have implemented a variant of the Big_Integers API, after a fair amount of internal discussion. In this variant, there is no Optional_Big_Integer, but Big_Integer can be declared without an explicit initial value. Ideally Bob or Steve will write up an AI to give the details. The goal was to make Big_Integer more like "regular" Integer. **************************************************************** From: Jeff Cousins Sent: Thursday, December 12, 2019 2:38 AM > The GNAT folks have implemented a variant of the Big_Integers API That sounds like good news! **************************************************************** From: Arnaud Charlet Sent: Thursday, December 12, 2019 2:43 AM Right and this confirms that prototyping and experimenting before standardizing is critically important and useful. **************************************************************** From: Arnaud Charlet Sent: Tuesday, January 14, 2020 2:33 AM 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. For Ada users: having to deal with two different type (a type and a subtype) and having to choose which one is relevant is a real burden and can actually lead to the wrong choice, only caught late at runtime, and makes reading and understand the API much harder. For SPARK users: having two different types makes generating provable formulas much harder and not direct. Since we anticipate SPARK users to be "big users" of "big integers", not having a straightforward and optimal mapping is really not suitable. Proposed change: use a single type for Big_Integer and Big_Real and remove all the Optional_Big_* types. Instead state that reading an uninitialized Big_* variable is a bounded error, similar to all scalar types, and add a precondition to each subprogram in the Big_Integers/Big_Reals packages ensuring that all possible uses of these objects is properly checked, except for the Is_Valid function itself, which is marked Intrinsic so that it's 'Access cannot be taken. See the below for the proposed API for Big_Integers. A similar change is proposed for Big_Reals which has been successfully implemented and used at AdaCore. -- with Ada.Streams; package Ada.Numerics.Big_Numbers.Big_Integers with Preelaborate, Nonblocking is type Big_Integer is private with Integer_Literal => From_String, Put_Image => Put_Image; 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); function "<" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function "<=" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function ">" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function ">=" (L, R : Big_Integer) return Boolean with Pre => Is_Valid (L) and Is_Valid (R); function To_Big_Integer (Arg : Integer) return Big_Integer; subtype Big_Positive is Big_Integer with Dynamic_Predicate => Big_Positive > 0, Predicate_Failure => (raise Constraint_Error); subtype Big_Natural is Big_Integer with Dynamic_Predicate => Big_Natural >= 0, 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); 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); 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 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 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 : Big_Integer; Width : Field := 0; Base : Number_Base := 10) return String with Pre => Is_Valid (Arg), Post => To_String'Result'First = 1; function From_String (Arg : String) return Big_Integer; procedure Put_Image (Stream : not null access Ada.Streams.Root_Stream_Type'Class; Arg : Big_Integer) with Pre => Is_Valid (Arg); function "+" (L : Big_Integer) return Big_Integer with Pre => Is_Valid (L); function "-" (L : Big_Integer) return Big_Integer with Pre => Is_Valid (L); function "abs" (L : Big_Integer) return Big_Integer with Pre => Is_Valid (L); function "+" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "-" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "*" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "/" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "mod" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "rem" (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function "**" (L : Big_Integer; R : Natural) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function Min (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function Max (L, R : Big_Integer) return Big_Integer with Pre => Is_Valid (L) and Is_Valid (R); function Greatest_Common_Divisor (L, R : 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; **************************************************************** From: Randy Brukardt Sent: Tuesday, January 14, 2020 4:39 PM I think that solution was a case of temporary mass insanity, as it doesn't make a lot of sense on review. In hindsight, I have no idea why we went with that - probably an attempt to split the baby. Anyway, a procedural note on this: the deadline for submissions for the upcoming meeting was noon yesterday. We set these deadlines early by the request of various ARG members who wanted a reasonable amount of time to review AIs before a meeting. Before we set that rule, certain people would do their homework on the plane to a meeting, leaving us discussing something no one had seen. I can sometimes take late submissions (as with yesterday, when I ended up with a lengthy afternoon dental appointment), but I need to be given a heads-up before the deadline that they are coming so I can avoid repeating work. As such, this submission won't be processed until after tomorrow's meeting, and won't be discussed unless we somehow magically get through all of the AIs on the agenda (very unlikely in three hours). Ideally, submissions that aren't ready by the deadline should be held until after the meeting so as to not distract people with things that aren't immediately relevant and/or having it get lost as it may disappear into the volume of one's inbox by the time the meeting is over. **************************************************************** From: Steve Baird Sent: Tuesday, January 14, 2020 4:59 PM > As such, this submission won't be processed until after tomorrow's > meeting, and won't be discussed unless we somehow magically get > through all of the AIs on the agenda (very unlikely in three hours). Right - this wasn't intended to be discussed this meeting (unless, as you described, we run out of other topics). Arno and I discussed this at a meeting on Monday morning (the end of the meeting coincided with the noon deadline) and I encouraged him to send the message without making any heroic efforts to meet any deadline. He was prompt enough that it looked like a near miss in an attempt to meet the deadline; it wasn't. I know, you aren't used to dealing with messages coming in *earlier* than expected. **************************************************************** From: Randy Brukardt Sent: Tuesday, January 14, 2020 5:15 PM Ideally, nothing would be sent in the dead period between the deadline and the meeting, as we don't want to be putting effort into non-agenda items before the meeting (particularly items that cause lengthy discussions), and it is easy to forget about such items after the meeting. Since I have to process it, that isn't a problem for me, I guess, but it likely is for everyone else (based on the typical result that if there isn't a response to a posting in 24 hours, there almost never is one). Such a dead period isn't really enforceable, but it seems preferable for everyone to follow it. **************************************************************** From: Randy Brukardt Sent: Monday, February 10, 2020 11:35 PM I'm trying to organize this for an AI, and it seems underspecified and underjustified... > 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. > > For Ada users: having to deal with two different type (a type and a > subtype) and having to choose which one is relevant is a real burden > and can actually lead to the wrong choice, only caught late at > runtime, and makes reading and understand the API much harder. There's a big difference between "two types" and "a type and a subtype", in that the possibilities of the first are not necessarily comparable, while the second is just a set and a subset of values. IMHO, subtypes are necessary in any decent-sized API, at a minimum to meet the DRY (Don't Repeat Yourself) principle. Still, the naming of the current proposal is likely to be confusing (the type should definitely be Big_Integer). In my experience, one declares objects (including components) with the least restrictive type (typically the base type), and parameters with a more restrictive subtype. That pretty much requires multiple subtypes (note that is pretty much the only way in Ada 95/2005 code to add any contract conditions to a subprogram specification). > For SPARK users: having two different types makes generating provable > formulas much harder and not direct. Since we anticipate SPARK users > to be "big users" of "big integers", not having a straightforward and > optimal mapping is really not suitable. This I don't understand, could you explain further? I would expect that a subtype would make analyzing a value of a type easier, since it necessarily restricts the set of values that are possible. And it has no other effect so it shouldn't make anything harder. I tend to start introducing subtypes when something appears in my code more than 2 or 3 times; giving something a name rather that duplicating it all over seems to be classic DRY. I wouldn't expect introducing short-hands to make problems for SPARK or any other Ada-aware tool. To take an example of what I typically find in my code, here's a tiny piece of the declarations from the web site log analyzer: type User_Counts is range 0 .. 1_000_000; NO_USER : constant User_Counts := 0; subtype User_Indices is User_Counts range 1 .. User_Counts'Last; Objects typically are declared with type User_Counts (with the exception of a few local temporaries) and most everything else is declared with User_Indices (including most parameters). Many types I declare end up with this or a similar structure, as there often is a need to separate an uninitialized/unknown value from the known values. I see that with access types (null exclusions mainly can be applied to parameters; components usually have to have the possibility of being null in order to deal with error cases and with piece-meal construction). It's not unusual for the unknown/uninitialized value to be represented by the result of a function call like Is_Valid. (That's especially likely for private types.) With predicates, one would prefer to write a subtype with a predicate rather than to duplicate a check 30-some times in preconditions. This is precisely what the original specification was doing. Pretty much every new specification (standard and in user code) has opportunities to take some advantage of this pattern (it's even recommended in the predicate examples in the Ada 2012 RM + Corrigendum 1, see 3.2.4(41-51/4)). > Proposed change: use a single type for Big_Integer and Big_Real and > remove all the Optional_Big_* types. Instead state that reading an > uninitialized > Big_* variable is a bounded error, similar to all scalar types, and > add a precondition to each subprogram in the Big_Integers/Big_Reals > packages ensuring that all possible uses of these objects is properly > checked, except for the Is_Valid function itself, which is marked > Intrinsic so that it's 'Access cannot be taken. > > See the below for the proposed API for Big_Integers. A similar change > is proposed for Big_Reals which has been successfully implemented and > used at AdaCore. The wording changes that go with this are missing. As such I don't know precisely what is intended. In particular, I do not understand how this Bounded Error is supposed to work or why we need it. I'd also like some justification for marking Is_Valid Intrinsic, since one expects this package to be written in Ada. I don't see any reason that taking 'Access of Is_Valid would be a problem (nor do I see any reason to do it, but that's a different issue). Is_Valid probably should be marked to have no side-effects (that is, with Global => null), but Intrinsic doesn't by itself have that effect. > type Big_Integer is private > with Integer_Literal => From_String, > Put_Image => Put_Image; There should be some Default_Initial_Condition here; Ada package specifications are often used as patterns by Ada users and thus should represent best practices. Uninitialized objects, OTOH, are a necessary evil in the case of existing language-defined types, but are just evil otherwise. I don't think that specifying Default_Initial_Condition => not Is_Valid (Big_Integer), has any significant performance or correctness impacts (and it should make it easier for SPARK by giving any such objects a known state). > with Ada.Streams; ... > procedure Put_Image > (Stream : not null access Ada.Streams.Root_Stream_Type'Class; > Arg : Big_Integer) > with Pre => Is_Valid (Arg); Put_Image doesn't use Streams anymore, we changed it to using a text buffer (AI12-0315-1). This should be: procedure Put_Image (Buffer : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class; Arg : Big_Integer) with Pre => Is_Valid (Arg); > function "+" (L : Big_Integer) return Big_Integer > with Pre => Is_Valid (L); This precondition changes the exception raised from Constraint_Error to Assertion_Error. The exception raised might not matter to SPARK, but for Ada it should be either Constraint_Error or Program_Error. (That is the case for the "regular" integers as well, if you're really trying to match that behavior.) I think it would be better to be Program_Error (use of an invalid value), but 13.9.1(9) allows either. In any case, the exception needs to be reflected in this precondition and all of the others as well: function "+" (L : Big_Integer) return Big_Integer with Pre => (if Is_Valid (L) then raise Program_Error); ****************************************************************