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

Differences between 1.6 and version 1.7
Log of other versions for file ai12s/ai12-0187-1.txt

--- ai12s/ai12-0187-1.txt	2016/12/29 00:53:24	1.6
+++ ai12s/ai12-0187-1.txt	2017/04/06 02:38:59	1.7
@@ -1,4 +1,4 @@
-!standard 7.3.3(0)                                    16-12-28  AI12-0187-1/03
+!standard 7.3.3(0)                                    17-04-05  AI12-0187-1/04
 !standard 13.1.1(4/3)
 !class Amendment 16-06-02
 !status work item 16-06-02
@@ -200,12 +200,20 @@
 replacing aspect Stable_Properties with aspect Stable_Properties'Class
 in the above definition.
 
+The *explicit* specific postcondition expression for a subprogram S is the
+expression directly specified for S with the Post aspect. Similarly, the
+*explicit* specific postcondition expression for a subprogram S is the
+expression directly specified for S with the Post'Class aspect. 
+
 For every primitive subprogram S of a type T that is not a stable property
-function of T, the actual specific postcondition of S includes expressions of
-the form F(P) = F(P)'Old, all /and/ed with each other and any explicit specific
-postcondition, where F is each stable property function of S for type T that
-does not occur in the explicit specific postcondition of S, and P is each
-parameter of S that has type T.
+function of T, the specific postcondition expression of S is modified to
+include expressions of the form F(P) = F(P)'Old, all /and/ed with each other
+and any explicit specific postcondition expression, where F is each stable
+property function of S for type T that does not occur in the explicit
+specific postcondition expression of S, and P is each parameter of S that
+has type T. The resulting specific postcondition expression of S is used
+in place of the explicit specific postcondition expression of S Redundant[
+when interpreting the meaning of the postcondition as defined in 6.1.1].
 
    AARM Ramification: There is one F(P) = F(P)'Old subexpression for every
    combination of stable expression function of type T and parameter of type T.
@@ -215,15 +223,20 @@
 
    The resulting specific postcondition is evaluated as described in 6.1.1.
    One hopes that compilers can be smart enough to prove that many of these
-   postconditions cannot fail, but that is not required here.
+   added postcondition subexpressions cannot fail, but that is not required
+   here.
    End AARM Ramification.
 
 For every primitive subprogram S of a type T that is not a stable property
-function of T, the actual class-wide postcondition of S includes expressions
-of the form F(P) = F(P)'Old, all /and/ed with each other and any explicit 
-class-wide postcondition, where F is each class-wide stable property function
-of S for type T that does not occur in any class-wide postcondition that
-applies to S, and P is each parameter of S that has type T.
+function of T, the class-wide postcondition expression of S is modified to
+include expressions of the form F(P) = F(P)'Old, all /and/ed with each other
+and any explicit class-wide postcondition expression, where F is each
+class-wide stable property function of S for type T that does not occur in
+any class-wide postcondition expression that applies to S, and P is each
+parameter of S that has type T. The resulting class-wide postcondition
+expression of S is used in place of the explicit class-wide postcondition
+expression of S Redundant[when interpreting the meaning of the postcondition
+as defined in 6.1.1].
 
    AARM Reason: We suppress stable property expressions if the property
    function appears in the explicit class-wide postcondition, or in any
@@ -266,11 +279,11 @@
 (2) I considered allowing more parameters on a property function, so long as
 they can be specified by literals or global objects. However, that made the
 rules more complex without much benefit, since a user can always wrap a
-function that has too many parameters in an expression function. The parameters
-have to be global or literal so that the property function can appear in the
-postcondition of every primitive routine of the type; they can't depend on
-a parameter of the routine as that would insist that every operation has a
-second, identical parameter.
+function that has too many parameters in an expression function. The extra
+parameters have to be global or literal so that the property function can
+appear in the postcondition of every primitive routine of the type; they can't
+depend on a parameter of the routine as that would insist that every operation
+has a second, identical parameter.
 
 (3) I thought about restricting the result types of property functions to
 elementary types. Since the semantics of 'Old are well-defined for nonlimited
@@ -483,3 +496,128 @@
 [Following was version /03 of the AI - Editor.]
 
 ****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, December 28, 2016  6:42 PM
