6.1.1 Preconditions and Postconditions

Ramification: {AI12-0045-1} “Noninstance subprogram” excludes a subprogram that is an instance of a generic subprogram. In that case, the aspects should be specified on the generic subprogram. If preconditions or postconditions need to be added to an instance of a generic subprogram, it can be accomplished by creating a separate subprogram specification and then completing that specification with a renames-as-body of the instance. 

Proof: {AI12-0272-1} A generic formal subprogram is a subprogram, and there are no rules to prevent using these attributes on it. 

To be honest: In this and the following rules, we are talking about the enumeration literal True declared in package Standard (see A.1), and not some other value or identifier True. That matters as some rules depend on full conformance of these expressions, which depends on the specific declarations involved.

Aspect Description for Pre: Precondition; a condition that is expected to must hold true before a call.

Ramification: {AI05-0254-1} If other class-wide preconditions apply to the entity and no class-wide precondition is specified, no class-wide precondition is defined for the entity; of course, the class-wide preconditions (of ancestors) that apply are still going to be checked. We need subprograms that don't have ancestors and don't specify a class-wide precondition to have a class-wide precondition of True, so that adding such a precondition to a descendant has no effect (necessary as a dispatching call through the root routine would not check any precondition).

{AI12-0220-1} Pre'Class cannot be specified on an access-to-subprogram type because of a Legality Rule found in 13.1.1 that limits 'Class aspects to tagged types and primitive subprograms of tagged types. The same is true for Post'Class (below). 

Aspect Description for Pre'Class: Precondition that applies to corresponding subprograms of descendant types inherited on type derivation.

Aspect Description for Post: Postcondition; a condition that will must hold true after a call.

Aspect Description for Post'Class: Postcondition that applies to corresponding subprograms of descendant types inherited on type derivation.

Discussion: {AI12-0005-1} In the AARM notes below, we use the terms “inherited” and “inheritance” informally with respect to class-wide pre/post-conditions, to mean that the aspect applies to corresponding subprograms in descendant types. 

Reason: {AI12-0159-1} This ensures that the expression is well-defined for any primitive subprogram of a type descended from T.

Ramification: {AI12-0170-1} The operations of NT are also nonabstract, so the rule against a call of an abstract subprogram does not trigger for a class-wide precondition or postcondition. 

Discussion: {AI05-0183-1} Pre'Class and Post'Class can only be specified on primitive routines of tagged types, by a blanket rule found in 13.1.1.

Discussion: We use the term "requires overriding" here so that this rule is taken into account when calculating visibility in 8.3; otherwise we would have a mess when this routine is overridden. 

Reason: Such an inherited subprogram would necessarily violate the Liskov Substitutability Principle (LSP) if called via a dispatching call from an ancestor other than the one that provides the called body. In such a case, the class-wide precondition of the actual body is stronger than the class-wide precondition of the ancestor. If we did not enforce that precondition for the body, the body could be called when the precondition it knows about is False — such "counterfeiting" of preconditions has to be avoided. But enforcing the precondition violates LSP. We do not want the language to be implicitly creating bodies that violate LSP; the programmer can still write an explicit body that calls the appropriate parent subprogram. In that case, the violation of LSP is explicitly in the code and obvious to code reviewers (both human and automated).

We have to say that the subprogram is abstract for an abstract type in this case, so that the next concrete type has to override it for the reasons above. Otherwise, inserting an extra level of abstract types would eliminate the requirement to override (as there is only one declared operation for the concrete type), and that would be bad for the reasons given above. 

Ramification: This requires the set of class-wide preconditions that apply to the interface routine to be strictly stronger than those that apply to the concrete routine. Since full conformance requires each name to denote the same declaration, it is unlikely that independently declared preconditions would conform. This rule does allow "diamond inheritance" of preconditions, and of course no preconditions at all match.

We considered adopting a rule that would allow examples where the expressions would conform after all inheritance has been applied, but this is complex and is not likely to be common in practice. Since the penalty here is just that an explicit overriding is required, the complexity is too much. 

Reason: Such an overriding subprogram would violate LSP, as the precondition of S1 would usually be different (and thus stronger) than the one known to a dispatching call through an ancestor routine of S2. This is always OK if the preconditions match, so we always allow that. 

Ramification: This only applies to primitives of tagged types; other routines cannot have class-wide preconditions.

Reason: Any such Pre'Class will have no effect, as it will be ored with True. As such, it is highly misleading for readers, especially for those who are determining the assumptions that can be made in the body of the primitive subprogram. Note that in this case there is nothing explicit that might indicate that the class-wide precondition is ineffective. This rule does not prevent explicitly writing an ineffective class-wide precondition (for instance, if the parent subprogram has explicitly specified a precondition of True). 

