!standard 11.5 (00) 09-02-16 AI05-0145-1/02 !standard 11.4.1 (10) !class amendment 09-02-15 !status work item 09-02-15 !status received 09-02-15 !priority Medium !difficulty Medium !subject Pre- and Postconditions !summary To augment the basic "assert" pragma capability in Ada 2005, 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 Assertion_Policy configuration pragma. !problem 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 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 The pragmas Precondition, Inherited_Precondition, Postcondition, and Inherited_Postcondition have the following form: pragma Precondition(subprogram_local_name, [Check =>] boolean_expression [, [Message =>] string_expression]); pragma Inherited_Precondition(dispatching_subprogram_local_name, [Check =>] boolean_expression [, [Message =>] string_expression]); pragma Postcondition(subprogram_local_name, [Check =>] boolean_expression [, [Message =>] string_expression]); pragma Inherited_Postcondition(dispatching_subprogram_local_name, [Check =>] boolean_expression [, [Message =>] string_expression]); The (dispatching_)subprogram_name must name the immediately preceding subprogram. For Inherited_Precondition and Inherited_Postcondition, 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 directly visible. The names in the boolean_expression of a precondition or postcondition pragma are resolved not at the point of the pragma, but rather at the freezing point of the named subprogram, or at the end of the immediately enclosing visible part, whichever comes first. 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 pragma is specified for a primitive subprogram, then it also applies to all overridings of the primitive. By contrast, Precondition/Postcondition pragmas may be applied to non-primitive subprograms, and are not inherited. 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 precondition or postcondition pragma have the type specified in the subprogram's parameter profile. If the assertion policy in effect at the point of a precondition pragma is "Check," then upon a call on the specified subprogram, after evaluating the actual parameters and making the parameter associations, 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 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 Inherited_Preconditions), 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 postcondition pragma 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, with 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 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 message provided corresponds to one of the failing checks. 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 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 precondition or postcondition 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. !wording !discussion This is based on AI95-0288. The precondition and postcondition pragmas provide a basic capability 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 at the point of the call or inside the subprogram body, and both the caller and the callee "know" whether the check will be performed (which might affect optimization). We provide a separate "Inherited_" version of the pragmas to distinguish 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 "Inherited_" version necessarily must be less specific to the particular body (Inherited_Precondition must be more restrictive, and Inherited_Postcondition must be more lax), and hence cannot catch as many bugs by itself as the combination of an inherited condition and a condition specific to a particular body. We defer resolving the names in the boolean_expression because it is natural for preconditions or postconditions to refer to other subprograms declared in the same scope, and requiring that there be no forward references unduly restricts the expressions. 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: procedure Proc_with_check( ...; Nonlimited_Inout_Param1 : in out Inout_Type1; ...) is -- Procedure with pre/post conditions inserted begin -- Check precondition(s) if not and then not and then not ... then raise Ada.Assertions.Assertion_Error [with ]; end if; declare -- save Old values of nonlimited in/out params -- referenced in postconditions Nonlimited_Inout_Param1'Old : constant Inout_Type1 := Nonlimited_Inout_Param1; ... -- other nonlimited in/out params referenced in postconditions begin -- Call the "real" procedure Proc(..., Nonlimited_Inout_Param1, ...); -- check postcondition(s) if not then raise Ada.Assertions.Assertion_Error [with ]; end if; ... -- any other postconditions end; end Proc_with_check; function Func_with_check(...) return Result_Type is -- Function with pre/post conditions inserted begin -- Check precondition(s) if not and then not and then not ... then raise Ada.Assertions.Assertion_Error; -- or Ada.Exceptions.Raise_Exception(..., ) end if; declare -- Save result of calling the function (use "renames" -- so this works with limited-type return as well) Func'Result: Result_Type renames Func(...); begin -- Check postcondition(s) if not then raise Ada.Assertions.Assertion_Error; -- or Ada.Exceptions.Raise_Exception(..., ) end if; ... -- any other postconditions -- Now return to the caller return Func'Result; end; end Func_with_check; 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 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 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 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 calls which includes the check, and one which is used when 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 other hand, postcondition checks are probably most optimizable when 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 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 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 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 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. ;-) Assertion Policy We have used the Assertion_Policy pragma of Ada 2005, with the same options and interpretation. It might make sense to define separate pragmas, such as Precondition_Policy, and Postcondition_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. Inherited vs. Inheritable vs. Classwide vs. ... We considered other names for Inherited_Precondition and Inherited_Postcondition. The Ada 95 AI used "Classwide_Precondition." We also considered "Inheritable_Precondition", though that sounded a bit like a disease. In the end we went with what seemed the simplest name that conveyed the intent. !example generic type Item is private; package Stacks is type Stack is private; function Is_Empty(S : in Stack) return Boolean; 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)); procedure Pop(S : in out Stack; I : out Item); pragma Precondition(Pop, not Is_Empty(S)); pragma Postcondition(Pop, not Is_Full(S)); function Top(S : in Stack) return Item; pragma Precondition(Top, not Is_Empty(S)); function Is_Valid_Stack(S : in Stack) return Boolean; Stack_Error : exception; private -- whatever end Stacks; !ACATS test !appendix From: Tucker Taft Sent: Sunday, February 15, 2009 3:56 PM This is a resurrection of AI95-00288, on pre- and postconditions. It is virtually unchanged. The proposed pragma names are: pragma Precondition pragma Inherited_Precondition pragma Postcondition pragma Inherited_Postcondition These were discussed at some length at a meeting at AdaCore which took place on 12/2/2008, with Tucker Taft of SofCheck as guest. [This is version /01 of the AI - ED]. **************************************************************** From: Tucker Taft Sent: Sunday, February 15, 2009 4:27 PM I left out one important issue: The names in the boolean_expression of a precondition or postcondition pragma are resolved not at the point of the pragma, but rather at the freezing point of the named subprogram, or at the end of the immediately enclosing visible part, whichever comes first. and from the discussion: We defer resolving the names in the boolean_expression because it is natural for preconditions or postconditions to refer to other subprograms declared in the same scope, and requiring that there be no forward references unduly restricts the expressions. **************************************************************** From: Robert Dewar Sent: Sunday, February 15, 2009 5:01 PM I haven't studied the whole proposal carefully, but as far as I can tell, the Precondition/Postcondition part of it corresponds pretty much exactly to what has been implemented in GNAT, and used fairly extensively. >> A resurrection of AI95-00375 on type invariants will appear shortly. I look forward to that, we have always got stuck on invariants :-) ****************************************************************