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

Differences between 1.3 and version 1.4
Log of other versions for file ai12s/ai12-0366-1.txt

--- ai12s/ai12-0366-1.txt	2020/04/28 02:33:02	1.3
+++ ai12s/ai12-0366-1.txt	2020/05/02 03:43:14	1.4
@@ -1,6 +1,8 @@
-!standard A.5.6(0)                                   20-04-26  AI12-0366-1/02
+!standard A.5.6(0)                                   20-04-30  AI12-0366-1/03
 !standard A.5.7(0)
 !class Amendment 20-02-10
+!status Amendment 1-2012 20-04-30
+!status ARG Approved 13-1-0  20-04-30
 !status work item 20-02-10
 !status received 20-01-02
 !priority Low
@@ -54,8 +56,7 @@
 
 with Ada.Strings.Text_Buffers;
 package Ada.Numerics.Big_Numbers.Big_Integers
-  with Preelaborate, Nonblocking, Global => null
-is
+  with Preelaborate, Nonblocking, Global => null is
    type Big_Integer is private
      with Integer_Literal => From_String,
           Put_Image => Put_Image;
@@ -63,7 +64,7 @@
    function Is_Valid (Arg : Big_Integer) return Boolean
      with Convention => Intrinsic;
 
-   subtype Valid_Big_Integer is Integer
+   subtype Valid_Big_Integer is Big_Integer
      with Dynamic_Predicate => Is_Valid (Valid_Big_Integer),
           Predicate_Failure => raise Program_Error;
 
@@ -80,11 +81,11 @@
    function To_Big_Integer (Arg : Integer) return Valid_Big_Integer;
 
    subtype Big_Positive is Big_Integer
-     with Dynamic_Predicate => Big_Positive > 0,
+     with Dyanmic_Predicate => (if Is_Valid (Big_Positive) then Big_Positive > 0),
           Predicate_Failure => raise Constraint_Error;
 
    subtype Big_Natural is Big_Integer
-     with Dynamic_Predicate => Big_Natural >= 0,
+     with Dyanmic_Predicate => (if Is_Valid (Big_Natural) then Big_Natural => 0),
           Predicate_Failure => raise Constraint_Error;
 
    function In_Range (Arg, Low, High : Big_Integer) return Boolean is
@@ -204,11 +205,11 @@
 
 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.Numerics.Big_Numbers.Big_Integers; 
+   use all type Big_Integers.Big_Integer;
 with Ada.Strings.Text_Buffers;
 package Ada.Numerics.Big_Numbers.Big_Reals
-  with Preelaborate, Nonblocking, Global => null
-is
+  with Preelaborate, Nonblocking, Global => null is
    type Big_Real is private with
      Real_Literal => From_String,
      Put_Image    => Put_Image;
@@ -225,13 +226,20 @@
                   or else raise Constraint_Error;
 
    function Numerator
-     (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer;
+     (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer
+     with Post => (if Arg = 0.0 then NumeratoríResult = 0);
 
+   AARM Reason: The postcondition of Numerator cannot be complete as it cannot
+   mention Denominator. Since the postcondition of Denominator uses Numerator,
+   we would get an infinite mutual recursion of both postconditions are enabled.
+   The postcondition of Denominator serves as the postcondition for Numerator
+   as well unless Arg = 0.0.
+
    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;
+       (if Arg = 0.0 then DenominatoríResult = 1 
+        else Greatest_Common_Divisor (Numerator (Arg), Denominator'Result) = 1);
 
    function To_Big_Real
      (Arg : Big_Integers.Big_Integer)
@@ -369,12 +377,9 @@
 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.
+We changed the postcondition of Denominator to say something about the result
+when Arg = 0.0, and added a postcondition to Numerator to do the same.
 
 !ASIS
 

Questions? Ask the ACAA Technical Agent