CVS difference for ais/ai-00288.txt

Differences between 1.3 and version 1.4
Log of other versions for file ais/ai-00288.txt

--- ais/ai-00288.txt	2003/01/24 04:14:27	1.3
+++ ais/ai-00288.txt	2004/03/02 03:33:51	1.4
@@ -1,17 +1,16 @@
-!standard 11.5 (00)                                02-03-08  AI95-00288/01
+!standard 11.5 (00)                                04-02-29  AI95-00288/02
 !standard 11.4.1 (10)
 !class amendment 02-02-05
 !status work item 02-02-05
 !status received 02-02-05
 !priority Medium
 !difficulty Medium
-!subject Pre/Postconditions and Invariants
+!subject Pre- and Postconditions
 
 !summary
 
 To augment the basic "assert" pragma capability proposed in AI-00286,
-we propose pragmas for specifying pre/post conditions for subprograms,
-and invariants for packages and types.
+we propose pragmas for specifying pre and post conditions for subprograms.
 
 The semantics for these pragmas are defined in terms of the
 Assertion_Error exception used by the Assert pragma and the
@@ -19,48 +18,42 @@
 
 !problem
 
-A number of programming paradigms include the heavy use of
-pre/post conditions on subprograms and/or the use of invariants
-associated with types or modules (i.e. packages).
-Having a basic standardized "Assert" pragma supports this
-approach to some degree, but generally requires that the
-Assert pragmas actually be inserted inside the bodies of
-the associated code.  It would be much more appropriate if
-these pre/post conditions and invariants appeared on the
-specification of the subprograms, types, and packages rather
-than buried in the body, as it really represents part
-of the contract.  In particular, one wants any implementation
-of a given package spec to conform to all of the pre/post conditions
-and invariants specified, in the same way one wants any implementation
+A number of programming paradigms include the heavy use of pre/post
+conditions on subprograms. Having a basic standardized "Assert" pragma
+supports this approach to some degree, but generally requires that the
+Assert pragmas actually be inserted inside the bodies of the associated
+code. It would be much more appropriate if these pre/post conditions
+appeared on the specification of the subprograms rather than buried in the
+body, as it really represents part of the contract. In particular, one
+wants any implementation of a given package spec to conform to all of the
+pre/post conditions specified, in the same way one wants any implementation
 of a package to conform to the constraints of the parameter and result
 subtypes of the visible subprograms of the package.
 
-Effectively, pre/post conditions and invariants may be considered
-as generalized, user-definable constraints.  They have the same power
-to define more accurately the "contract" between the user and
-implementor of a package, and to thereby catch errors in usage
-or implementation earlier in the development cycle.  They also can
-provide valuable documentation of the intended semantics of an abstraction.
+Effectively, pre/post conditions may be considered as generalized,
+user-definable constraints. They have the same power to define more
+accurately the "contract" between the user and implementor of a package,
+and to thereby catch errors in usage or implementation earlier in the
+development cycle. They also can provide valuable documentation of the
+intended semantics of an abstraction.
 
 !proposal
 
-Preconditions and Postconditions:
+The pragmas Pre_Assert, Classwide_Pre_Assert, Post_Assert,
+and Classwide_Post_Assert have the following form:
 