Ramification: A Pre'Class defaults to True only if no class-wide preconditions are inherited for the subprogram. The same is true for Post'Class. 

Reason: We have to inherit precondition expressions that default to True, so that later overridings don't strengthen the precondition (a violation of LSP). We do the same for postconditions for consistency. 

Reason: We have to define the corresponding expression this way as overriding routines are only required to be subtype conformant; in particular, the parameter names can be different. So we have to talk about corresponding parameters without mentioning any names. 

This paragraph was deleted.Ramification: This can happen, for instance, if one of the subprograms called in the corresponding expression is abstract. We made the rule general so that we don't have to worry about exactly which cases can cause this to happen, both now and in the future. 

Reason: {AI12-0412-1} The above rules mean that a concrete primitive of an abstract type is effectively treated as abstract, if any nontrivial Pre'Class or Post'Class aspects apply to it. This makes sense because we are using a notional formal derived type model for such aspects, and an abstract type is not permitted as an actual type for such a formal type. If we didn't do this, the evaluation of the precondition or postcondition of a concrete subprogram of an abstract type could possibly call abstract functions. We allow illegal corresponding expressions on abstract subprograms as they could never be evaluated, and we need to allow such expressions to contain calls to abstract subprograms.

Discussion: {AI12-0412-1} As this Reference Manual was frozen, a significant incompatibility has come to light with the above rule. The wording makes some calls to non-abstract primitives of a tagged abstract type illegal even if no abstract routines are involved in the Pre'Class or Post'Class. It is likely that the above rule will be adjusted; check with ARG work at www.ada-auth.org/arg.html to find the adjusted rules. 

Ramification: {AI05-0290-1} If a class-wide precondition or postcondition expression is enabled, it remains enabled when inherited by an overriding subprogram, even if the policy in effect is Ignore for the inheriting subprogram. 

Reason: {AI12-0280-2} We mention literals explicitly in case they are not static (as when their subtype is not static, they are the literal null, and so on). We exclude literals of types with the aspects that are not Global => null as those cause a user-written subprogram with possible side effects to be called. 

Ramification: Constants of types with immutably limited or controlled parts are not allowed by this rule. Generic formal in objects are allowed by this rule (as they are defined to be full constant declarations). 

Reason: We only want things that cannot be changed. We can't just say “constant” since that includes views of variables in some cases (for instance, a dereference of an access to constant object can be a view of a variable). There are other things we could have allowed (like a loop parameter), but having a subprogram declaration where those could be used (like inside of a loop) seems unusual enough to not be worth defining. 

Ramification: All such parameters are by-copy, so the value won't change during the execution of the subprogram. 

Reason: Such a function can only depend on the values of its parameters. 

Discussion: It's OK if such an expression raises an exception, so long as every evaluation of the expression raises the same exception. 

Ramification: To be precise, a conditionally evaluated expression is determined to be unevaluated (including all of its subexpressions) under the following circumstances: 

Ramification: {AI12-0280-2} If X'Old occurs in a subexpression that is determined to be unevaluated, then there is no associated constant, and no evaluation of the prefix takes place. In general, this will require evaluating one or more known-on-entry subexpressions before creating and initializing any X'Old constants. Note that any 'Old in a known-on-entry subexpression evaluated this way represents the current value of the prefix (the 'Old itself can be ignored).

{AI12-0193-1} In the case of an accept statement, the constant is declared inside of the rendezvous. It is considered part of the initialization of the postcondition check, which is part of the rendezvous by definition (see 9.5.2). 

Ramification: This means that the underlying tag associated with X'Old is that of X and not that of the nominal type of X. 

Discussion: The prefix X can be any nonlimited object that obeys the syntax for prefix other than the few exceptions given above (discussed below). Useful cases are: the name of a formal parameter of mode [in] out, the name of a global variable updated by the subprogram, a function call passing those as parameters, a subcomponent of those things, etc.

A qualified expression can be used to make an arbitrary expression into a valid prefix, so T'(X + Y)'Old is legal, even though (X + Y)'Old is not. The value being saved here is the sum of X and Y (a function result is an object). Of course, in this case "+"(X, Y)'Old is also legal, but the qualified expression is arguably more readable.

Note that F(X)'Old and F(X'Old) are not necessarily equal. The former calls F(X) and saves that value for later use during the postcondition. The latter saves the value of X, and during the postcondition, passes that saved value to F. In most cases, the former is what one wants (but it is not always legal, see below).

