Annotated Ada Reference ManualLegal Information
Contents   Index   References   Search   Previous   Next 

6.1.1 Preconditions and Postconditions

1/4
{AI05-0145-2} {AI05-0247-1} {AI12-0045-1} For a noninstance subprogram, a generic subprogram, or an entry, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
1.a/4
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. 
2/3
Pre
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.
2.a/3
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.
2.b/3
Aspect Description for Pre: Precondition; a condition that must hold true before a call.
3/3
{AI05-0254-1} {AI05-0262-1} Pre'Class

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.
3.a/3
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). 
3.b/3
Aspect Description for Pre'Class: Precondition inherited on type derivation.
4/3
Post
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.
4.a/3
Aspect Description for Post: Postcondition; a condition that must hold true after a call.
5/3
{AI05-0262-1} Post'Class

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.
5.a/3
Aspect Description for Post'Class: Postcondition inherited on type derivation.

Name Resolution Rules

6/3
{AI05-0145-2} The expected type for a precondition or postcondition expression is any boolean type.
7/4
{AI05-0145-2} {AI05-0262-1} {AI12-0113-1} {AI12-0159-1} Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram S of a tagged type T, a name that denotes a formal parameter (or S'Result) of type T is interpreted as though it had a (notional) type NT that is a formal derived type whose ancestor type is T, with directly visible primitive operations. Similarly, a name that denotes a formal access parameter (or S'Result) of type access-to-T is interpreted as having type access-to-NT. [The result of this interpretation is that the only operations that can be applied to such names are those defined for such a formal derived type.]
7.a/4
Reason: {AI12-0159-1} This ensures that the expression is well-defined for any primitive subprogram of a type descended from T
8/3
{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

9/3
{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.]
9.a/3
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.
10/3
{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
11/3
the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and
12/3
the class-wide precondition expression True does not apply to P1 (implicitly or explicitly); and
13/3
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
14/3
{AI05-0247-1} {AI05-0254-1} then:
15/3
If the type T is abstract, the implicitly declared subprogram P is abstract.
16/3
Otherwise, the subprogram P requires overriding and shall be overridden with a nonabstract subprogram.
16.a/3
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. 
16.b/3
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).
16.c/3
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. 
16.d/3
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.
16.e/3
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. 
17/3
{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.
17.a/3
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. 
17.b/3
Ramification: This only applies to primitives of tagged types; other routines cannot have class-wide preconditions.
17.1/4
  {AI12-0131-1} Pre'Class shall not be specified for an overriding primitive subprogram of a tagged type T unless the Pre'Class aspect is specified for the corresponding primitive subprogram of some ancestor of T.
17.c/4
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).
17.2/4
  {AI12-0131-1} In addition to the places where Legality Rules normally apply (see 12.3), these rules also apply in the private part of an instance of a generic unit. 

Static Semantics

18/4
{AI05-0145-2} {AI12-0113-1} {AI12-0131-1} If a Pre'Class or Post'Class aspect is specified for a primitive subprogram S of a tagged type T, or such an aspect defaults to True, then a corresponding expression also applies to the corresponding primitive subprogram S of each descendant of T. The corresponding expression is constructed from the associated expression as follows:
18.a/4
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. 
18.b/4
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. 
18.1/4
{AI12-0113-1} References to formal parameters of S (or to S itself) are replaced with references to the corresponding formal parameters of the corresponding inherited or overriding subprogram S (or to the corresponding subprogram S itself).
18.c/4
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.
18.2/4
  {AI12-0113-1} The primitive subprogram S is illegal if it is not abstract and the corresponding expression for a Pre'Class or Post'Class aspect would be illegal.
18.d/4
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. 
18.e/4
Reason: 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.
19/3
{AI05-0145-2} {AI05-0262-1} {AI05-0290-1} If performing checks is required by the Pre, Pre'Class, Post, or Post'Class assertion policies (see 11.4.2) in effect at the point of a corresponding aspect specification applicable to a given subprogram or entry, then the respective precondition or postcondition expressions are considered enabled.
19.a/3
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. 
20/3
{AI05-0273-1} An expression is potentially unevaluated if it occurs within:
21/3
any part of an if_expression other than the first condition;
22/3
a dependent_expression of a case_expression;
22.1/4
{AI12-0032-1} a predicate of a quantified_expression;
23/3
the right operand of a short-circuit control form; or
24/3
a membership_choice other than the first of a membership operation. 
25/3
{AI05-0145-2} For a prefix X that denotes an object of a nonlimited type, the following attribute is defined: 
26/4
X'Old
{AI05-0145-2} {AI05-0262-1} {AI05-0273-1} {AI12-0032-1} Each X'Old in a postcondition expression that is enabled denotes a constant that is implicitly declared at the beginning of the subprogram body, entry body, or accept statement.
26.1/4
{AI12-0032-1} {AI12-0159-1} The implicitly declared entity denoted by each occurrence of X'Old is declared as follows:
26.2/4
If X is of an anonymous access type defined by an access_definition A then 
26.3/4
X'Old : constant A := X;
26.4/4
If X is of a specific tagged type T then 
26.5/4
anonymous : constant T'Class := T'Class(X);
X'Old : T renames T(anonymous);
26.6/4
where the name X'Old denotes the object renaming. 
26.a/4
Ramification: This means that the underlying tag associated with X'Old is that of X and not that of the nominal type of X. 
26.7/4
Otherwise
26.8/4
X'Old : constant S := X;
26.9/4
where S is the nominal subtype of X. This includes the case where the type of S is an anonymous array type or a universal type. 
26.10/4
{AI12-0032-1} The nominal subtype of X'Old is as implied by the above definitions. The expected type of the prefix of an Old attribute is that of the attribute. Similarly, if an Old attribute shall resolve to be of some type, then the prefix of the attribute shall resolve to be of that type.
27/3
{AI05-0145-2} {AI05-0262-1} {AI05-0273-1} Reference to this attribute is only allowed within a postcondition expression. The prefix of an Old attribute_reference shall not contain a Result attribute_reference, nor an Old attribute_reference, nor a use of an entity declared within the postcondition expression but not within prefix itself (for example, the loop parameter of an enclosing quantified_expression). The prefix of an Old attribute_reference that is potentially unevaluated shall statically denote an entity.
27.a/3
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.
27.b/3
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.
27.c/3
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).
27.d/4
{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.
27.e/3
If postconditions are disabled, we want the compiler to avoid any overhead associated with saving 'Old values.
27.f/3
'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. 
27.g/3
Reason: {AI05-0273-1} Since the prefix is evaluated unconditionally when the subprogram is called, 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 it to include 'Old references, as those would be redundant (the entire prefix 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).
27.h/3
{AI05-0273-1} In addition, we only allow simple names as the prefix of the Old attribute 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; the compiler cannot in general know whether they will be needed in the postcondition expression. To see the problem, consider:
27.i/3
Table : array (1..10) of Integer := ...
procedure Bar (I : in out Natural)
   with Post => I > 0 and then Table(I)'Old = 1; -- Illegal
27.j/3
In this example, the compiler cannot know 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 in such a context to statically denote an object, which eliminates anything that could change at during execution.
27.k/3
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.) 
27.l/4
Ramification: {AI12-0032-1} An accept statement for a task entry with enabled postconditions such as 
27.m/4
accept E do
   statements
