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. 
+
+****************************************************************