CVS difference for ai05s/ai05-0145-2.txt
--- ai05s/ai05-0145-2.txt 2009/11/03 05:55:42 1.1
+++ ai05s/ai05-0145-2.txt 2009/11/03 05:59:07 1.2
@@ -1,4 +1,4 @@
-!standard 11.5 (00) 09-06-12 AI05-0145-2/01
+!standard 11.5 (00) 09-11-02 AI05-0145-2/02
!standard 11.4.1 (10)
!class amendment 09-06-12
!status work item 09-06-12
@@ -9,13 +9,12 @@
!summary
-To augment the basic "assert" pragma capability in Ada 2005,
-we propose a notation for specifying pre- and post-conditions for subprograms,
-including null and abstract operations on interfaces, and subprograms
-and entries of synchronized types.
+To augment the basic "assert" pragma capability in Ada 2005, we propose
+to allow the specification of pre/postconditions for subprograms
+and entries.
-The notation uses the notion of "aspect specification" used for
-other representation aspects and for type invariants.
+We presume the use of the "aspect_specification" syntax defined in
+AI05-0183-1.
!problem
@@ -40,141 +39,166 @@
!proposal
-The following aspects are defined for subprograms and entries:
- Pre, Post, Inherited_Pre, Inherited_Post.
+Using the aspect_specification syntax, we propose to allow the
+specification of pre/postconditions for subprograms and entries.
+The aspects Pre and Post are used for this purpose. In addition, for
+primitive subprograms of tagged types, the aspects Pre'Class and
+Post'Class are also available. These aspects are inherited by the
+corresponding primitive subprogram of types descended from the original
+tagged type. When multiple preconditions apply to a subprogram, they are
+"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
+satisfied).
-The syntax of subprogram and entry declarations is modified as follows:
+!wording
+
+
+Modify 3.9.3(1.1/2):
+
+ abstract_subprogram_declaration :=
+ subprogram_specification IS ABSTRACT
+ [aspect_specification];
+
+Modify 6.1(2/2):
subprogram_declaration ::=
[overriding_indicator]
- subprogram_specification;
- [aspect_specification]
+ subprogram_specification
+ [aspect_specification]
- abstract_subprogram_declaration :=
- subprogram_specification IS ABSTRACT;
- [aspect_specification];
+Modify 6.7(2/2):
null_procedure_declaration ::=
- procedure_specification IS NULL;
- [aspect_specification];
+ procedure_specification IS NULL
+ [aspect_specification];
+
+Modify 9.5.2(2/2):
entry_declaration ::=
[overriding_indicator]
- ENTRY defining_identifier [(discrete_subtype_definition)] parameter_profile;
- [aspect_specification];
+ ENTRY defining_identifier [(discrete_subtype_definition)] parameter_profile
+ [aspect_specification];
- aspect_specification ::=
- with aspect_mark => boolean_expression {,aspect_mark => boolean-expression};
+Add a new section:
-We say that a Pre aspect, a Post aspect, an Inherited_Pre aspect, an Inherited_Pro
-aspect, specify respectively a Precondition, a Postcondition, an Inherited_Precondition
-or an Inherited_Postcondition of the subprogram or entry.
-
-At most one occurrence of each aspect is allowed for a subprogram or entry.
-declaration. For an Inherited_Precondition or Inherited_Postcondition,
-the subprogram must be a dispatching subprogram.
-The boolean expression is defined within the context of the
-specification of the operation so that the formal parameter names
-(and the entry family index) are directly visible.
-
-The names in the boolean_expression of a Precondition or Postcondtion
-are resolved not at the point of the declaration, but rather at the
-freezing point of the operation.
-
-For a Postcondition on a function, the attribute "Result" is defined
-on the subprogram name, yielding the value returned by the function.
-For a Postcondition on a procedure, the attribute "Old"
-is defined on each of the IN OUT nonlimited
-formal parameters, yielding the value of the formal parameter
-at the beginning of the execution of the procedure.
-
-If an Inherited_Precondition or Inherited_Postcondition is specified
-for a primitive subprogram, then it also applies to all its overridings.
-By contrast, Pre/Post aspects may be also be applied to non-primitive
-subprograms, and are not inherited. For abstract subprograms, only
-Inherited_Pre/Postconditions are meaningful.
-
-For an Inherited_Precondition or Inherited_Postcondition, if a formal
-parameter name corresponding to a controlling operand of the subprogram
-appears in the boolean expression, it is view-converted to the associated
-class-wide type, implying that dispatching is performed if calls on primitive
-functions occur in the expression. All other formal parameter names
-appearing within the boolean expression of a pre or post aspect
-have the type specified in the subprogram's parameter profile.
-
-If the assertion policy in effect at the point of a subprogram or entry
-declaration that includes an aspect specification
-is "Check," then upon a call on the specified subprogram or entry, after
-evaluating the actual parameters and making the parameter associations,
-the check associated with the aspect is performed.
-This consists of the evaluation of the boolean expression, If the expression
-is False, then Ada.Assertions.Assertion_Error is raised..
-It is not specified whether any check for elaboration of the subprogram
-body is performed before or after the precondition check.
-
-If multiple Preconditions apply to the same subprogram (through
-inheritance of Inherited_Pre aspects), then only if all of the boolean
-expressions evaluate to False, is Assertion_Error raised; an
-implementation-defined message is associated with the exception occurrence
-in this case. If any one of them evaluates to True, the subprogram
-call proceeds normally. The order in which multiple precondition pragmas are
-checked is not specified, and if one of them evaluates to True, it is
-not specified whether the others are checked.
-
-If the assertion policy in effect at the point of a Post aspect specification
-is "Check," then upon successful return from a call on the specified
-subprogram (as opposed to a return due to the propagation of an exception),
-and prior to copying back any by-copy [IN] OUT parameters, the check
-associated with the postcondition pragma is performed.
-This consists of evaluating the boolean expression, and if
-false, raising Ada.Assertions.Assertion_Error,.
-It is not specified whether the exception, if any, is raised at the point
-of the return statement or after leaving the subprogram. (I.e. it is not
-specified whether the exception can be handled within the subprogram)
-
-If multiple postcondition checks apply to the same subprogram, then
-Assertion_Error is raised if any of them evaluates to False;
-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 [IN] OUT parameters are performed before or after the postcondition checks.
-
-For a dispatching call or a call via an access-to-subprogram, the
-precondition/postconditions that apply to the call are determined by
-the subprogram actually invoked. Note that for a dispatching call, if there
-is an Inherited_Precondition that applies to the subprogram named
-in the call, then the rules for checking preconditions ensure that so
-long as this Inherited_Precondition is satisfied, the overall precondition
-check will succeed (because if any precondition evaluates to True, the
-call proceeds normally).
-
-Assertion Policy
-
-If the assertion policy at the point of a Pre/Post aspect specification
-is "Check" then the semantics are as described above. If the assertion
-If the assertion policy at the point of the specification is
-"Ignore" then the aspect has no effect.
-
-!wording
+ 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.*
+
+ 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.
+
+ 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 converted to T'Class. Similarly, a name that
+ denotes a formal access parameter of type access-to-T is converted to
+ access-to-T'Class. Finally, if the subprogram is a function returning
+ T or access T, the Result attribute is converted to 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.]
+
+ Legality Rules
+
+ The Pre or Post aspect shall not be specified for an abstract
+ subprogram. [Redundant: Only the Pre'Class and Post'Class aspects may
+ be specified for such a subprogram.]
+
+ Static Semantics
+
+ If a Pre'Class or Post'Class aspect is specified for a primitive
+ subprogram of a tagged type T, then the associated precondition
+ expression also applies to the corresponding primitive subprogram of
+ each descendant of T.
+
+ 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 consists of 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
+ 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
+ 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.
+
+ 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 IN OUT or 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 IN OUT or 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. [Redundant: 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. [Redundant: 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.
+
+ [Redundant: 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.]
!discussion
-This is based on AI05-145-1. The Pre/Post aspects are specified using the
-syntax introduced for AI-0146. There is no message associated with
-the failure of an aspect check: it was deemed that these aspects are intended
-for verification, and that for debugging purposes the Assert pragma is
+This is based on AI05-145-1. The Pre/Post aspects are specified using
+the aspect_specification syntax defined in AI05-0183-1. There is no
+message associated with the failure of a precondition or postcondition
+check: it was deemed that these annotations are intended for
+verification, and that for debugging purposes the Assert pragma is
sufficient.
-The new version preserves the flexibility of the previous one concerning the
-point at which the aspect is checked: either callee or caller can perform the
-check, and the failure or a postcondition may be (but need not be) handled in
-the faulty caller itself.
-
-These aspects can be specified for protected operations and for protected and
-task entries. It appears necessary that preconditions on tasks entries be
-evaluated by the caller, because their failure should take place before the
-rendezvous is attempted.
+The new version preserves the flexibility of the previous one concerning
+the point at which the aspect is checked: either callee or caller can
+perform the check, except for indirect calls, where a wrapper will be
+required if the caller normally performs the checks. Note however that
+the callee cannot handle the Assertion_Error, as there seems no reason
+to allow that degree of implementation dependence.
+
+These aspects can be specified for protected operations and for
+protected and task entries. It appears necessary that preconditions on
+entries be evaluated by the caller, because their failure should take
+place before the caller is suspended waiting on the entry queue. In the
+case of an entry that implements a primitive subprogram, the
+preconditions would have to be checked by the "wrapper" prior to calling
+the entry. We allow the precondition check to be performed inside or
+outside the protected action associated with a protected subprogram
+call.
!example
Questions? Ask the ACAA Technical Agent