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