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

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