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

--- ai05s/ai05-0145-2.txt	2010/04/13 02:13:07	1.9
+++ ai05s/ai05-0145-2.txt	2010/09/04 02:49:24	1.10
@@ -1,5 +1,6 @@
-!standard 13.3.2 (00)                                10-04-12  AI05-0145-2/06
+!standard 13.3.2 (00)                                10-09-02  AI05-0145-2/07
 !class amendment 09-06-12
+!status Amendment 2012 10-09-02
 !status ARG Approved  11-0-0  10-02-28
 !status work item 10-01-14
 !status ARG Approved 11-0-1  09-11-07
@@ -67,15 +68,25 @@
 
   13.3.2 Preconditions and Postconditions
 
-  Preconditions and postconditions may be specified for subprograms and
-  entries, using an aspect_specification for aspect Pre, Pre'Class,
-  Post, or Post'Class. The expression associated with a Pre or Pre'Class
-  aspect is called a *precondition expression*, and the expression
-  associated with a Post or Post'Class aspect is called a *postcondition
-  expression.*
+  For a subprogram or entry, the following language-defined aspects may
+  be specified with an aspect_specification:
+     Pre
+       This aspect specifies a precondition for a callable entity; it shall
+       be specified by an expression, called a *precondition expression*.
+     Pre'Class
+       This aspect specifies a precondition for a callable entity and its
+       decendants; it shall be specified by an expression, called a
+       *precondition expression*.
+     Post
+       This aspect specifies a postcondition for a callable entity; it shall
+       be specified by an expression, called a *postcondition expression*.
+     Post'Class
+       This aspect specifies a postcondition for a callable entity and its
+       decendants; it shall be specified by an expression, called a
+       *precondition expression*.
+       
+          Name Resolution Rules
 
-         Name Resolution Rules
-
   The expected type for a precondition or postcondition expression is
   the predefined type Boolean.
 
@@ -104,7 +115,7 @@
   applies to the corresponding primitive subprogram of each descendant
   of T.
 
-  For a prefix X that is of a nonlimited type,
+  For a prefix X that denotes an object of a nonlimited type,
   the following attribute is defined:
 
        X'Old    Denotes the value of X at the beginning of the execution
@@ -121,7 +132,7 @@
 
 AARM annotation:
 
-  The prefix X can be anything nonlimited that obeys the syntax for
+  The prefix X can be any nonlimited object 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
@@ -129,7 +140,9 @@
 
   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.
+  is not. The value being saved here is the sum of X and Y (a function
+  result is an object). Of course, in this case "+"(X, Y)'Old is also
+  legal, but the qualified expression is arguably more readable.
 
   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
@@ -341,8 +354,162 @@
 A call on Stk_Inst.Push would evaluate "not Is_Empty(S)" as its precondition
 expression (that being inherited from the interface).
 
+
+!corrigendum 13.3.2(0)
+
+@dinsc
+
+For a subprogram or entry, the following language-defined aspects may
+be specified with an @fa<aspect_specification>:
+
+@xhang<@xterm<Pre>
+  This aspect specifies a precondition for a callable entity; it shall
+  be specified by an @fa<expression>, called a @i<precondition expression>.>
+
+@xhang<@xterm<Pre'Class>
+  This aspect specifies a precondition for a callable entity and its
+  decendants; it shall be specified by an @fa<expression>, called a
+  @i<precondition expression>.>
+
+@xhang<@xterm<Post>
+  This aspect specifies a postcondition for a callable entity; it shall
+  be specified by an @fa<expression>, called a @i<postcondition expression>.>
+
+@xhang<@xterm<Post'Class>
+  This aspect specifies a postcondition for a callable entity and its
+  decendants; it shall be specified by an @fa<expression>, called a
+  @i<precondition expression>.>
+
+@s8<@i<Name Resolution Rules>>
+
+The expected type for a precondition or postcondition expression is
+the predefined type Boolean.
+
+Within the expression for a Pre'Class or Post'Class aspect for a primitive
+subprogram of a tagged type @i<T>, a name that denotes a formal parameter of type
+@i<T> is interpreted as having type @i<T>'Class. Similarly, a name that denotes a
+formal access parameter of type access-to-T is interpreted as having type
+access-to-@i<T>'Class. This ensures the expression is
+well-defined for a primitive subprogram of a type descended from @i<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 @fa<prefix>; otherwise the @fa<prefix> shall be resolved independent
+of context.
+
+@s8<@i<Legality Rules>>
+
+The Pre or Post aspect shall not be specified for an abstract
+subprogram. Only the Pre'Class and Post'Class aspects may
+be specified for such a subprogram.
+
+@s8<@i<Static Semantics>>
+
+If a Pre'Class or Post'Class aspect is specified for a primitive
+subprogram of a tagged type @i<T>, then the associated expression also
+applies to the corresponding primitive subprogram of each descendant
+of @i<T>.
+
+For a @fa<prefix> X that denotes an object of a nonlimited type,
+the following attribute is defined:
+
+@xhang<@xterm<X'Old>
+  Denotes the value of X at the beginning of the execution
+  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.>
+
+@xindent<Use of this attribute is allowed only within a postcondition
+  expression.>
+
+For a @fa<prefix> F that denotes a function declaration, the following attribute is
+defined:
+
+@xhang<@xterm<F'Result>
+   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 @i<T>'Class, where @i<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 @i<T>'Class, where @i<T> is the
+   designated type of the function result type. Use of this attribute
+   is allowed only within a postcondition expression for F.>
+
+@s8<@i<Dynamic Semantics>>
+
+If one or more precondition expressions apply to a subprogram or
+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 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,
+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 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 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
+subprogram or entry declaration is Check, then upon successful return
+from a call of the subprogram or entry, prior to copying back any
+by-copy @b<in out> or @b<out> parameters, a postcondition check is performed.
+This consists of the evaluation of the postcondition expressions that
+apply to the subprogram or entry. If any of the the postcondition
+expressions evaluate to False, then Ada.Assertions.Assertion_Error is
+raised. The order of performing the checks is not specified, and if
+one of them evaluates to False, it is not specified whether the others
+are checked. It is not specified whether any constraint checks
+associated with copying back @b<in out> or @b<out> parameters are performed
+before or after the postcondition check.
+
+If a precondition or postcondition check fails, the exception is
+raised at the point of the call. The exception cannot
+be handled inside the called subprogram.
+
+For a dispatching call or a call via an access-to-subprogram value,
+the precondition or postcondition check performed is determined by the
+subprogram actually invoked. Note that for a dispatching
+call, if there is a Pre'Class aspect that applies to the subprogram
+named in the call, then if the precondition expression for that aspect
+evaluates to True, the precondition check for the call will succeed.
+
+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 @i<enabled> for that subprogram or
+entry.
+
+@s8<@i<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.
+  
+@s9<NOTES@hr
+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.>
+
+
 !ACATS test
 
+Various C-Tests should be created to test these features.
 
 !appendix