exception
   handlers
end;
27.n/4
behaves (at runtime) as follows: 
27.o/4
accept E do
   declare
      declarations, if any, of 'Old constants
   begin
      begin
         statements
      exception
         handlers
      end;
      postcondition checks
   end;
end;
27.p/4
{AI12-0032-1} Preconditions are checked by the caller before the rendezvous begins. Postcondition expressions might, of course, reference 'Old constants.
27.q/4
{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.
28/3
{AI05-0145-2} For a prefix F that denotes a function declaration, the following attribute is defined:
29/3
F'Result
{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.
30/3
{AI05-0262-1} Use of this attribute is allowed only within a postcondition expression for F. 

Dynamic Semantics

31/3
{AI05-0145-2} {AI05-0247-1} {AI05-0290-1} Upon a call of the subprogram or entry, after evaluating any actual parameters, precondition checks are performed as follows:
32/3
The specific precondition check begins with the evaluation of the specific precondition expression that applies to the subprogram or entry, if it is enabled; if the expression evaluates to False, Assertions.Assertion_Error is raised; if the expression is not enabled, the check succeeds.
33/3
The class-wide precondition check begins with the evaluation of any enabled 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.
33.a/3
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.
33.b/3
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. 
34/3
{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} {AI05-0269-1} The precondition 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.
34.a/3
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. 
35/3
{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} {AI05-0262-1} {AI05-0290-1} 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 any enabled 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 any constraint or predicate checks associated with in out or out parameters are performed in an arbitrary order.
35.a/3
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. 
35.1/4
  {AI12-0032-1} For a call to a task entry, the postcondition check is performed before the end of the rendezvous; for a call to a protected operation, the postcondition check is performed before the end of the protected action of the call. The postcondition check for any call is performed before the finalization of any implicitly-declared constants associated (as described above) with Old attribute_references but after the finalization of any other entities whose accessibility level is that of the execution of the callable construct. 
35.a.1/4
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. 
36/3
{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]. Similarly, any exception raised by the evaluation of a precondition or postcondition expression is raised at the point of call.
37/4
{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} {AI05-0262-1} {AI12-0113-1} {AI12-0159-1} For any call to a subprogram or entry S (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 subprogram of type T includes all class-wide postcondition expressions originating in any progenitor of T[, even if the primitive subprogram called is inherited from a type T1 and some of the postcondition expressions do not apply to the corresponding primitive subprogram of T1]. Any operations within a class-wide postcondition expression that were resolved as primitive operations of the (notional) formal derived type NT, are in the evaluation of the postcondition bound to the corresponding operations of the type identified by the controlling tag of the call on S.[ This applies to both dispatching and non-dispatching calls on S.]
37.a/3
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.
37.b/3
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.
37.c/3
Note that this rule does not apply to class-wide preconditions; they have their own rules mentioned below. 
38/4
{AI05-0145-2} {AI05-0247-1} {AI05-0254-1} {AI12-0113-1} {AI12-0159-1} The class-wide precondition check for a call to a subprogram or entry S consists solely of checking the class-wide precondition expressions that apply to the denoted callable entity (not necessarily to the one that is invoked). Any operations within such an expression that were resolved as primitive operations of the (notional) formal derived type NT are in the evaluation of the precondition bound to the corresponding operations of the type identified by the controlling tag of the call on S.[ This applies to both dispatching and non-dispatching calls on S.]
38.a/3
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. 
38.b/3
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.
38.c/3
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. 
39/3
{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.
NOTES
40/3
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. 

Extensions to Ada 2005

40.a/3
{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. 

Inconsistencies With Ada 2012

40.b/4
{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 Standard. 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.
40.c/4
{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.

Incompatibilities With Ada 2012

40.d/4
{AI12-0045-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).
40.e/4
{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.

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe