Rationale Update for Ada 2012

John Barnes
Contents   Index   References   Previous   Next 

Chapter 2: Contracts and aspects

This is perhaps the most exciting area of Ada 2012 and covers matters such as the new notation for aspects which replaces many uses of pragmas and also the introduction of contracts. Contracts include pre- and postconditions, type invariants, and subtype predicates.
The following Ada issues cover this area:
32
Questions on 'Old
41
Type_Invariant'Class for interface types
42
Type invariant checking rules
44*
Calling visible functions from type invariant expressions
45*
Pre- and Postconditions are allowed for generic subprograms
49
Invariants need to be checked on the initialization of deferred constants
54*
Aspect Predicate_Failure
68
Predicates and the current instance of a subtype
71*
Order of evaluation when multiple predicates apply
77
Has_Same_Storage on objects of size zero
96
The exception raised when a subtype conversion fails a predicate check
99
Wording problems with predicates
104
Overriding an aspect is undefined
105
Pre and Post are not allowed on any subprogram completion
113
Class-wide preconditions and statically bound calls
116
Private types and predicates
131
Inherited Pre'Class when unspecified on initial subprogram
133
Type invariants and default initialized objects
149
Type invariants are checked for functions returning access-to-type
150
Class-wide type invariants and statically bound calls
154
Aspects of library units
These changes can be grouped as follows.
There are a number of clarifications on pre- and postconditions in general (45, 105), some additional rules on the use of the aspect Old (32), and a trivial omission on the attribute Has_Same_Storage (77).
There are also clarifications regarding types and the use of class wide conditions and invariants (113, 150).
A number of additional rules are required describing the places where type invariants are checked (41, 42, 44, 49, 133, 149).
A new aspect Predicate_Failure and rules concerning checking order are added (54, 71, 96). A number of clarifications to the rules for predicates are added (68, 99, 116).
Finally, there are minor clarifications regarding aspects in general (104, 154).

AI-45 notes that pre-and postconditions (both specific and classwide) are allowed on generic programs but they are not allowed on instances of generic subprograms. This avoids awkward maintenance problems that might arise if such conditions were allowed on both a generic and an instance. On a similar matter, it was the intent that pre- and postconditions should always be visible to the user and so go on specifications and not bodies which are completions. However, the wording forgot to mention the new expression functions which as well as standing alone can also be completions (see the example of Non_Zero in AI-49 below). Such expression functions and null procedures acting as completions cannot have pre- and postconditions either (AI-105).
The attribute 'Old which is used in a postcondition to indicate the initial value of a parameter (or maybe a global) is a bit tricky. AI-32 adds some more (fairly obvious) detail such as that X and X'Old have the same type even if it is anonymous.
A trivial point about the attribute Has_Same_Storage which is useful in preconditions is that the expression X'Has_Same_Storage(Y) returns False if X or Y or both occupy zero bits. (AI-77).
AI-131 concerns Pre'Class. If the initial definition of a subprogram does not specify Pre'Class then the corresponding subprograms of derived types just inherit True as one would expect. It also notes that one cannot specify Pre'Class for an overriding subprogram of a type unless Pre'Class is specified for some ancestor. This is because it would be ored with True and thus have no effect.
AI-113 and AI-150 address a problem with Pre'Class, Post'Class and Type_Invariant'Class and parameters. Typically we might have something like
procedure P(S: in out T; ...)
   with Pre'Class => expression involving S
where T is a tagged type. The procedure P can be called with a statically bound parameter or indeed with a dynamically bound classwide parameter. The wording is clarified that the actual types of the actual parameters are always used. The reader is referred to the text of the Ada Issues which have a large example which should be helpful.
It is well-known that type invariants are not intended to be foolproof but to be helpful in catching many flaws (unlike pre- and postconditions which are meant to be perfect). As time has passed more little quirks have been found regarding when type invariants should or should not be checked. Remember that invariants apply to private types. When we have a full view of the type (as in a subprogram in the body of the package declaring the type) then we can change an object of the type temporarily to a state where the invariant does not apply (this is often necessary for intermediate stages in manipulation). However, when we leave the full view by for example returning from a subprogram in the package body then checks are applied on parameters and so on.
AI-44 states that type invariants are not checked on in parameters of functions but are checked on in parameters of procedures. This is necessary to avoid infinite recursion which would arise if an invariant itself calls a function with a parameter of the type. Moreover, a classwide invariant could not be used at all without this modification.
AI-49 adds that invariants need to be checked on the initialization of deferred constants (other initializations were already covered). An example is as follows
package R is
   type T is private
      with Type_Invariant => Non_Zero(T);
   function Non_Zero(X: T) return Boolean;
   Zero: constant T;
private
   type T is new Integer;
   function Non_Zero(X: T) return Boolean is
      (X /= 0);
   Zero: constant T := 0;
end R;
Currently, this is not caught but the declaration of Zero should raise Assertion_Error. Note the neat use of an expression function for the completion of Non_Zero.
AI-133 concerns default initializations and type invariants. Remember that initialization by default occurs in various circumstances. If a record type has components with an initial value as in
type R is
   record
      C: Integer := 99;
   end record;