-The pragmas Precondition, Classwide_Precondition, Postcondition,
-and Classwide_Postcondition have the following form:
-
-   pragma Precondition(subprogram_local_name,
+   pragma Pre_Assert(subprogram_local_name,
      boolean_expression [, [Message =>] string_expression]);
-   pragma Classwide_Precondition(dispatching_subprogram_local_name,
+   pragma Classwide_Pre_Assert(dispatching_subprogram_local_name,
      boolean_expression [, [Message =>] string_expression]);
 
-   pragma Postcondition(subprogram_local_name,
+   pragma Post_Assert(subprogram_local_name,
      boolean_expression [, [Message =>] string_expression]);
-   pragma Classwide_Postcondition(dispatching_subprogram_local_name,
+   pragma Classwide_Post_Assert(dispatching_subprogram_local_name,
      boolean_expression [, [Message =>] string_expression]);
 
 The (dispatching_)subprogram_name must name the immediately preceding
-subprogram.  For Classwide_Precondition and Classwide_Postcondition,
+subprogram. For Classwide_Pre_Assert and Classwide_Post_Assert,
 the subprogram must be a dispatching subprogram.
 The boolean expression is defined within the context of the
 subprogram specification so that the formal parameter names are
@@ -69,20 +62,20 @@
 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 "Incoming"
-is defined on each of the IN OUT elementary
+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 a Classwide_Precondition or Classwide_Postcondition pragma is specified
+If a Classwide_Pre_Assert or Classwide_Post_Assert pragma is specified
 for a primitive subprogram, then it also applies to all overridings
-of the primitive.  By contrast, Precondition/Postcondition
+of the primitive. By contrast, Pre_Assert/Post_Assert
 pragmas may be applied to non-primitive subprograms, and are not inherited.
 
-For a Classwide_Precondition or Classwide_Postcondition, if a formal
+For a Classwide_Pre_Assert or Classwide_Post_Assert, 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
+functions occur in the expression. All other formal parameter names
 appearing within the boolean expression of a precondition or postcondition
 pragma have the type specified in the subprogram's parameter profile.
 
@@ -92,16 +85,16 @@
 the check associated with the precondition pragma is performed.
 This consists of the evaluation of the boolean expression,
 and if False, a raise of the Ada.Assertions.Assertion_Error exception, with
-the specified Message if provided.  It is not specified whether
+the specified Message if provided. It is not specified whether
 any check for elaboration of the subprogram body is performed
 before or after the precondition check.
 
 If multiple precondition pragmas apply to the same subprogram (through
-inheritance of Classwide_Preconditions), then only if all of the boolean
+inheritance of Classwide_Pre_Asserts), 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
+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.
 
@@ -112,9 +105,9 @@
 associated with the postcondition pragma is performed.
 This consists of evaluating the boolean expression, and if
 false, raising Ada.Assertions.Assertion_Error, with
-the specified Message, if any.  It is not specified whether the
+the specified Message, if any. 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
+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
@@ -123,121 +116,38 @@
 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.
 If more than one evaluates to False, it is not specified which
-message is provided with the exception occurrence.  It is not specified
+message is provided with the exception occurrence. 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 a Classwide_Precondition that applies to the subprogram named
+the subprogram actually invoked. Note that for a dispatching call, if there
+is a Classwide_Pre_Assert that applies to the subprogram named
 in the call, then the rules for checking preconditions ensure that so
-long as this Classwide_Precondition is satisfied, the overall precondition
+long as this Classwide_Pre_Assert is satisfied, the overall precondition
 check will succeed (because if any precondition evaluates to True, the
 call proceeds normally).
 
-Invariants
-
-The pragmas Package_Invariant, Type_Invariant, and Classwide_Type_Invariant
-have the following form:
-
-    pragma Package_Invariant(package_local_name,
-      boolean_function_name [, [Message =>] string_expression]);
-
-    pragma Type_Invariant(first_subtype_local_name,
-      boolean_function_name [, [Message =>] string_expression]);
-
-    pragma Classwide_Type_Invariant(tagged_first_subtype_local_name,
-      boolean_function_name [, [Message =>] string_expression]);
-
-The package_local_name for Package_Invariant must denote the immediately
-enclosing program unit, which must be a package.  The boolean_function_name
-for Package_Invariant must denote a parameterless function declared
-within the specified package that has a Standard.Boolean result.
-
-The first_subtype_local_name for Type_Invariant must denote a first
-subtype declared in the immediately enclosing region, which must be
-a package.  The boolean_function_name for Type_Invariant must denote
-a function with one parameter of the type denoted by the
-first_subtype_local_name, and a Standard.Boolean result.
-
-The tagged_first_subtype_local_name for Classwide_Type_Invariant must
-denote a tagged first subtype declared in the immediately enclosing
-region, which must be a package.  The boolean_function_name for
-Classwide_Type_Invariant must denote a dispatching function with one
-parameter of the type denoted by the tagged_first_subtype_local_name,
-and a Standard.Boolean result.
-
-If the assertion policy at the point of an invariant pragma is
-"Check," then the associated check is performed at the following
-places:
-
-* For a Package_Invariant pragma, upon return
-  from a call on any procedure defined within the declarative
-  region of the package that is visible outside the package,
-  a call is performed on the specified parameterless function;
-  also, immediately after completing elaboration of the package.
-
-* For a Type_Invariant pragma, upon return from a call
-  on any procedure that
-    - has one or more [IN] OUT parameters of the specified type,
-    - is defined within the immediate scope of the type, and
-    - is visible outside the immediate scope of the type,
-  one call is performed on the specified boolean function for each such
-  [IN] OUT parameter.  Similarly, after evaluation of a function call or
-  type converstion that returns the specified type, a call is performed
-  on the specified boolean function passing the result.  Finally, after
-  default initialization of an object of the type, a call is performed
-  on the specified boolean function passing the default-initialized object.
-
-* For a Classwide_Type_Invariant pragma, upon return from a call
-  on any procedure that
-    - has one or more [IN] OUT parameters of a type within the
-      derivation class of the specified type,
-    - is defined within the immediate scope of the type, and
-    - is visible outside the immediate scope of the type,
-  one call is performed on the specified boolean dispatching function
-  for each such [IN] OUT parameter.  The parameter is view-converted
-  to the class-wide type prior to the call, ensuring that the call is
-  a dispatching call.  Similarly, after evaluation of a function call or
-  type conversion that returns a type within the derivation class, a
-  dispatching call is performed on the specified boolean function passing
-  the result.  Finally, after default initialization of an object of a
-  type within the derivation class, a dispatching call is performed on
-  the specified boolean function passing the default-initialized object.
-
-If any of these calls return False, Ada.Assertions.Assertion_Error is
-raised, with the specified Message if any.
-
-The invariant checks are performed prior to copying back
-any by-copy [IN] OUT parameters.  However, it is not specified
-whether any constraint checks associated with the copying back are
-performed before or after the invariant checks.  If there are any
-postconditions associated with the procedure, it is not specified
-whether these checks are performed before, after, or interleaved with
-the invariant checks.
-
 Assertion Policy
 
 If the assertion policy at the point of a pre/postcondition or invariant
-pragma is "Check" then the semantics are as described above.  If the assertion
-If the assertion policy at the point of the pragma is
-"Ignore" then the pragma has no effect.  If the assertion
-policy at the point of the pragma is "Assume_True" then if the check
-associated with the pragma would have failed, execution is erroneous.
+pragma is "Check" then the semantics are as described above. If the assertion
 If the assertion policy at the point of the pragma is
-"Evaluate_And_Assume_True" then the evaluations necessary to do the
-check are performed, but if the check fails, execution is erroneous.
+"Ignore" then the pragma has no effect.
 
 !wording
 
 
 !discussion
 
-Pre/Postcondition Pragmas
+NOTE: We have changed the names of the pragmas to use the terms
+Pre_Assert and Post_Assert rather than Precondition and Postcondition,
+because of objections that precondition/postcondition are terms
+reserved for static analysis.
 
 The precondition and postcondition pragmas provide a basic capability
-for defining the "contract" of a subprogram.  Implementation of the
+for defining the "contract" of a subprogram. Implementation of the
 corresponding checks is tied to the assertion policy in effect
 at the point of the pragma (rather than at the call or the body),
 to ensure that the checks may be inserted either
@@ -249,7 +159,7 @@
 between conditions that apply to a particular version of a dispatching
 operation from those that apply to all overridings of the operation.
 This distinction is missing in Eiffel, and represents a weakness (in
-our view) of their model.  The "Classwide_" version necessarily must be
+our view) of their model. The "Classwide_" version necessarily must be
 less specific, i.e. less "tight," and hence cannot catch as many bugs
 by itself as the combination of an inherited condition and a condition
 specific to a particular body.
@@ -257,10 +167,10 @@
 A possible implementation model for the pre/postcondition checks is as follows.
 Existing calls on Proc or Func are replaced with calls on "Proc_with_check"
 or "Func_with_check" if the assertion policy is "Check" at the point of the
-pragmas.  The "_with_check" subprograms are defined as follows:
+pragmas. The "_with_check" subprograms are defined as follows:
 
     procedure Proc_with_check(
-      ...; Elementary_Inout_Param1 : in out Inout_Type1; ...) is
+      ...; Nonlimited_Inout_Param1 : in out Inout_Type1; ...) is
         -- Procedure with pre/post conditions inserted
 
     begin
@@ -274,14 +184,15 @@
         end if;
 
         declare
-            -- save incoming values of elementary in/out params
-            Elementary_Inout_Param1'Incoming : constant Inout_Type1 :=
-              Elementary_Inout_Param1;
-            ... -- other elementary in/out params
+            -- save incoming values of nonlimited in/out params
+            -- referenced in postconditions
+            Nonlimited_Inout_Param1'Incoming : constant Inout_Type1 :=
+              Nonlimited_Inout_Param1;
+            ... -- other nonlimited in/out params referenced in postconditions
         begin
 
             -- Call the "real" procedure
-            Proc(..., Elementary_Inout_Param1, ...);
+            Proc(..., Nonlimited_Inout_Param1, ...);
 
             -- check postcondition(s)
             if not <postcondition_bool_expr> then
@@ -325,16 +236,16 @@
 
 Note we don't specify exactly where the precondition checks occur relative
 to elaboration checks so these checks may be done "outside" or "inside"
-the subprogram as is most convenient.  Similarly, we don't specify whether
+the subprogram as is most convenient. Similarly, we don't specify whether
 the postcondition checks are performed at the point of the return statement,
 or at the end of the call, to provide implementation flexibility.
 This means that in some implementations Assertion_Error could be caught inside
-the subprogram.  This does not seem to be a serious concern, and the
+the subprogram. This does not seem to be a serious concern, and the
 implementation flexibility seems valuable.
 
 However, we do require that dynamically bound calls, i.e. calls via
 an access-to-subprogram dereference or a dispatching call, have the
-applicable pre/postconditions checked.  This implies that in most
+applicable pre/postconditions checked. This implies that in most
 situations, the pre/postcondition checks will need to be implemented by
 adding code "inside" the subprogram, or by having two separate
 subprograms (as above), one which is used by dynamically bound
@@ -342,93 +253,38 @@
 the checks are performed by the caller.
 
 To do the best job of optimizing precondition checks, one would
-generally want to expand them at the point of the call.  On the
+generally want to expand them at the point of the call. On the
 other hand, postcondition checks are probably most optimizable when
-done inside the subprogram.  This would imply that under heavy
+done inside the subprogram. This would imply that under heavy
 optimization, it might be useful to have a separate version for
 dynamically bound calls that performs the precondition checks "inside,"
 while statically bound calls would perform the check at the
 point of call, and then call the version that bypasses the precondition
-check if the checks succeed.  This is similar to an approach that
+check if the checks succeed. This is similar to an approach that
 some compilers use for access-before-elaboration checking.
 Having postcondition checks inside seems preferable in any case.
 
 We don't provide a pre/postcondition pragma for access-to-subprogram types.
-That might be useful in some cases.  However, the pre/postcondition
+That might be useful in some cases. However, the pre/postcondition
 would (presumably) only apply on calls through a value of the type,
 which means additional implementation complexities, in that the
 checking code could not be inserted inside the designated subprograms,
 and would have to be at the call point, or in some kind of "indirection"
-stub.  I suppose one approach would be to interpret a pre/postcondition
+stub. I suppose one approach would be to interpret a pre/postcondition
 pragma on an access-to-subprogram type as a requirement for statically
 matching (or provably "stronger"?) pre/postconditions on all subprograms
-to be designated by values of the type.  That begins to get into
+to be designated by values of the type. That begins to get into
 theorem proving, etc., which might be appropriate for a separate tool,
 but is beyond what we want the "average" Ada compiler to have to do. ;-)
 