+
+Looks pretty good.  There are some places where I might suggests tweaks to the
+wording to improve clarity.  My biggest concern is probably the relatively
+informal definition of "actual postcondition."  There seems to be some pretty
+significant hand-waving going on there. ;-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, December 29, 2016  6:08 PM
+
+I fully expect "tweaks to the wording", but it's a bit of a disappointment to
+only find out that they're needed without anything more specific.
+
+I discussed the need for "hand-waving" in item (9) of the discussion. 6.1.1 is
+a jar of wiggly worms which for the moment has the lid on. Removing the lid
+seems like a bad idea, since I have no trouble finding many things in that
+wording that are inconsistent. (At the risk of loosening the lid that I'd
+rather leave in place, two examples are the use of "associated expression"
+in 6.1.1(18/5) while all other wording uses some form of "applies"; and the
+inconsistent use of "postcondition" and "postcondition expression" in the
+wording.)
+
+As such, what is going on is going to require some hand-waving, since the
+model is that we're adding stuff to the specific (or class-wide) postcondition
+(expression??).
+
+We could get quite specific and write the rules based on the (specific or
+class-wide) postcondition expression, but I'm not sure that helps much other
+than adding verbiage (especially as then it is necessary to define "explicit
+(specific or class-wide) postcondition expression" in order to avoid a
+circular definition):
+
+   The *explicit* specific postcondition expression for a subprogram S is the
+   expression directly specified for S with the Post aspect. Similarly, the
+   *explicit* specific postcondition expression for a subprogram S is the
+   expression directly specified for S with the Post'Class aspect. 
+
+   For every primitive subprogram S of a type T that is not a stable property
+   function of T, the specific postcondition expression of S is modified to
+   include expressions of the form F(P) = F(P)'Old, all /and/ed with each other
+   and any explicit specific postcondition expression, where F is each stable
+   property function of S for type T that does not occur in the explicit
+   specific postcondition expression of S, and P is each parameter of S that
+   has type T. The resulting specific postcondition expression of S is used
+   in place of the explicit specific postcondition expression of S Redundant[
+   when interpreting the meaning of the postcondition as defined in 6.1.1].
+
+[The last redundant part is already in an AARM note, perhaps it should stay
+only there??]
+
+And similarly for the class-wide version:
+
+   For every primitive subprogram S of a type T that is not a stable property
+   function of T, the class-wide postcondition expression of S is modified to
+   include expressions of the form F(P) = F(P)'Old, all /and/ed with each other
+   and any explicit class-wide postcondition expression, where F is each
+   class-wide stable property function of S for type T that does not occur in
+   any class-wide postcondition expression that applies to S, and P is each
+   parameter of S that has type T. The resulting class-wide postcondition
+   expression of S is used in place of the explicit class-wide postcondition
+   expression of S Redundant[when interpreting the meaning of the postcondition
+   as defined in 6.1.1].
+
+Is this the sort of thing you meant? Or was there some other problem??
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, December 29, 2016  11:12 PM
+
+> I fully expect "tweaks to the wording", but it's a bit of a 
+> disappointment to only find out that they're needed without anything more
+> specific.
+
+I will provide more precise suggestions later, but right now I am occupied
+with many year-end duties.
+
+> ...
+> Is this the sort of thing you meant? Or was there some other problem??
+
+Yes, something along the lines you suggested in this reply would definitely
+help me, at least, feel better about the proposal.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, December 29, 2016  11:53 PM
+
+> I will provide more precise suggestions later, but right now I am 
+> occupied with many year-end duties.
+
+So was I, the main one making sure that I exhausted my 2016 ARG budget.
+Having just successfully accomplished that task, I'll have to wait until
+next week to apply these changes to the draft.
+
+Happy New Year to all!!!
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, April 5, 2017  9:38 PM
+
+> I will provide more precise suggestions later, but right now 
+> I am occupied with many year-end duties.
+
+I wonder if "later" has arrived yet. I'd hope that you're done with your
+year-end duties by now. ;-) [Hopefully, the quarter-end duties, too.]
+
+>> ...
+>> Is this the sort of thing you meant? Or was there some other problem??
+>
+>Yes, something along the lines you suggested in this reply would definitely
+>help me, at least, feel better about the proposal.
+
+I've just applied and posted a revised version of the AI with these changes
+made.
+
+(I'll note that I promised to do that "next week" on Dec 29, so you're not
+the only one who can put off things indefinitely. ;-)
+
+***************************************************************

Questions? Ask the ACAA Technical Agent