We will look first at the simple case when inheritance is not involved and then look at more general cases. Specific preconditions and postconditions are applied using the aspects Pre and Post respectively whereas class wide conditions are applied using the aspects Pre'Class and Post'Class.

To apply a specific precondition Before and/or a specific postcondition After to a procedure P we write

where Before and After are expressions of a Boolean type (that is of type Boolean or a type derived from it).

The precondition Before and the postcondition After can involve the parameters P1 and P2 and P3 and any visible entities such as other variables, constants and functions. Note that Before can involve the out parameter P3 inasmuch as one can always read any constraints on an out parameter such as the bounds if it were an array.

The attribute X'Old will be found useful in postconditions; it denotes the value of X on entry to P. Old is typically applied to parameters of mode in out such as P2 but it can be applied to any visible entity such as a global variable. This can be useful for monitoring global variables which are updated by the call of P. But note that 'Old can only be used in postconditions and not in arbitrary text and it cannot be applied to objects of a limited type.

Perhaps surprisingly 'Old can also be applied to parameters of mode out. For example, in the case of a parameter of a record type that is updated as a whole, nevertheless we might want to check that a particular component has not changed. Thus in updating some personal details, such as address and occupation, we might want to ensure that the person's date of birth and sex are not tampered with by writing

In the case of an array, we can write A(I)'Old which means the original value of A(I). But A(I'Old) is different since it is the component of the final value of A but indexed by the old value of I.