-Invariant Pragmas
-
-We have provided both type oriented and package oriented "invariant"
-pragmas.  This reflects the fact that some abstractions are
-for abstract data types, while others are for abstract state machines.
-We only enforce the package-oriented invariant on return from visible
-procedures of the package.  If a visible function has side-effects,
-the implementor may want to insert an explicit postcondition on
-the function, or a Assert pragma inside.
-
-For type invariants, we apply them on [IN] OUT parameters of
-procedures after the call, and on the result of functions and conversions.
-
-The invariants are defined by referring to a boolean function.
-The more general boolean_expression allowed in the other assertion-like
-pragmas was not used because it was unlikely that the invariant
-could be defined in terms of visible entities, and there was
-no obvious way to refer to the particular instance of the type
-for the Type_Invariant pragma.  In addition, given that the
-checks may be performed at the call point, space economization argues
-for bundling the invariant into a callable subprogram.  The programmer
-might as well do this bundling him/herself.
-
-Invariant checks apply to all calls on (relevant) procedures
-declared in the visible part of the package, even those within the package.
-This allows the checks to be performed inside the procedures rather than
-at the call point, and makes the invariant pragmas equivalent to a series of
-postcondition pragmas. We considered making invariant checks apply only to
-calls from outside the package, but this appeared to complicate the
-implementation and description with little additional benefit.
-
-The invariant checks are performed as postcondition checks to ensure
-that violations are caught as soon as possible. Presumably the invariants
-could also be enforced as preconditions, but those checks would in
-general be redundant, and the failures would be harder to track down
-since the call that actually created the problem would be harder
-to identify.
-
-We do not specify any inheritance of invariant pragmas.  It might
-make sense for a type invariant to be inherited by its descendants.
-However, in that case, a separate Inheritable_Type_Invariant would
-probably be appropriate, based on the same argument given above
-relating to inheritable pre/postcondition pragmas.
-Presumably we would allow these pragmas in generic packages, with the
-obvious semantics in the instance.
-
-We have not specified whether the invariants apply to any
-inherited primitive subprograms that are implicitly declared
-within the package containing the pragma.  We have not specified
-whether invariants apply to dynamically-bound calls, which might
-reach subprograms that are not declared in the visible part of
-the package.  Clearly these issues need to be resolved.
-
 Assertion Policy
 
