CVS difference for ai05s/ai05-0145-2.txt
--- ai05s/ai05-0145-2.txt 2010/09/04 02:49:24 1.10
+++ ai05s/ai05-0145-2.txt 2010/10/19 00:38:38 1.11
@@ -1,4 +1,4 @@
-!standard 13.3.2 (00) 10-09-02 AI05-0145-2/07
+!standard 13.3.2 (00) 10-10-18 AI05-0145-2/09
!class amendment 09-06-12
!status Amendment 2012 10-09-02
!status ARG Approved 11-0-0 10-02-28
@@ -12,13 +12,9 @@
!summary
-To augment the basic "assert" pragma capability in Ada 2005, we propose
-to allow the specification of pre/postconditions for subprograms
-and entries.
+The basic assert pragma of Ada 2005 is augmented by the specification of
+pre/postconditions for subprograms and entries.
-We presume the use of the "aspect_specification" syntax defined in
-AI05-0183-1.
-
!problem
A number of programming paradigms include the heavy use of pre/post
@@ -42,8 +38,8 @@
!proposal
-Using the aspect_specification syntax, we propose to allow the
-specification of pre/postconditions for subprograms and entries.
+Using the aspect_specification syntax introduced in AI05-0183-1, 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
@@ -75,20 +71,20 @@
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
+ descendants; 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*.
+ descendants; it shall be specified by an expression, called a
+ *postcondition expression*.
Name Resolution Rules
The expected type for a precondition or postcondition expression is
- the predefined type Boolean.
+ any boolean type.
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
@@ -99,7 +95,7 @@
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
+ applies to the prefix; otherwise the prefix shall be resolved independently
of context.
Legality Rules
@@ -203,13 +199,13 @@
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
+ apply to the subprogram or entry. If any of 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.
+ one of them evaluates to False, it is not specified whether the other
+ postcondition expressions are evaluated. 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
@@ -249,9 +245,10 @@
This is based on the previous alternative AI05-0145-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.
+postcondition check; in the face of multiple pre/postcondition failures, it
+would be ambiguous which message to use, and furthermore, it was deemed that
+an implementation could provide automatically a message that indicated which
+pre/postcondition(s) failed, and that would be sufficient for debugging purposes.
The new version preserves the flexibility of the previous one concerning
the point at which the aspect is checked: either callee or caller can
@@ -368,7 +365,7 @@
@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
+ descendants; it shall be specified by an @fa<expression>, called a
@i<precondition expression>.>
@xhang<@xterm<Post>
@@ -377,24 +374,24 @@
@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>.>
+ descendants; it shall be specified by an @fa<expression>, called a
+ @i<postcondition expression>.>
@s8<@i<Name Resolution Rules>>
The expected type for a precondition or postcondition expression is
-the predefined type Boolean.
+any boolean type.
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
+formal access parameter of type access-to-@i<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
+applies to the @fa<prefix>; otherwise the @fa<prefix> shall be resolved independently
of context.
@s8<@i<Legality Rules>>
@@ -466,13 +463,13 @@
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
+apply to the subprogram or entry. If any of 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.
+one of them evaluates to False, it is not specified whether the other
+postcondition expressions are evaluated. 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
Questions? Ask the ACAA Technical Agent