CVS difference for ai05s/ai05-0145-2.txt
--- ai05s/ai05-0145-2.txt 2010/01/22 01:27:48 1.6
+++ ai05s/ai05-0145-2.txt 2010/02/04 07:11:43 1.7
@@ -1,4 +1,4 @@
-!standard 13.3.2 (00) 09-12-28 AI05-0145-2/03
+!standard 13.3.2 (00) 10-02-03 AI05-0145-2/04
!class amendment 09-06-12
!status work item 10-01-14
!status ARG Approved 11-0-1 09-11-07
@@ -53,6 +53,12 @@
postconditions must be satisfied for the overall postcondition is
satisfied).
+Within a postcondition, Prefix'Old denotes the value of Prefix as it was
+at the beginning of the execution of the subprogram.
+
+Within a postcondition on a function F, F'Result denotes the value returned
+by the function.
+
!wording
@@ -70,21 +76,13 @@
Name Resolution
The expected type for a precondition or postcondition expression is
- the predefined type Boolean. Within a postcondition expression of a
- function, the attribute Result is defined for the function, yielding
- the value returned by the function. Within a postcondition expression
- of a subprogram or entry with at least one IN OUT formal parameter of a
- nonlimited type, the attribute Old is defined for each such formal
- parameter, yielding the value of the formal parameter at the beginning
- of the execution of the subprogram or entry.
+ the predefined type Boolean.
Within the expression for a Pre'Class or Post'Class aspect for a primitive
subprogram of a tagged type T, a name that denotes a formal parameter of type
T is interpreted as having type T'Class. Similarly, a name that denotes a
formal access parameter of type access-to-T is interpreted as having type
- access-to-T'Class. Finally, if the subprogram is a function returning T or
- access T, the Result attribute is interpreted as having type T'Class or
- access-to-T'Class, respectively. [Redundant: This ensures the expression is
+ access-to-T'Class. [Redundant: This ensures the expression is
well-defined for a primitive subprogram of a type descended from T.]
Legality Rules
@@ -100,6 +98,65 @@
applies to the corresponding primitive subprogram of each descendant
of T.
+ For a prefix X that is of a nonlimited type,
+ the following attribute is defined:
+
+ X'Old Denotes the value of X at the beginning of the execution
+ of the subprogram or entry. In particular, if X'Old appears in
+ a postcondition, and postconditions are enabled, a constant
+ is implicitly declared at the beginning of the subprogram or
+ entry, of the type of X, initialized to X. The value of X'Old
+ in the postcondition is the value of this constant.
+ These implicit declarations occur in an arbitrary order.
+
+ Use of this attribute is allowed only within a postcondition.
+
+AARM annotation:
+
+ The prefix X can be anything nonlimited that obeys the syntax for
+ prefix. Useful cases are: the name of a formal parameter of mode
+ '[in] out', the name of a global variable updated by the subprogram,
+ a function call passing those as parameters, a subcomponent
+ of those things, etc.
+
+ A qualified expression can be used to make an arbitrary expression into a
+ valid prefix, so T'(X + Y)'Old is legal, even though (X + Y)'Old
+ is not. The value being saved here is the sum of X and Y.
+
+ Note that F(X)'Old and F(X'Old) are not necessarily equal.
+ The former calls F(X) and saves that value for later use during
+ the postcondition. The latter saves the value of X,
+ and during the postcondition, passes that saved value
+ to F. In most cases, the former is what one wants.
+
+ If X has controlled parts, adjustment and finalization are implied
+ by the implicit constant declaration.
+
+ If postconditions are disabled, we want the compiler to avoid any
+ overhead associated with saving 'Old values.
+
+ 'Old makes no sense for limited types, because its implementation
+ involves copying, in general. Well, it might make semantic sense to
+ allow build-in-place, but it's not worth the trouble.
+
+end AARM annotation.
+
+ For a prefix F that denotes a function, the following attribute is
+ defined:
+
+ F'Result
+ Denotes the result of the function.
+ The type of this attribute is that of the function result
+ except within a Post'Class postcondition for a function
+ with a controlling result or with a controlling access result.
+ In the former case, the type of the attribute is T'Class,
+ where T is the function result type. In the latter case,
+ the type of the attribute is an anonymous access type whose
+ designated type is T'Class, where T is the designated type
+ of the function result type. Use of this attribute is allowed
+ only within a postcondition for F.
+
+
Dynamic Semantics
If one or more precondition expressions apply to a subprogram or
@@ -625,5 +682,262 @@
executed: Count(Obj) could not be zero yet.
(Yes, I know this is a lousy Postcondition -- I said it was in extreme cases...)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, February 3, 2010 11:24 AM
+
+Here's an Old message from Randy that nicely illustrates the issue with 'Old
+that I mentioned at the last phone meeting. There seems to be an
+assumption/requirement in ai05-0145-1 (the other variant of this AI) that 'Old
+applies only to formal parameters. That makes no sense to me, and Randy's
+message illustrates why.
+
+[Bob repeats the previous message.]
+
+It seems clear (to me) that you want "Count(Obj)'Old" above, instead of
+"Count(Obj'Old)". The semantics of "Count(Obj)'Old" are to evaluate
+"Count(Obj)", and save that value. We are not saving the value of Obj in that
+case, so Adjust or whatever is not called.
+
+Of course, you are allowed to say "Count(Obj'Old)", and then you'd get a saved
+copy of Obj -- with Adjust, Finalize, whatever. So don't do that, if it's not
+what you want.
+
+My homework is to write up the wording for 'Old and 'Result. To be included in
+AI05-0145-2, right? My plan is that the prefix of 'Old can be any non-limited
+object.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, February 3, 2010 2:33 PM
+
+AI05-0145-2/03 Pre- and Postconditions
+
+Here is my homework to write the !wording for the 'Old and 'Result attributes.
+
+Add to the end of the !proposal:
+
+Within a postcondition, Prefix'Old denotes the value of Prefix as it was at the
+beginning of the execution of the subprogram.
+
+Within a postcondition on a function F, F'Result denotes the value returned by
+the function.
+
+
+For reference, the current (version 03 of this AI) Name Resolution section under
+!wording says:
+
+ The expected type for a precondition or postcondition expression is
+ the predefined type Boolean. Within a postcondition expression of a
+ function, the attribute Result is defined for the function, yielding
+ the value returned by the function. Within a postcondition expression
+ of a subprogram or entry with at least one IN OUT formal parameter of a
+ nonlimited type, the attribute Old is defined for each such formal
+ parameter, yielding the value of the formal parameter at the beginning
+ of the execution of the subprogram or entry.
+
+ Within the expression for a Pre'Class or Post'Class aspect for a primitive
+ subprogram of a tagged type T, a name that denotes a formal parameter of type
+ T is interpreted as having type T'Class. Similarly, a name that denotes a
+ formal access parameter of type access-to-T is interpreted as having type
+ access-to-T'Class. Finally, if the subprogram is a function returning T or
+ access T, the Result attribute is interpreted as having type T'Class or
+ access-to-T'Class, respectively. [Redundant: This ensures the expression is
+ well-defined for a primitive subprogram of a type descended from T.]
+
+Replace with:
+
+ The expected type for a precondition or postcondition expression is
+ the predefined type Boolean.
+
+ For a prefix X that is of a nonlimited type,
+ the following attribute is defined.
+ This attribute is allowed only within a postcondition.
+
+ X'Old Denotes the value of X at the beginning of the execution
+ of the subprogram or entry. In particular, if X'Old appears in
+ a postcondition, and postconditions are enabled, a constant
+ is implicitly declared at the beginning of the subprogram or
+ entry, of the type of X, initialized to X. The value of X'Old
+ in the postcondition is the value of this constant.
+ These implicit declarations occur in an arbitrary order.
+
+AARM annotation:
+
+ The prefix X can be anything nonlimited that obeys the syntax for
+ prefix. Useful cases are: the name of a formal parameter of mode
+ '[in] out', the name of a global variable updated by the subprogram,
+ a function call passing those as parameters, a subcomponent
+ of those things, etc.
+
+ A qualified expression can be used to make an arbitrary expression into a
+ valid prefix, so T'(X + Y)'Old is legal, even though (X + Y)'Old
+ is not. The value being saved here is the sum of X and Y.
+
+ Note that F(X)'Old and F(X'Old) are not necessarily equal.
+ The former calls F(X) and saves that value for later use during
+ the postcondition. The latter saves the value of X,
+ and during the postcondition, passes that saved value
+ to F. In most cases, the former is what one wants.
+
+ If X has controlled parts, adjustment and finalization are implied
+ by the implicit constant declaration.
+
+ If postconditions are disabled, we want the compiler to avoid any
+ overhead associated with saving 'Old values.
+
+ 'Old makes no sense for limited types, because its implementation
+ involves copying, in general. Well, it might make semantic sense to
+ allow build-in-place, but it's not worth the trouble.
+
+end AARM annotation.
+
+ For a prefix F that denotes a function, the following attribute is
+ defined. This attribute is allowed only within a postcondition for F.
+
+ F'Result Denotes the result of the function.
+ The type of this attribute is normally that of the function
+ result. The only exception is that within Post'Class
+ of a primitive function of type T, F'Result is of type
+ T'Class.
+
+ Within the expression for a Pre'Class or Post'Class aspect for a primitive
+ subprogram of a tagged type T, a name that denotes a formal parameter of type
+ T is interpreted as having type T'Class. Similarly, a name that denotes a
+ formal access parameter of type access-to-T is interpreted as having type
+ access-to-T'Class. Finally, if the subprogram is a function returning T,
+ the Result attribute is interpreted as having type T'Class.
+ [Redundant: This ensures the expression is well-defined for a primitive
+ subprogram of a type descended from T.]
+
+[Note from Bob: The last para above used to talk about "access T"
+for function results, but I don't see why, since those aren't primitive in T.
+So I deleted that part.]
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, February 3, 2010 2:47 PM
+
+> [Note from Bob: The last para above used to talk about "access T"
+> for function results, but I don't see why, since those aren't
+> primitive in T. So I deleted that part.]
+
+Huh? They surely are primitive for T: see 3.2.3(6) (which says that the
+primitives are the ones that "operate on the type") and 3.2.3(1/2) which defines
+"operate on the type" to include access result types. So a function like:
+
+ function Foobar (A : Natural) return access T;
+
+is surely primitive on T. That's good, because such a function is
+tag-indeterminate and can be dispatched on!
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, February 3, 2010 5:13 PM
+
+Right. I somehow got stuck in Ada 95.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, February 3, 2010 3:09 PM
+
+> My plan is that the prefix of 'Old can be any non-limited object.
+
+That's what we implement now, and I think that is the desirable choice.
+
+In general it is always possible to write preconditions and postconditions with
+unacceptable side effects. We don't prevent that, and the ability to be able to
+do this is not a legitimate argument against a particular class of usage.
+
+****************************************************************
+
+From: Gary Dismukes
+Sent: Wednesday, February 3, 2010 3:53 PM
+
+> For a prefix F that denotes a function, the following attribute is
+> defined. This attribute is allowed only within a postcondition for F.
+>
+> F'Result Denotes the result of the function.
+> The type of this attribute is normally that of the function
+> result. The only exception is that within Post'Class
+> of a primitive function of type T, F'Result is of type
+> T'Class.
+
+I think the phrase "primitive function of type T" should be changed to something
+like "primitive function of a tagged type T whose result is T", since the
+primitive function might have some other result type.
+
+> Within the expression for a Pre'Class or Post'Class aspect for a primitive
+> subprogram of a tagged type T, a name that denotes a formal parameter of type
+> T is interpreted as having type T'Class. Similarly, a name that denotes a
+> formal access parameter of type access-to-T is interpreted as having type
+> access-to-T'Class. Finally, if the subprogram is a function returning T,
+> the Result attribute is interpreted as having type T'Class.
+> [Redundant: This ensures the expression is well-defined for a primitive
+> subprogram of a type descended from T.]
+
+The earlier paragraph says that F'Result *is* of type T'Class, whereas here
+you're saying that it's interpreted as having type T'Class. I think the former
+is all that is needed, right? Also, for consistency, should the earlier
+description of X'Old include the stuff related to Pre'Class/Post'Class? (Of
+course, that would make most of the above paragraph redundant.)
+
+> [Note from Bob: The last para above used to talk about "access T"
+> for function results, but I don't see why, since those aren't
+> primitive in T. So I deleted that part.]
+
+But those *are* primitive for type T (as also noted by Randy).
+
+****************************************************************
+
+From: Steve Baird
+Sent: Wednesday, February 3, 2010 4:46 PM
+
+> I think the phrase "primitive function of type T" should be changed to
+> something like "primitive function of a tagged type T whose result is
+> T", since the primitive function might have some other result type.
+
+This seems like a good place to somehow use the terms "controlling result" and
+"controlling access result".
+
+Maybe
+
+ F'Result Denotes the result of the function.
+ The type of this attribute is that of the function result
+ except within a Post'Class postcondition for a function
+ with a controlling result or with a controlling access result.
+ In the former case, the type of the attribute is T'Class,
+ where T is the function result type. In the latter case,
+ the type of the attribute is an anonymous access type whose
+ designated type is T'Class, where T is the designated type
+ of the function result type.
+
+Do we need to define the accessibility level of this access type?
+Do we need to say anything more to ensure that F'Result does not make a copy
+(except in the elementary case)?
+
+> The earlier paragraph says that F'Result *is* of type T'Class, whereas
+> here you're saying that it's interpreted as having type T'Class. I
+> think the former is all that is needed, right?
+
+I agree.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, February 3, 2010 10:48 PM
+
+For the record, I made these changes and also put the attributes in the Static
+Semantics section where they belong in the posted AI.
+
+[I also reorganized the wording to be consistent with E'Caller,
+the only other attribute that I could think of that is only
+allowed in a single contexts.]
****************************************************************
Questions? Ask the ACAA Technical Agent