{AI12-0032-1} If X has controlled parts, adjustment and finalization are implied by the implicit constant declaration. Similarly, the implicit constant declaration defines the accessibility level of X'Old.

If postconditions are disabled, we want the compiler to avoid any overhead associated with saving 'Old values.

'Old makes no sense for limited types, because its implementation involves copying. It might make semantic sense to allow build-in-place, but it's not worth the trouble. 

Reason: {AI05-0273-1} {AI12-0280-2} {AI12-0005-1} Since the prefix of an Old attribute_reference is evaluated unconditionally when the subprogram is called (if it is evaluated at all), we cannot allow it to include values that do not exist at that time (like 'Result and loop parameters of quantified_expressions). We also do not allow the prefix itself it to include 'Old references, as those would be redundant (because the evaluation of the the entire prefix, if it occurs, already happens on entry to is evaluated when the subprogram  is called), and allowing them would require some sort of order to the implicit constant declarations (because in A(I'Old)'Old, we surely would want the value of I'Old evaluated before the A(I'Old) is evaluated).

{AI05-0273-1} {AI12-0280-2} An additional rule applies when it cannot be determined on entry to the subprogram whether the Old attribute_reference will or will not be evaluated when the overall postcondition expression is evaluated. In such cases In addition, we require that only allow simple names as the prefix of the Old attribute_reference to statically name some object attrribute if the attribute_reference might not be evaluated when the postcondition expression is evaluated. This is necessary because the Old prefixes have to be unconditionally evaluated when the subprogram is called if there is any possibility that they might be needed; the compiler cannot in general know whether they will be needed in the postcondition expression. To see the problem, consider:

{AI12-0005-1} In this example, the compiler cannot know on entry what will be the value of I when the subprogram returns (since the subprogram execution can change it), and thus it does not know whether Table(I)'Old will be needed then. Thus it has to always create an implicit constant and evaluate Table(I) when Bar is called (because not having the value when it is needed is not acceptable). But if I = 0 when the subprogram is called, that evaluation will raise Constraint_Error, and that will happen even if I is unchanged by the subprogram and the value of Table(I)'Old is not ultimately needed. It's easy to see how a similar problem could occur for a dereference of an access type. This would be mystifying (since the point of the short circuit is to eliminate this possibility, but it cannot do so). Therefore, we require the prefix of any Old attribute_reference attribute in such a context to statically name denote an object, which eliminates anything that could change at during execution.

It is easy to work around most errors that occur because of this rule. Just move the 'Old to the outer object, before any indexing, dereferences, or components. (That does not work for function calls, however, nor does it work for array indexing if the index can change during the execution of the subprogram.) 

Ramification: {AI12-0032-1} An accept statement for a task entry with enabled postconditions such as 

behaves (at runtime) as follows: 

{AI12-0032-1} Preconditions are checked by the caller before the rendezvous begins. Postcondition expressions might, of course, reference 'Old constants.

{AI12-0032-1} In the case of a protected operation with enabled postconditions, 'Old constant declarations (if any) are elaborated after the start of the protected action. Postcondition checks (which might reference these constants) are performed before the end of the protected action as described below.

{AI12-0280-2} The prefix of an Old attribute_reference has to statically name an entity if it appears within a repeatedly evaluated expression. 

To be honest: {AI05-0220-1} An “access-to-function type” is an access-to-subprogram type whose designated profile is a function profile.

Ramification: The class-wide precondition expressions of the entity itself as well as those of any parent or progenitor operations are evaluated, as these expressions apply to the corresponding operations of all descendants.

Class-wide precondition checks are performed for all appropriate calls, but only enabled precondition expressions are evaluated. Thus, the check would be trivial if no precondition expressions are enabled. 

Reason: We need to explicitly allow short-circuiting of the evaluation of the class-wide precondition check if any expression fails, as it consists of multiple expressions; we don't need a similar permission for the specific precondition check as it consists only of a single expression. Nothing is evaluated for the call after a check fails, as the failed check propagates an exception. 

Ramification: The class-wide postcondition expressions of the entity itself as well as those of any parent or progenitor operations are evaluated, as these apply to all descendants; in contrast, only the specific postcondition of the entity applies. Postconditions can always be evaluated inside the invoked body. 

Reason: {AI12-0032-1} If a postcondition references the implicitly-declared constant associated with an Old attribute, the postcondition must be evaluated before the constant is finalized. One way to think of this is to imagine declaring a controlled object between any implicit "'Old" constant declarations and any explicit declarations, then performing postcondition checks during the finalization of this object. 

Ramification: This applies to access-to-subprogram calls, dispatching calls, and to statically bound calls. We need this rule to cover statically bound calls as well, as specific pre- and postconditions are not inherited, but the subprogram might be.

For concrete subprograms, we require the original specific postcondition to be evaluated as well as the inherited class-wide postconditions in order that the semantics of an explicitly defined wrapper that does nothing but call the original subprogram is the same as that of an inherited subprogram.

Note that this rule does not apply to class-wide preconditions; they have their own rules mentioned below. 

Ramification: For a dispatching call, we are talking about the Pre'Class(es) that apply to the subprogram that the dispatching call is resolving to, not the Pre'Class(es) for the subprogram that is ultimately dispatched to. The class-wide precondition of the resolved call is necessarily the same or stronger than that of the invoked call. For a statically bound call, these are the same; for an access-to-subprogram, (which has no class-wide preconditions of its own), we check the class-wide preconditions of the invoked routine.

{AI12-0233-1} Since this check is based on the “callable entity”, it does not depend on the view of the entity. This matters any time the ancestor type (if any) of the partial view differs from the parent type of the full view. In such a case, the view of the callable entity associated with the full view might inherit a Pre'Class while the view of the same callable entity associated with the partial view does not. 

Implementation Note: These rules imply that logically, class-wide preconditions of routines must be checked at the point of call (other than for access-to-subprogram calls, which must be checked in the body, probably using a wrapper). Specific preconditions that might be called with a dispatching call or via an access-to-subprogram value must be checked inside of the subprogram body. In contrast, the postcondition checks always need to be checked inside the body of the routine. Of course, an implementation can evaluate all of these at the point of call for statically bound calls if the implementation uses wrappers for dispatching bodies and for 'Access values.

There is no requirement for an implementation to generate special code for routines that are imported from outside of the Ada program. That's because there is a requirement on the programmer that the use of interfacing aspects do not violate Ada semantics (see B.1). That includes making pre- and postcondition checks. For instance, if the implementation expects routines to make their own postcondition checks in the body before returning, C code can be assumed to do this (even though that is highly unlikely). That's even though the formal definition of those checks is that they are evaluated at the call site. Note that pre- and postconditions can be very useful for verification tools (even if they aren't checked), because they tell the tool about the expectations on the foreign code that it most likely cannot analyze. 

Implementation Note: If the class-wide pre- and postcondition expressions are equivalent for S and S' because none of the primitive subprograms called in those expressions were overridden, no wrapper is needed. Otherwise, a wrapper is presumably needed to provide the correct logic. 

Implementation Note: {AI12-0220-1} A call via an access-to-subprogram value can be considered equivalent (with respect to dynamic semantics) to a call to a notional "wrapper" subprogram which has the Pre and Post aspects and the profile of the access-to-subprogram type and whose body contains (and returns, in the case of a function) only a call to the designated subprogram. However, other evaluation orders for the checks are allowed beyond those allowed by strictly following this model. This equivalence can be used to determine the appropriate point at which the constant associated with an Old attribute reference in the Post aspect for an access-to-subprogram type is elaborated and finalized.

Ramification: {AI12-0220-1} In the case of type conversion between two access-to-subprogram types, the Pre and Post aspects of the source type of the conversion play no role in any subsequent call via the conversion result; only the Pre and Post aspects of the target type of the conversion are relevant in that case. The same applies in the case of a “conversion” (using the term loosely) which is accomplished by combining a dereference and an Access attribute reference, as in Some_Pointer.all'Access.

Proof: {AI12-0272-1} This follows from the general Dynamic Semantics rules given above, but we mention it explicitly so that there can be no doubt that it is intended. 

To be honest: {AI12-0371-1} The specific precondition and postcondition that apply to a generic formal subprogram also apply to any renaming of that subprogram, even if that renaming is visible in the instance and called from outside of the generic instance. 

Reason: {AI12-0280-2} We allow the evaluation of known-on-entry subexpressions when they might be needed to determine whether to create a particular 'Old constant. We allow them to be evaluated later as well, or for the results to be saved somehow. This permission shouldn't matter, as the results ought to be same wherever they are evaluated and there should not be any side effects. The main effect of the permission is to determine when any exceptions caused by such subexpressions may be raised. We never require waiting to determine the value of such subexpressions, even if they aren't used to determine the creation of a constant for 'Old.

{AI05-0145-2} {AI05-0230-1} {AI05-0247-1} {AI05-0254-1} {AI05-0262-1} {AI05-0273-1} {AI05-0274-1} Pre and Post aspects are new. 

{AI12-0032-1} Corrigendum: The Old attribute is defined more carefully. This changes the nominal subtype and place of declaration of the attribute compared to the published Ada 2012 Reference Manual. In extreme cases, this could change the runtime behavior of the attribute (for instance, the tag might be different). The changes are most likely going to prevent bugs by being more intuitive, but it is possible that a program that previously worked might fail.

{AI12-0113-1} {AI12-0159-1} Corrigendum: Eliminated unintentional redispatching from class-wide preconditions and postconditions. This means that a different body might be evaluated for a statically bound call to a routine that has a class-wide precondition or postcondition. The change means that the behavior of Pre and Pre'Class will be the same for a particular subprogram, and that the known behavior of the operations can be assumed within the body of that subprogram for Pre'Class. We expect that this change will primarily fix bugs, as it will make Pre'Class and Post'Class work more like expected. In the case where redispatching is desired, an explicit conversion to a class-wide type can be used.

{AI12-0166-1} Correction: Specified that precondition checks always take place before starting a protected action. Original Ada 2012 left this unspecified, so if an implementation made the checks after starting the protected action, and a program depended upon that, the program might fail in a different compiler. But such a program was depending on unspecified behavior anyway, and thus was never portable; as such, such programs should be rare.

{AI12-0195-1} Correction: Specified that an inherited subprogram check both the original and new versions of a class-wide precondition. If a call on an inherited subprogram fails the original class-wide precondition when it passes the new class-wide precondition, then the call will fail the precondition check whereas it would have passed in original Ada 2012. (A similar possibility exists for class-wide postconditions.) This can only happen if the overriding subprograms somehow fail to follow the guidelines of LSP, so this should be rare (the entire point of class-wide preconditions and postconditions is to use them in cases where LSP is followed). 

{AI12-0045-1} {AI12-0005-1} Corrigendum: Precondition and postcondition aspects cannot be specified on instances of generic subprograms (they should be specified on the generic subprogram instead). This was (unintentionally) allowed by the Ada 2012 standard. These are not be allowed on instances as there is no corresponding way to add preconditions and postconditions to subprograms declared within the instance of a generic package. Therefore, allowing specification on a subprogram instance could present a maintenance problem in the future if the entity needs to be converted to a generic package (a common conversion).

{AI12-0131-1} Corrigendum: Pre'Class is no longer allowed to be specified for an overriding primitive subprogram unless there are also inherited class-wide precondittions. This incompatibility prevents cases where the explicit Pre'Class is counterfeited by an implicit class-wide precondition of True. This rule should catch more bugs than it creates; the programmer should have written Pre rather than Pre'Class in this case (or written Pre'Class on the original subprogram, not an overriding). Note that this incompatibility eliminates what otherwise would be an inconsistency with original Ada 2012, where precondition checks that would have previously been made for a statically bound call would no longer be made. That dynamic change was necessary to eliminate cases where the evaluated class-wide precondition on a dispatching call would have been weaker than the class-wide precondition of a statically bound call. (The original Ada 2012 violated the LSP semantics that class-wide preconditions were intended to model.)

{AI12-0198-1} Correction: A component expression in an array aggregate can now be potentially unevaluated, requiring the prefix to be statically determined. Existing code that uses the Old attribute with a dynamic prefix in such contexts will now be illegal. However, in many cases, the existing code will not do what the programmer is expecting (as Old is evaluated textually, once per occurrence, while array aggregate components are evaluated once per component). In addition, Old is a new Ada 2012 feature, so most Ada legacy code will not contain it. The problem is usually easily fixed by moving Old to an outer object (such as the entire aggregate). 

{AI12-0143-1} The Index attribute is new.

{AI12-0217-1} Correction: The prefix of a statically unevaluated Old attribute_reference can be a selected_component or indexed_component. This is considered a correction as the old rule is unintentionally too fierce, rejecting safe cases.

{AI12-0280-2} We make no restriction on the prefix of an Old attribute_reference if we can determine when the subprogram is entered (which is the point when Old prefixes are evaluated) whether it will be needed in the evaluation of the postcondition.

{AI12-0220-1} {AI12-0272-1} Pre and Post can be given on an access-to-subprogram type and on a generic formal subprogram.

{AI12-0412-1} Correction: We now allow the definition of a concrete subprogram S that has applicable Pre'Class or Post'Class expressions that is primitive for an abstract type T even when a Pre'Class or Post'Class may call an abstract subprogram. Rather, S is treated as if it is abstract (meaning that uses that might require evaluating a statically bound Pre'Class or Post'Class expression are not allowed). 

{AI05-0170-1} Correction: Clarified the wording about the meaning of the notional type NT and the corresponding expression. Both changes follow from other rules but are nonobvious.

{AI05-0185-1} Correction: Removed redundant (and sometimes incorrect) wording about the resolution of the Old and Result attributes.