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