CVS difference for ai05s/ai05-0145-2.txt

Differences between 1.8 and version 1.9
Log of other versions for file 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