-We have used the Assertion_Policy pragma defined in AI-00286,
-with the same options and interpretation.  It might make sense
-to define separate pragmas, such as Precondition_Policy,
-Postcondition_Policy, and Invariant_Policy, but with the
-same set of identifiers.  This would give the programmer more
-control.  On the other hand, typically either the programmer wants
-full debugging, or full speed.  Intermediate points seem relatively
-rare.
+We have used the Assertion_Policy pragma defined in AI-00286, with the same
+options and interpretation. It might make sense to define separate
+pragmas, such as Pre_Assert_Policy, and Post_Assert_Policy but with the
+same set of identifiers. This would give the programmer more control. On
+the other hand, typically either the programmer wants full debugging, or
+full speed. Intermediate points seem relatively rare.
 
 !example
 
@@ -441,15 +297,15 @@
     function Is_Full(S : in Stack) return Boolean;
 
     procedure Push(S : in out Stack; I : in Item);
-    pragma Precondition(Push, not Is_Full(S));
-    pragma Postcondition(Push, not Is_Empty(S));
+    pragma Pre_Assert(Push, not Is_Full(S));
+    pragma Post_Assert(Push, not Is_Empty(S));
 
     procedure Pop(S : in out Stack; I : out Item);
-    pragma Precondition(Pop, not Is_Empty(S));
-    pragma Postcondition(Pop, not Is_Full(S));
+    pragma Pre_Assert(Pop, not Is_Empty(S));
+    pragma Post_Assert(Pop, not Is_Full(S));
 
     function Top(S : in Stack) return Item;
-    pragma Precondition(Top, not Is_Empty(S));
+    pragma Pre_Assert(Top, not Is_Empty(S));
 
     function Is_Valid_Stack(S : in Stack) return Boolean;
     pragma Type_Invariant(Stack, Is_Valid_Stack);

Questions? Ask the ACAA Technical Agent