CVS difference for ai05s/ai05-0145-2.txt
--- ai05s/ai05-0145-2.txt 2010/02/23 07:31:06 1.8
+++ ai05s/ai05-0145-2.txt 2010/04/13 02:13:07 1.9
@@ -1,5 +1,6 @@
-!standard 13.3.2 (00) 10-02-04 AI05-0145-2/05
+!standard 13.3.2 (00) 10-04-12 AI05-0145-2/06
!class amendment 09-06-12
+!status ARG Approved 11-0-0 10-02-28
!status work item 10-01-14
!status ARG Approved 11-0-1 09-11-07
!status work item 09-06-12
@@ -50,7 +51,7 @@
"or"ed together (that is, if any of the preconditions is satisfied, the
overall precondition is satisfied). When multiple postconditions apply
to a subprogram, they are "and"ed together (that is, all of the
-postconditions must be satisfied for the overall postcondition is
+postconditions must be satisfied for the overall postcondition to be
satisfied).
Within a postcondition, Prefix'Old denotes the value of Prefix as it was
@@ -85,6 +86,11 @@
access-to-T'Class. [Redundant: This ensures the expression is
well-defined for a primitive subprogram of a type descended from T.]
+ For an attribute_reference with attribute_designator Old, if the attribute
+ reference has an expected type or shall resolve to a given type, the same
+ applies to the prefix; otherwise the prefix shall be resolved independent
+ of context.
+
Legality Rules
The Pre or Post aspect shall not be specified for an abstract
@@ -102,13 +108,13 @@
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 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.
+ of the subprogram or entry. For each X'Old in a postcondition
+ expression that is 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. The type of X'Old
+ is the type of X. These implicit
+ declarations occur in an arbitrary order.
Use of this attribute is allowed only within a postcondition
expression.
@@ -138,25 +144,25 @@
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.
+ involves copying. 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
+ For a prefix F that denotes a function declaration, the following attribute is
defined:
F'Result
- Denotes the result object of the function.
- The type of this attribute is that of the function result
- 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 expression for F.
+ Within a postcondition expression for function F, denotes
+ the result object of the function. The type of this attribute is that
+ of the function result except within a Post'Class postcondition
+ expression for a function with a controlling result or with a
+ controlling access result. For a controlling result, the type of the
+ attribute is T'Class, where T is the function result type. For a
+ controlling access result, 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 expression for F.
Dynamic Semantics
@@ -165,18 +171,18 @@
entry, and the Assertion_Policy in effect at the point of the
subprogram or entry declaration is Check, then upon a call of the
subprogram or entry, after evaluating any actual parameters, a
- precondition check is performed. This consists of the evaluation of
+ precondition check is performed. This begins with the evaluation of
the precondition expressions that apply to the subprogram or entry. If
- and only if all the precondition expressions evaluate to False, then
+ and only if all the precondition expressions evaluate to False,
Ada.Assertions.Assertion_Error is raised. The order of performing the
checks is not specified, and if any of the precondition expressions
evaluate to True, it is not specified whether the other precondition
- expressions are checked. It is not specified whether any check for
+ expressions are evaluated. It is not specified whether any check for
elaboration of the subprogram body is performed before or after the
precondition check. It is not specified whether in a call on a
protected operation, the check is performed before or after starting
- the protected action. For an entry call, the check is performed prior
- to checking whether the entry is open.
+ the protected action. For a task or protected entry call, the check is
+ performed prior to checking whether the entry is open.
If one or more postcondition expressions apply to a subprogram or
entry, and the Assertion_Policy in effect at the point of the
@@ -206,6 +212,24 @@
If the Assertion_Policy in effect at the point of a
subprogram or entry declaration is Ignore, then no precondition or
postcondition check is performed on a call on that subprogram or entry.
+ If the Assertion_Policy in effect at the point of a
+ subprogram or entry declaration is Check, then preconditions and
+ postconditions are considered to be *enabled* for that subprogram or
+ entry.
+
+ Bounded Errors
+
+ It is a bounded error to invoke a potentially blocking operation (see
+ 9.5.1) during the evaluation of a precondition or postcondition expression.
+ If the bounded error is detected, Program_Error is raised. If not detected,
+ execution proceeds normally, but if it is invoked within a protected action,
+ it might result in deadlock or a (nested) protected action.
+
+
+NOTE: A precondition is checked just before the call. If another task can
+change any value that the precondition expression depends on, the precondition
+may not hold within the subprogram or entry body.
+
!discussion
Questions? Ask the ACAA Technical Agent