CVS difference for ai12s/ai12-0366-1.txt
--- 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