CVS difference for ai05s/ai05-0145-2.txt
--- ai05s/ai05-0145-2.txt 2010/02/04 07:11:43 1.7
+++ ai05s/ai05-0145-2.txt 2010/02/23 07:31:06 1.8
@@ -1,4 +1,4 @@
-!standard 13.3.2 (00) 10-02-03 AI05-0145-2/04
+!standard 13.3.2 (00) 10-02-04 AI05-0145-2/05
!class amendment 09-06-12
!status work item 10-01-14
!status ARG Approved 11-0-1 09-11-07
@@ -73,7 +73,7 @@
associated with a Post or Post'Class aspect is called a *postcondition
expression.*
- Name Resolution
+ Name Resolution Rules
The expected type for a precondition or postcondition expression is
the predefined type Boolean.
@@ -103,13 +103,15 @@
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.
+ a postcondition expression, 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 expression is the value
+ of this constant. These implicit declarations occur in an
+ arbitrary order.
- Use of this attribute is allowed only within a postcondition.
+ Use of this attribute is allowed only within a postcondition
+ expression.
AARM annotation:
@@ -145,16 +147,16 @@
defined:
F'Result
- Denotes the result of the function.
+ Denotes the result object of the function.
The type of this attribute is that of the function result
- except within a Post'Class postcondition for a function
+ except within a Post'Class postcondition expression 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.
+ only within a postcondition expression for F.
Dynamic Semantics
@@ -518,13 +520,19 @@
Tucker Taft wrote:
> I essentially agree with Randy, as I wrote on 11/8/2009.
-
-I agree with Randy's conclusion, that the precondition should be checked before an entry call (after locking the lock), and not at the beginning of the entry body. I suppose it should also be checked on a requeue, right?
-The caller has to ensure that the precondition is true, and the caller can't be expected to know what goes on between enqueueing the call and starting the body.
-Yes, that could cause race conditions -- it's the responsibility of the protected type to deal with it (e.g. don't write preconditions that can change in that time).
+I agree with Randy's conclusion, that the precondition should be checked before
+an entry call (after locking the lock), and not at the beginning of the entry
+body. I suppose it should also be checked on a requeue, right? The caller has
+to ensure that the precondition is true, and the caller can't be expected to
+know what goes on between enqueueing the call and starting the body.
+
+Yes, that could cause race conditions -- it's the responsibility of the
+protected type to deal with it (e.g. don't write preconditions that can change
+in that time).
-But I don't entirely agree with Randy's reasoning -- Randy is overly pessimistic, as is his wont ;-), when he says:
+But I don't entirely agree with Randy's reasoning -- Randy is overly
+pessimistic, as is his wont ;-), when he says:
> The *only* way to be able to argue *anything* about Pre *anywhere* is
> to put "almost unreasonable restrictions" on the nature of Pre.
@@ -533,17 +541,23 @@
If there are no shared variables, then procedure P's precondition
is True at the start of P.
-
-(I'm assuming we have globals annotations.) A tool that knows that could be extremely useful, so long as its users understand that they must analyze any shared variables separately "by hand".
-Alternatively, one could come up with annotations that allow the proof tool (the compiler?) to know about shared variables.
-I should have suggested that before the deadline for new ideas -- at least part of my brain understood the issue, because such annotations exist in my hobby language.
-Too late -- but it could be an impl-def pragma or something.
+(I'm assuming we have globals annotations.) A tool that knows that could be
+extremely useful, so long as its users understand that they must analyze any
+shared variables separately "by hand".
+
+Alternatively, one could come up with annotations that allow the proof tool (the
+compiler?) to know about shared variables. I should have suggested that before
+the deadline for new ideas -- at least part of my brain understood the issue,
+because such annotations exist in my hobby language. Too late -- but it could be
+an impl-def pragma or something.
+
+Another alternative (which I don't like) would be for the tool to do
+whole-program analysis. I don't like it because it's slow. I also don't like
+it because it's not modular: I don't just want to prove that a procedure works
+in this particular program; I want to prove that it works, period, even if other
+parts of the program are modified.
-Another alternative (which I don't like) would be for the tool to do whole-program analysis. I don't like it because it's slow. I also don't like it because it's not modular: I don't just want to prove that a procedure works in this particular program;
I want to prove that it works, period, even if other parts of the program are modified.
-
-- Bob
-
P.S. Because you have to read the conversation backwards.
P.P.S. Why is top-posting evil?
@@ -941,3 +955,136 @@
allowed in a single contexts.]
****************************************************************
+
+From: Steve Baird
+Sent: Thursday, February 4, 2010 4:42 PM
+
+> F'Result Denotes the result of the function.
+> ... . 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?
+
+There was a request for an example to illustrate whatever issue it was that I
+had in mind when I asked this question.
+
+Consider
+
+ Type Root is tagged null record;
+
+ type Ref is access constant Root'Class;
+
+ function F (Ptr : Ref) return Boolean;
+
+ procedure Enclosing is
+
+ package Pkg is
+ type T is new Root with ... ;
+ function F (...) return access T
+ with Post'Class => F (Ref (F'Result));
+ end Pkg;
+ ...
+ begin ... end Enclosing;
+
+We want to be sure that the right RM wording exists to support rejecting this
+type conversion.
+
+4.6(24.17/3) requires that in this case
+ The accessibility level of the operand type shall not be
+ statically deeper than that of the target type, ...
+
+For this to make sense, the accessibility level of the operand type must be
+defined.
+
+I think this boils down to a question of whether 3.10/2(7/2) applies in this
+case:
+
+ An entity or view defined created by a declaration and created as part
+ of its elaboration has the same accessibility level as the innermost
+ enclosing master of the declaration except in the cases of renaming
+ and derived access types described below.
+
+I think we can decide that this rule does apply (don't spend too much time
+pondering that "created as part of its elaboration" clause) and that therefore
+the type conversion in the example is illegal and no action is required.
+
+Comments?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, February 4, 2010 4:58 PM
+
+...
+> Comments?
+
+The example would make a whole lot more sense if the two functions had different
+names. I briefly thought you were trying to illustrate a recursive Post
+expression.
+
+Which does beg the question: is a self-recursive Post expression allowed? (I
+suppose; the name of the function must not be hidden from all visibility or the
+attribute 'Result could never work.) If so, I presume it will eventually raise
+Storage_Error.
+
+i.e.
+
+ function F (Whatever : Natural) return Natural with
+ Post => F (Whatever'Old) = F'Result;
+
+Obviously this is a totally goofy postcondition, but it is also one that is true
+and someone might write by being too clever for their own good. A warning would
+be good, I guess.
+
+P.S. If you don't see the problem, recall that the call of F in Post also has a
+Postcondition, and that postcondition also calls F. The net effect is that the
+evaluation of postconditions will never terminate until the task runs out of
+stack space. That's irrespective of whatever the body of F does.
+
+P.P.S. None of this really has anything to do with Steve's example, but it's the
+sort of flight of fancy that us ARG members are known for. Gotta keep up the
+status quo on that. :-)
+
+****************************************************************
+
+From: Steve Baird
+Sent: Thursday, February 4, 2010 5:10 PM
+
+> The example would make a whole lot more sense if the two functions had
+> different names. I briefly thought you were trying to illustrate a
+> recursive Post expression.
+
+Good point. I didn't mean to give them the same name.
+
+[And recursive calls from within a post condition seem fine; the recursion might
+even bottom out and accomplish something useful.]
+
+****************************************************************
+
+From: Gary Dismukes
+Sent: Thursday, February 4, 2010 5:48 PM
+
+> ...
+> I think this boils down to a question of whether 3.10/2(7/2) applies
+> in this case:
+>
+> An entity or view defined created by a declaration and created as part
+> of its elaboration has the same accessibility level as the innermost
+> enclosing master of the declaration except in the cases of renaming
+> and derived access types described below.
+>
+> I think we can decide that this rule does apply (don't spend too much
+> time pondering that "created as part of its elaboration" clause) and
+> that therefore the type conversion in the example is illegal and no
+> action is required.
+>
+> Comments?
+
+Yes, I think that paragraph does apply. So no further action needed, I'd say.
+
+(At first I was thinking that the level had something to do with the point of
+calls, but that was confused. Accessibility is often that way...)
+
+****************************************************************
\ No newline at end of file
Questions? Ask the ACAA Technical Agent