then when we declare an object of type R without any initialization thus
X: R;
then we are assured that X.C will have the value 99. Moreover, in Ada 2012 we can give default values for other types by the new aspects Default_Value and Default_Component_Value (these are discussed in 3). But we cannot give defaults for existing predefined types such as Integer since we can only give the default when the type is declared.
The question arises as to whether or not the rule about default initializations being checked for the type invariant applies to an object declared inside the package body. Normally, of course, we can do what we like inside the body so we might expect such initializations not to be checked. However, since the default initialization mechanism is the same for clients outside the body as it is for the writer of the body, it was felt that it would be better if they were all checked for consistency and simplicity. An error might thus be detected earlier.
But there is an exception. If the partial view of the type has unknown discriminants then the user cannot declare objects of the type anyway and so no check could be performed externally. For uniformity no check is performed internally either.
AI-149 adds checks for functions whose return type is an access type with a designated type having a part of the type concerned (parameters were already covered). Further similar checks are added by AI-42 concerning type extensions. It is all a bit subtle and maybe other problems are lurking. One is tempted to quote a wee bonny poem of Sir Walter Scott
O what a tangled web we weave, When first we practise to deceive! 
A more exciting change (AI-41) is to allow Type_Invariant'Class on interface types. This can be used to ensure that any type derived from the interface satisfies certain properties. The following example is given
type Window is interface
   with Type_Invariant'Class =>
      Window.Width * Window.Height = 100;
function Width(W: Window) return Integer is abstract;
function Height(W: Window) return Integer is abstract;
This ensures that any type derived from the interface Window will provide functions giving the height and width of the windows such that their product is exactly 100. This is a display window of 100 pixels (poor quality I fear).
If we derive a type from several such interfaces then the Type_Invariant'Class is of course the conjunction of the individual invariants.
A new aspect Predicate_Failure is introduced by AI-54 (with a wording correction in AI-96). A related issue concerning the order of evaluation of predicates is discussed in AI-71. These were discussed in detail in the Ada 2012 Rationale and in Section 16.5 of Programming in Ada 2012. A short extract will suffice here.
The expected type of the expression defined by the aspect Predicate_Failure is String and gives the message to be associated with a failure. So we can write
subtype Open_File_Type is File_Type
   with
       Dynamic_Predicate => Is_Open(Open_File_Type),
       Predicate_Failure => "File not open";
If the predicate fails then Assertion_Error is raised with the message "File not open".
We can also use a raise expression (see AI-22 in the next section) and thereby ensure that a more appropriate exception is raised. If we write
       Predicate_Failure =>
          raise Status_Error with "File not open";
then Status_Error is raised rather than Assertion_Error with the given message. We could of course explicitly mention Assertion_Error thus by writing
       Predicate_Failure =>
          raise Assertion_Error with "A message";
Finally, we could omit any message and just write
       Predicate_Failure => raise Status_Error;
in which case the message is null.
A related issue is discussed in AI-71. If several predicates apply to a subtype which has been declared by a refined sequence then the predicates are evaluated in the order in which they occur. This is especially important if different exceptions are specified by the use of Predicate_Failure since without this rule the wrong exception might be raised. The same applies to a combination of predicates, null exclusions and old-fashioned subtypes.
There are a number of minor wording omissions and corrections with the description of predicates. AI-116 notes that one cannot give a specification of an aspect such as Dynamic_Predicate to both the full view and private view of a type (there is such a rule for most aspects but it was forgotten for predicates). A subtle point covered by AI-68 is that within a predicate the current instance (such as T in the expression Non_Zero(T) in the example of AI-49) acts like a value rather than an object. (This prevents certain undesirable uses of T such as applying a number of object attributes.) AI-99 confirms that not is an allowed operation in a Static_Predicate and also corrects some wording in relation to tasks and protected objects.
An interesting topic is addressed by AI-154. It may be recalled that rather than writing
package P is
   pragma Pure(P);
...
we can instead write
package P
   with Pure is
...
or more pedantically even
package P
   with Pure => True is
...
or really foolishly
package P
   with Pure => False is
...
Using a pragma rather than an aspect specification is the preferred style for library unit pragmas. But there might be some benefit in using an aspect specification since one could change the state of a whole group of packages in one blow by a structure such as
package State_Control is
   Purity: constant Boolean := True;
   ...
end State_Control;
...
with State_Control;
package P
   with Pure  => State_Control.Purity is
   ...
end P;
...          --  and so on for several packages
We could then make Purity false for adding some debugging material during development and then set it to true for final production.
Observe that AI-154 illustrates that one could be silly enough to try to write
package P with Pure => Purity is
   ...
   Purity: constant Boolean := True;    -- illegal
end P;
which raises the question of when is the wretched static expression Purity evaluated. The answer is immediately of course just like the pragma and so the example is illegal because Purity has not yet been elaborated. Note that aspects such as type invariants in
type Stack is private
   with Type_Invariant => Is_Unduplicated(Stack);
require the elaboration to be deferred. But this cannot be done with Pure because it controls the application of some Legality Rules.
The final AI-104 regarding aspects simply replaces a confusing sentence by a (confusing?) user note. Aspects such as Constant_Indexing can be inherited; the aspects themselves cannot be redefined but the functions they denote can be modified by overriding or by overloading.

Contents   Index   References   Previous   Next 
© 2016 John Barnes Informatics.