Remember that the result of a function is an object and so 'Old can be applied to it. Note carefully the difference between F(X)'Old and F(X'Old). The former applies F to X on entry to the subprogram and saves it. The latter saves X and applies F to it when the postcondition is evaluated. These could be different because the function F might also involve global variables which have changed.

Generally 'Old can be applied to anything but there are restrictions on its use in certain conditional structures in which it can only be applied to statically determined objects. This is illustrated by the following (based on an example in the AARM)

The programmer's intent is that the postcondition uses a short circuit form to avoid evaluating Table(I) f I is not positive on exit from the procedure. But, 'Old is evaluated and stored on entry and this could raise Constraint_Error because I might for example be zero. This is a conundrum since the compiler cannot know whether the value of Table(I) will be needed and also I can change so it cannot know which I anyway. So such structures are forbidden.

(The collector of Ada curiosities might be amused to note that we can write

and then in a postcondition we could have

which is palindromic. If the subtype were blo rather than dlo then the expression would be mirror reflective!

I am grateful to Jean-Pierre Rosen for this example.)

In the case of a postcondition applying to a function F, the result of the function is denoted by the attribute F'Result. Again this attribute can only be used in postconditions.

Some trivial examples of declarations of a procedure Pinc and function Finc to perform an increment are

Preconditions and postconditions are controlled by the pragma Assertion_Policy. They are enabled by

and disabled by using parameter Ignore. It is the value in effect at the point of the subprogram declaration that matters. So we cannot have a situation where the policy changes during the call so that preconditions are switched on but postconditions are off or vice versa.

And so the overall effect of calling P with checks enabled is roughly that, after evaluating any parameters at the point of call, it as if the body were

Occurrances of Assertion_Error are propagated and so raised at the point of call; they cannot be handled inside P. Of course, if the evaluation of Before or After themselves raise some exception then that will similarly be propagated to the point of call.

Note that conditions Pre and Post can also be applied to entries.

Before progressing to the problems of inheritance it is worth reconsidering the purpose of pre- and postconditions.

The symmetry is neatly illustrated by the diagram below

The simplest form of inheritance occurs with derived types that are not tagged. Suppose we declare the procedure Pinc as above with the postcondition shown and supply a body

and then declare a type

then the procedure Pinc is inherited by the type Apples. So if we then write

what actually happens is that the code of the procedure Pinc originally written for Integer is called and so the postcondition is inherited automatically.

If the user now wants to add a precondition to Pinc that the number of apples is not negative then a completely new subprogram has to be declared which overrides the old one thus

and a new body has to be supplied (which will of course in this curious case be essentially the same as the old one). So we cannot inherit an operation and change its conditions at the same time.

We now turn to tagged types and first continue to consider the specific conditions Pre and Post. As a perhaps familiar example, consider the hierarchy consisting of a type Object and then direct descendants Circle, Square and Triangle.

Suppose the type Object is

and we declare a function Area thus

This imposes a requirement on the caller that the function is called only with objects with positive x-coordinate (for some obscure reason), and a requirement on the implementer of the body that the area is zero (raw objects are just points and have no area).

If we now declare a type Circle as

and override the inherited function Area then the Pre and Post conditions on Area for Object are not inherited and we have to supply new ones, perhaps

The conditions ensure that all of the circle is in the right half-plane and that the area is about right!

So the rules so far are exactly as for the untagged case. If an operation is not overridden then it inherits the conditions from its ancestor but if it is overridden then those conditions are lost and new ones have to be supplied. And if no new ones are supplied then they are by default taken to be True.

In conclusion, the conditions Pre and Post are very much part of the actual body. One consequence of this is that an abstract subprogram cannot have Pre and Post conditions because an abstract subprogram has no body.

We now turn to the class wide conditions Pre'Class and Post'Class which are subtly different. The first point is that the class wide ones apply to all descendants as well even if the operations are overridden. In the case of Post'Class if an overridden operation has no condition given then it is taken to be True (as in the case of Post). But in the case of Pre'Class, if an overridden operation has no condition given then it is only taken to be True if no other Pre'Class applies (no other is inherited). We will now look at the consequences of these rules.

It might be that we want certain conditions to hold throughout the hierarchy, perhaps that all objects concerned have a positive x-coordinate and nonnegative area. In that case we can use class wide conditions.

Now when we declare Area for Circle, Pre'Class and Post'Class from Object will be inherited by the function Area for Circle. Note that within a class wide condition a formal parameter of type T is interpreted as of T'Class. Thus O is of type Object'Class and thus applies to Circle. The inherited postcondition is simply that the area is not negative and uses the attribute 'Result.

If we do not supply conditions for the overriding Area for Circle and simply write

then the precondition inherited from Object still applies. In the case of the postcondition not only is the postcondition from Object inherited but there is also an implicit postcondition of True. So the applicable conditions for Area for Circle are

Suppose on the other hand that we give explicit Pre'Class and Post'Class for Area for Circle thus

We then find that the applicable conditions for Area for Circle are

Incidentally, it makes a lot of sense to declare the type Object as abstract so that we cannot declare pointless objects. In that case Area might as well be abstract as well. Although we cannot give conditions Pre and Post for an abstract operation we can still give the class wide conditions Pre'Class and Post'Class.

If the hierarchy extends further, perhaps Equilateral_Triangle is derived from Triangle which itself is derived from Object, then we could add class wide conditions to Area for Triangle and these would also apply to Area for Equilateral_Triangle. And we might add specific conditions for Equilateral_Triangle as well. So we would then find that the following apply to Area for Equilateral_Triangle

The postconditions are quite straightforward, all apply and all must be true on return from the function Area. The compiler can see all these postconditions when the code for Area is compiled and so they are all checked in the body. Note that any default True makes no difference because B and True is the same as B.

However, the rules regarding preconditions are perhaps surprising. The specific precondition Pre for Equilateral_Triangle must be true (checked in the body) but so long as just one of the class wide preconditions Pre'Class for Object and Triangle is true then all is well. Note that class wide preconditions are checked at the point of call. Do not get confused over the use of the word apply. They all apply but only the ones seen at the point of call are actually checked.

The reason for this state of affairs concerns dispatching and especially redispatching. Consider the case of Ada airlines which has Basic, Nice and Posh passengers. Basic passengers just get a seat. Nice passengers also get a meal and Posh passengers also get a limo. The types Reservation, Nice_Reservation, and Posh_Reservation form a hierarchy with Nice_Reservation being extended from Reservation and so on. The facilities are assigned when a reservation is made by calling an appropriate procedure Make thus

Each Make calls its ancestor in order to avoid duplication of code and to ease maintenance.

A variation involving redispatching introduces two different procedures Order_Meal, one for Nice passengers and one for Posh passengers. We then need to ensure that Posh passengers get a posh meal rather than a nice meal. We write

Now suppose we have a precondition Pre'Class on Order_Meal for Nice passengers and one on Order_Meal for Posh passengers. The call of Order_Meal sees that it is for Nice_Reservation'Class and so the code includes a test of Pre'Class on Nice_Reservation. It does not necessarily know of the existence of the type Posh_Reservation and cannot check Pre'Class on that Order_Meal. At a later date we might add Supersonic passengers (RIP Concorde) and this can be done without recompiling the rest of the system so it certainly cannot do anything about checking Pre'Class on Order_Meal for Supersonic_Reservation which does not exist when the call is compiled. So when we eventually get to the body of one of the procedures Order_Meal all we know is that some Pre'Class on Order_Meal has been checked somewhere. And that is all that the writer of the code of Order_Meal can rely upon. Note that nowhere does the compiled code actually "or" a lot of preconditions together.

In summary, class wide preconditions are checked at the point of call. Class wide postconditions and both specific pre- and postconditions are checked in the actual body.

A small point to remember is that a class wide operation such as

is not a primitive operation of T and so although we can specify Pre and Post for Do_It we cannot specify Pre'Class and Post'Class for Do_It.

We noted above that the aspects Pre and Post cannot be specified for an abstract subprogram because it doesn't have a body. They cannot be given for a null procedure either, since we want all null procedures to be identical and do nothing and that includes no conditions.

We now turn to the question of multiple inheritance and progenitors.

In the case of multiple inheritance we have to consider the so-called Liskov Substitution Principle (LSP). The usual consequence of LSP is that in the case of preconditions they are combined with "or" (thus weakening) and the rule for postconditions is that they are combined with "and" (thus strengthening). But the important thing is that a relevant concrete operation can be substituted for the corresponding operations of all its relevant ancestors.

In Ada, a type T can have one parent and several progenitors. Thus we might have

where P is the parent and G1 and G2 are progenitors. Remember that a progenitor cannot have components and cannot have concrete operations (apart possibly for null procedures). So the operations of the progenitors have to be abstract or null and cannot have Pre and Post conditions. However, they can have Pre'Class and Post'Class conditions. It is possible that the same operation Op is primitive for more than one of these. Thus the progenitors G1 and G2 might both have an operation Op thus

If they are conforming (as they are in this case) then the one concrete operation Op of the type T derived from both G1 and G2 will implement both of these. (If they don't conform then they are simply overloadings and two operations of T are required). Hence the one Op for T can be substituted for the Op of both G1 and G2 and LSP is satisfied.

Now suppose both abstract operations have pre- and postconditions. Take postconditions first, we might have

Users of the Op of G1 will expect the postcondition After1 to be satisfied by any implementation of that Op. So if using the Op of T which implements the abstract Op of G1, it follows that Op of T must satisfy the postcondition After1. By a similar argument regarding G2, it must also satisfy the postcondition After2.

It thus follows that the effective postcondition on the concrete Op of T is as if we had written

But of course we don't actually have to write that since we simply write

and it automatically inherits both postconditions and the compiler inserts the appropriate code in the body. Remember that if we don't give a condition then it is True by default but anding in True makes no difference.

If we do provide another postcondition thus

then the overall class wide postcondition to be checked before returning will be After1 and After2 and After_T.

Now consider preconditions. Suppose the declarations of the two versions of Op are

Assuming that there is no corresponding Op for P, we must provide a concrete operation for T thus

This means that at a point of call of Op the precondition to be checked is Before_T or exam[Before1] or Before2. As long as this is satisfied it does not matter that Before1 and Before2 might have been different.

If we do not provide an explicit Pre'Class then the condition to be checked at the point of call is Before1 or Before2.

An interesting case arises if a progenitor (say G1) and the parent have a conforming operation. Thus suppose P itself has the operation

and moreover that the operation is not abstract. Then (ignoring preconditions for the moment) this Op for P is inherited by T and thus provides a satisfactory implementation of Op for G1 and all is well.

Now suppose that Op for P has a precondition thus

and that Before_P and Before1 are not the same. If we do not provide an explicit overriding for Op, it would be possible to call the body of Op for P when the precondition it knows about, Before_P, is False (since Before1 being True would be sufficient to allow the call to proceed). This would effectively mean that no class wide preconditions could be trusted within the subprogram body and that would be totally unacceptable. So in this case there is a rule that an explicit overriding is required for Op for T.

If Op for P is abstract then a concrete Op for T must be provided and the situation is just as in the case for the Op for G1 and G2.

If T itself is declared as abstract (and P is not abstract and Op for P is concrete) then the inherited Op for T is abstract.

(These rules are similar to those for functions returning a tagged type when the type is extended; it has to be overridden unless the type is abstract in which case the inherited operation is abstract.)

We finish this somewhat mechanical discussion of the rules by pointing out that if silly inappropriate preconditions are given then we will get a silly program.

At the end of the day, the real point is that programmers should not write preconditions that are not sensible and sensibly related to each other. Because of the generality, the compiler cannot tell so stupid things are hard to prohibit. There is no defence against stupid programmers.

A concrete example using simple numbers might help. Suppose we have a tagged type T1 and an operation Solve which takes a parameter of type T1 and perhaps finds the solution to an equation defined by the components of T1. Solve delivers the answer in a parameter A with a parameter D giving the number of significant digits required in the answer. Also we impose a precondition on the number of digits D thus

The intent here is that the version of Solve for the type T1 always works if the number of significant digits asked for is less than 5.

Now suppose we declare a type T2 derived from T1 and that we override the inherited Solve with a new version that works if the number of significant digits asked for is less than 10

And so on with a type T3

Thus we have a hierarchy of algorithms Solve with increasing capability.

Now suppose we have a dispatching call

this will dispatch to one of the Solve procedures but we do not know which one. The only precondition that applies is that on the Solve for T1 which is D < 5. That is fine because D < 5 implies D < 10 and D < 15 and so on. Thus the preconditions work because the hierarchy weakens them.

Similarly, if we have

then it will dispatch to a Solve for one of T2, T3, ..., but not to the Solve for T1. The applicable preconditions are D < 5 and D < 10 and these are notionally ored together which means D < 10 is actually required. To see this suppose we supply D = Digs = 7. Then D < 5 is False but D < 10 is True so by oring False and True we get True, so the call works.

On the other hand if we write

then no dispatching is involved and the Solve for T2 is called. But both class wide preconditions D < 5 and D < 10 apply and so again the resulting ored precondition that is required is D < 10.

Now it should be clear that if the preconditions do not form a weakening hierarchy then we will be in trouble. Thus if the preconditions were D < 15 for T1, D < 10 for T2, and D < 5 for T3, then dispatching from the root will only check D < 15. However, we could end up calling the Solve for T2 which expects the precondition D < 10 and this might not be satisfied.

Care is thus needed with preconditions that they are sensibly related.

Finally, note that pre- and postconditions are allowed on generic units but not on instances. See Section 9.5 of the Epilogue.

© 2011, 2012, 2013 John Barnes Informatics.

Sponsored in part by: