Preconditions and Postconditions

This aspect specifies a specific precondition for a callable entity; it shall be specified by an expression, called a specific precondition expression. If not specified for an entity, the specific precondition expression for the entity is the enumeration literal True.

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.

This aspect specifies a class-wide precondition for an operation of a tagged type and its descendants; it shall be specified by an expression, called a class-wide precondition expression. If not specified for an entity, then if no other class-wide precondition applies to the entity, the class-wide precondition expression for the entity is the enumeration literal True.

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).

This aspect specifies a specific postcondition for a callable entity; it shall be specified by an expression, called a specific postcondition expression. If not specified for an entity, the specific postcondition expression for the entity is the enumeration literal True.

This aspect specifies a class-wide postcondition for an operation of a tagged type and its descendants; it shall be specified by an expression, called a class-wide postcondition expression. If not specified for an entity, the class-wide postcondition expression for the entity is the enumeration literal True.

Name Resolution Rules

{AI05-0145-2} The expected type for a precondition or postcondition expression is any boolean type.

{AI05-0145-2} {AI05-0262-1} 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 T is interpreted as having type T'Class. Similarly, a name that denotes a formal access parameter of type access-to-T is interpreted as having type access-to-T'Class. [This ensures that the expression is well-defined for a primitive subprogram of a type descended from T.]

{AI05-0145-2} {AI05-0264-1} 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 independently of context.

Legality Rules

{AI05-0145-2} {AI05-0230-1} The Pre or Post aspect shall not be specified for an abstract subprogram or a null procedure. [Only the Pre'Class and Post'Class aspects may be specified for such a subprogram.]

{AI05-0247-1} {AI05-0254-1} If a type T has an implicitly declared subprogram P inherited from a parent type T1 and a homograph (see 8.3) of P from a progenitor type T2, and

there is a class-wide precondition expression that applies to the corresponding primitive subprogram P2 of T2 that does not fully conform to any class-wide precondition expression that applies to P1,

{AI05-0247-1} {AI05-0254-1} then:

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.

{AI05-0247-1} If a renaming of a subprogram or entry S1 overrides an inherited subprogram S2, then the overriding is illegal unless each class-wide precondition expression that applies to S1 fully conforms to some class-wide precondition expression that applies to S2 and each class-wide precondition expression that applies to S2 fully conforms to some class-wide precondition expression that applies to S1.

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.

Static Semantics

{AI05-0145-2} If a Pre'Class or Post'Class aspect is specified for a primitive subprogram of a tagged type T, then the associated expression also applies to the corresponding primitive subprogram of each descendant of T.

{AI05-0145-2} {AI05-0262-1} If the assertion policy in effect at the point of a subprogram or entry declaration is Check, then preconditions and postconditions are considered to be enabled for that subprogram or entry.

{AI05-0145-2} For a prefix X that denotes an object of a nonlimited type, the following attribute is defined:

{AI05-0145-2} {AI05-0262-1} Within a postcondition expression, denotes the value of X at the beginning of the execution of the subprogram or entry to which the postcondition applies. For each X'Old in a postcondition expression that is enabled, a constant is implicitly declared at the beginning of the subprogram or entry, of the type of X, initialized to X. The value of X'Old in the postcondition expression is the value of this constant. The type of X'Old is the type of X. These implicit declarations occur in an arbitrary order.

Discussion: The prefix X can be any nonlimited object that obeys the syntax for prefix. 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.

{AI05-0145-2} For a prefix F that denotes a function declaration, the following attribute is defined:

{AI05-0145-2} {AI05-0262-1} Within a postcondition expression for function F, denotes the result object of the function. The type of this attribute is that of the function result except within a Post'Class postcondition expression for a function with a controlling result or with a controlling access result. For a controlling result, the type of the attribute is T'Class, where T is the function result type. For a controlling access result, the type of the attribute is an anonymous access type whose designated type is T'Class, where T is the designated type of the function result type.

Dynamic Semantics

{AI05-0145-2} {AI05-0247-1} If the assertion policy (see 11.4.2) in effect at the point of a subprogram or entry declaration is Check, then upon a call of the subprogram or entry, after evaluating any actual parameters, precondition checks are performed as follows:

The specific precondition check begins with the evaluation of the specific precondition expression that applies to the subprogram or entry; if the expression evaluates to False, Assertions.Assertion_Error is raised.

The class-wide precondition check begins with the evaluation of any class-wide precondition expressions that apply to the subprogram or entry. If and only if all the class-wide precondition expressions evaluate to False, Assertions.Assertion_Error is raised.

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.

{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} The checks are performed in an arbitrary order, and if any of the class-wide precondition expressions evaluate to True, it is not specified whether the other class-wide precondition expressions are evaluated. The precondition checks and any check for elaboration of the subprogram body are performed in an arbitrary order. It is not specified whether in a call on a protected operation, the checks are performed before or after starting the protected action. For an entry call, the checks are performed prior to checking whether the entry is open.

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.

{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} {AI05-0262-1} If the assertion policy in effect at the point of a subprogram or entry declaration is Check, then upon successful return from a call of the subprogram or entry, prior to copying back any by-copy in out or out parameters, the postcondition check is performed. This consists of the evaluation of the specific and class-wide postcondition expressions that apply to the subprogram or entry. If any of the postcondition expressions evaluate to False, then Assertions.Assertion_Error is raised. The postcondition expressions are evaluated in an arbitrary order, and if any postcondition expression evaluates to False, it is not specified whether any other postcondition expressions are evaluated. The postcondition check and constraint checks associated with copying back in out or out parameters are performed in an arbitrary order.

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.

{AI05-0145-2} {AI05-0262-1} If a precondition or postcondition check fails, the exception is raised at the point of the call. [The exception cannot be handled inside the called subprogram or entry.] An exception raised by the evaluation of a precondition or postcondition expression is also raised at the point of call.

{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} {AI05-0262-1} For any subprogram or entry call (including dispatching calls), the checks that are performed to verify specific precondition expressions and specific and class-wide postcondition expressions are determined by those for the subprogram or entry actually invoked. Note that the class-wide postcondition expressions verified by the postcondition check that is part of a call on a primitive of type T includes all class-wide postcondition expressions originating in any progenitor of T[, even if the primitive called is inherited from a type T1 and some of the postcondition expressions do not apply to the corresponding primitive of T1].

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.

{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} The class-wide precondition check for a call to a subprogram or entry consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily the one that is invoked).

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.

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.

{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} For a call via an access-to-subprogram value, all precondition and postcondition checks performed are determined by the subprogram or entry denoted by the prefix of the Access attribute reference that produced the value.

{AI05-0145-2} {AI05-0262-1} If the assertion policy in effect at the point of a subprogram or entry declaration is Ignore, then no precondition or postcondition check is performed on a call on that subprogram or entry. For a dispatching call, if the assertion policy in effect at the point of the declaration of the denoted callable entity is not the same as the assertion policy in effect at the point of the declaration of the invoked callable entity, it is implementation defined whether any precondition or postcondition checks are made.

Discussion: {AI05-0262-1} For a dispatching call with different policies, whether a check is made probably will be different for different checks, depending on whether the implementation makes them at the call site, in a wrapper, or inside the called subprogram or entry.

Bounded (Run-Time) Errors

{AI05-0145-2} It is a bounded error to invoke a potentially blocking operation (see 9.5.1) during the evaluation of a precondition or postcondition expression. If the bounded error is detected, Program_Error is raised. If not detected, execution proceeds normally, but if it is invoked within a protected action, it might result in deadlock or a (nested) protected action.

5 {AI05-0145-2} {AI05-0262-1} A precondition is checked just before the call. If another task can change any value that the precondition expression depends on, the precondition need not hold within the subprogram or entry body.

6.1.1 Preconditions and Postconditions

Name Resolution Rules

Legality Rules

Static Semantics

Dynamic Semantics

Bounded (Run-Time) Errors

Extensions to Ada 2005