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

Differences between 1.11 and version 1.12
Log of other versions for file ai12s/ai12-0208-1.txt

--- 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