--- ai12s/ai12-0366-1.txt 2020/05/16 04:39:24 1.7 +++ ai12s/ai12-0366-1.txt 2020/05/29 03:57:24 1.8 @@ -1770,3 +1770,88 @@ foisted on us by SPARK. **************************************************************** + +From: Christoph Grein +Sent: Tuesday, May 19, 2020 9:10 AM + +I'm being tenacious. + +In light of how many meanings to this list are posted on truely insignificant +themes (e.g. end record [id]), this theme must be of utmost importance if I +measure it inversely proportional to the number of posts. At least I feel a +bit like this. + +Is it really so absurd to request a complete post condition on Denominator? +Why should the condition be left open on Value 0? As has been stated, the +result of Denominator need not be what it is internally, i.e. GCD (costly) +is only called to compute the results of Numerator and Denominator. + +function Denominator (Arg : Big_Real) return Big_Positive +with Post => + (if Arg = 0.0 then Denominator'Result = 1) + or else + (Big_Integers.Greatest_Common_Divisor + (Numerator (Arg), Denominator'Result) = 1); + +And BTW: Shouldn't there be a related post condition on Numerator? + +**************************************************************** + +From: Jeff Cousins +Sent: Tuesday, May 19, 2020 10:11 AM + +Aren’t the latest proposals adequate?, i.e. to quote the latest ARG minutes: + +“ +Tucker didn’t change the postcondition of Denominator. Bob would like a +complete postcondition. + +(if Arg = 0.0 then Denominator’Result = 1 else + Greatest_Common_Divisor (Numerator (Arg), Denominator'Result) = 1); + + +Also, Post => (if Arg = 0.0 then Numerator’Result = 0) on Numerator. We can’t +mention Denominator here, as that would be recursive (since the Post of +Denominator calls Numerator). +“ + +**************************************************************** + +From: Bob Duff +Sent: Tuesday, May 19, 2020 10:41 AM + +> Is it really so absurd to request a complete post condition on +> Denominator? + +No. Of course it should be complete. + +> And BTW: Shouldn't there be a related post condition on Numerator? + +Well, I think that would lead to infinite mutual recursion. + +**************************************************************** + +From: Christoph Grein +Sent: Wednesday, May 20, 2020 5:23 AM + +>> And BTW: Shouldn't there be a related post condition on Numerator? +> Well, I think that would lead to infinite mutual recursion. + +Oh ah, of course. I guess a little remark on AARM would then be appropriate, +perhaps "To be honest". + +**************************************************************** + +From: Randy Brukardt +Sent: Thursday, May 28, 2020 10:21 PM + +Sigh. You should have waited for Draft 25. Under Numerator there is an AARM +note: + +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 if both postconditions are enabled. +The postcondition of Denominator serves as the postcondition for Numerator as +well unless Arg = 0.0. + +****************************************************************

Questions? Ask the ACAA Technical Agent