Rationale for Ada 2012
1.3.1 Overview: Contracts
One of the important issues highlighted by WG9 for
the Amendment was the introduction of material for enforcing contracts
such as preconditions and postconditions. As a simple example consider
a stack with procedures
Push and
Pop.
An obvious precondition for
Pop is that the
stack must not be empty. If we have a function
Is_Empty
for testing the state of the stack then a call of
Is_Empty
would provide the basis for an appropriate precondition.
The question now is to find a good way to associate
the expression not Is_Empty with the
specification of the procedure Pop. Note that
it is the specification that matters since it is the specification that
provides the essence of the contract between the caller of the procedure
Pop and the writer of its body. The contract
provided by a traditional Ada subprogram specification is rather weak
– essentially it just provides enough information for the compiler
to generate the correct code for the calls but says nothing about the
semantic behaviour of the associated body.
The traditional way to add information of this kind
in Ada is via a pragma or by giving some kind of aspect clause. However,
there were problems with these approaches. One is that there is no convenient
way to distinguish between several overloaded subprograms and another
is that such information is given later on because of interactions with
freezing and linear elaboration rules.
Accordingly, it was
decided that a radical new approach should be devised and this led to
the introduction of aspect specifications which are given with the item
to which they relate using the reserved word with.
In the case of preconditions and postconditions,
Ada 2012 introduces aspects
Pre and
Post.
So to give the precondition for
Pop we augment
the specification of
Pop by writing
procedure Pop(S: in out Stack; X: out Item)
with Pre => not Is_Empty(S);
In a similar way we
might give a postcondition as well which might be that the stack is not
full. So altogether the specification of a generic package for stacks
might be
generic
type Item is private;
package Stacks is
type Stack is private;
function Is_Empty(S: Stack) return Boolean;
function Is_Full(S: Stack) return Boolean;
procedure Push(S: in out Stack; X: in Item)
with
Pre => not Is_Full(S),
Post => not Is_Empty(S);
procedure Pop(S: in out Stack; X: out Item)
with
Pre => not Is_Empty(S),
Post => not Is_Full(S);
private
...
end Stacks;
Note how the individual
aspects Pre and Post
take the form of
aspect_mark => expression
and that if there are
several then they are separated by commas. The final semicolon is of
course the semicolon at the end of the subprogram declaration as a whole.
Thus the overall syntax is now
subprogram_declaration ::=
[overriding_indicator]
subprogram_specification
[aspect_specification] ;
and in general
aspect_specification ::=
with aspect_mark [ => expression] { ,
aspect_mark [ => expression] }
Pre- and postconditions
are controlled by the same mechanism as assertions using the pragma
Assert.
It will be recalled that these can be switched on and off by the pragma
Assertion_Policy.
Thus
if we write
pragma Assertion_Policy(Check);
then assertions are enabled whereas if the parameter
of the pragma is Ignore then all assertions
are ignored.
In the case of a precondition, whenever a subprogram
with a precondition is called, if the policy is Check
then the precondition is evaluated and if it is False
then Assertion_Error is raised and the subprogram
is not entered. Similarly, on return from a subprogram with a postcondition,
if the policy is Check then the postcondition
is evaluated and if it is False then Assertion_Error
is raised.
So if the policy is Check
and Pop is called when the stack is empty
then Assertion_Error is raised whereas if
the policy is Ignore then the predefined exception
Constraint_Error would probably be raised
(depending upon how the stack had been implemented).
Note that, unlike the pragma Assert,
it is not possible to associate a specific message with the raising of
Assertion_Error by a pre- or postcondition.
The main reason is that it might be confusing with multiple conditions
(which can arise with inheritance) and in any event it is expected that
the implementation will give adequate information about which condition
has been violated.
Note that it is not permitted to give the aspects
Pre or Post for
a null procedure; this is because all null procedures are meant to be
interchangeable.
There are also aspects
Pre'Class
and
Post'Class for use with tagged types (and
they can be given with null procedures). The subtle topic of multiple
inheritance of pre- and postconditions will be discussed in detail in
Section
2.3.
Two new attributes are useful in postconditions.
X'Old denotes the value of
X
on entry to the subprogram whereas
X denotes
the value on exit. And in the case of a function
F,
the value returned by the function can be denoted by
F'Result
in a postcondition for
F.
As a general rule, the new aspect specifications
can be used instead of aspect clauses and pragmas for giving information
regarding entities such as types and subprograms.
For example rather
than
type Bit_Vector is array (0 .. 15) of Boolean;
followed later by
for Bit_Vector'Component_Size use 1;
we can more conveniently
write
type Bit_Vector is array (0 .. 15) of Boolean
with Component_Size => 1;
However, certain aspects such as record representation
and enumeration representations cannot be given in this way because of
the special syntax involved.
In cases where aspect specifications can now be used,
the existing pragmas are mostly considered obsolescent and condemned
to Annex J.
It should be noted
that pragmas are still preferred for stating properties of program units
such as Pure, Preelaborable
and so on. However, we now talk about the pure property as being an aspect
of a package. It is a general rule that the new aspect specifications
are preferred with types and subprograms but pragmas continue to be preferred
for program units. Nevertheless, the enthusiast for the new notation
could write
package Ada_Twin
with Pure is
end Ada_Twin;
which illustrates that in some cases no value is
required for the aspect (by default it is True).
A notable curiosity is that Preelaborable_Initialization
still has to be specified by a pragma (this is because of problems with
different views of the type).
Note incidentally that to avoid confusion with some
other uses of the reserved word with, in the case of aspect specifications
with is typically written at the beginning of the line.
There are two other new facilities of a contractual
nature concerning types and subtypes. One is known as type invariants
and these describe properties of a type that remain true and can be relied
upon. The other is known as subtype predicates which extend the idea
of constraints. The distinction can be confusing at first sight and the
following extract from one of the Ada Issues might be helpful.
“Note that type invariants are not the same
thing as constraints, as invariants apply to all values of a type, while
constraints are generally used to identify a subset of the values of
a type. Invariants are only meaningful on private types, where there
is a clear boundary (the enclosing package) that separates where the
invariant applies (outside) and where it need not be satisfied (inside).
In some ways, an invariant is more like the range of values specified
when declaring a new integer type, as opposed to the constraint specified
when defining an integer subtype. The specified range of an integer type
can be violated (to some degree) in the middle of an arithmetic computation,
but must be satisfied by the time the value is stored back into an object
of the type.”
Type invariants are
useful if we want to ensure that some relationship between the components
of a private type always holds. Thus suppose we have a stack and wish
to ensure that no value is placed on the stack equal to an existing value
on the stack. We can modify the earlier example to
package Stacks is
type Stack is private
with
Type_Invariant => Is_Unduplicated(Stack);
function Is_Empty(S: Stack) return Boolean;
function Is_Full(S: Stack) return Boolean;
function Is_Unduplicated(S: Stack) return Boolean;
procedure Push(S: in out Stack; X: in Item)
with
Pre => not Is_Full(S),
Post => not Is_Empty(S);
-- and so on
The function Is_Unduplicated
then has to be written (in the package body as usual) to check that all
values of the stack are different.
Note that we have mentioned Is_Unduplicated
in the type invariant before its specification. This violates the usual
"linear order of elaboration". However, there is a general
rule that all aspect specifications are only elaborated when the entity
they refer to is frozen. Recall that one of the reasons for the introduction
of aspect specifications was to overcome this problem with the existing
mechanisms which caused information to become separated from the entities
to which it relates.
The invariant on a
private type T is checked when the value can
be changed from the point of view of the outside user. That is primarily
after default initialization of an object of type
T,
after a conversion to type T,
after a call that returns a result of a type T
or has an out or in out or access parameter of type T.
The checks also apply to subprograms with parameters
or results whose components are of the type T.
In the case of the stack, the invariant Is_Unduplicated
will be checked when we declare a new object of type Stack
and each time we call Push and Pop.
Note that any subprograms internal to the package
and not visible to the user can do what they like. It is only when a
value of the type Stack emerges into the outside
world that the invariant is checked.
The type invariant could be given on the full type
in the private part rather than on the visible declaration of the private
type (but not on both). Thus the user need not know that an invariant
applies to the type.
Type invariants, like pre- and postconditions, are
controlled by the pragma
Assertion_Policy
and only checked if the policy is
Check. If
an invariant fails to be true then
Assertion_Error
is raised at the appropriate point.
There is also an aspect
Type_Invariant'Class
for use with tagged types.
The subtype feature of Ada is very valuable and enables
the early detection of errors that linger in many programs in other languages
and cause disaster later. However, although valuable, the subtype mechanism
is somewhat limited. We can only specify a contiguous range of values
in the case of integer and enumeration types.
Accordingly, Ada 2012 introduces subtype predicates
as an aspect that can be applied to type and subtype declarations. The
requirements proved awkward to satisfy with a single feature so in fact
there are two aspects:
Static_Predicate and
Dynamic_Predicate. They both take a
Boolean
expression and the key difference is that the static predicate is restricted
to certain types of expressions so that it can be used in more contexts.
Suppose we are concerned
with seasons and that we have a type Month
thus
type Month is
(Jan, Feb, Mar, Apr, May, ..., Nov, Dec);
Now suppose we wish
to declare subtypes for the seasons. For most people winter is December,
January, February. (From the point of view of solstices and equinoxes,
winter is from December 21 until March 21 or thereabouts, but March seems
to me generally more like spring rather than winter and December feels
more like winter than autumn.) So we would like to declare a subtype
embracing Dec, Jan
and Feb. We cannot do this with a constraint
but we can use a static predicate by writing
subtype Winter is Month
with Static_Predicate => Winter in Dec | Jan | Feb;
and then we are assured that objects of subtype Winter
can only be Dec, Jan
or Feb (provided once more that the Assertion_Policy
pragma has set the Policy to Check).
Note the use of the subtype name (Winter)
in the expression where it stands for the current instance of the subtype.
The aspect is checked whenever an object is default
initialized, on assignments, on conversions, on parameter passing and
so on. If a check fails then Assertion_Error
is raised.
The observant reader will note also that the membership
test takes a more flexible form in Ada 2012 as explained in the next
section.
If we want the expression to be dynamic then we have
to use Dynamic_Predicate thus
type T is
... ;
function Is_Good(X: T) return Boolean;
subtype Good_T is T
with Dynamic_Predicate => Is_Good(Good_T);
Note that a subtype
with predicates cannot be used in some contexts such as index constraints.
This is to avoid having arrays with holes and similar nasty things. However,
static predicates are allowed in a for loop meaning to try every value.
So we could write
for M in Winter loop...
Beware that the loop uses values for M
in the order, Jan, Feb,
Dec and not Dec,
Jan, Feb as the
user might have wanted.
As another example,
suppose we wish to specify that an integer is even. We might expect to
be able to write
subtype Even is Integer
with Static_Predicate => Even mod 2 = 0; -- illegal
Sadly, this is illegal
because the expression in a static predicate is restricted and cannot
use some operations such as mod. We have to use a dynamic predicate
thus
subtype Even is Integer
with Dynamic_Predicate => Even mod 2 = 0; --OK
and then we cannot
write
for X in Even loop ...
but have to spell it
out in detail such as
for X in Integer loop
if X mod 2 = 0 then --or if X in Even then
... -- body of loop
end if;
end loop;
The assurance given
by type invariants and subtype predicates can depend upon the object
having a sensible initial value. There is a school of thought that giving
default initial values (such as zero) is bad since it can obscure flow
errors. However, it is strange that Ada does allow default initial values
to be given for components of records but not for scalar types or array
types. This is rectified in Ada 2012 by aspects
Default_Value
and
Default_Component_Value. We can write
type Signal is
(Red, Amber, Green)
with Default_Value => Red;
type Text is new String
with Default_Component_Value => Ada.Characters.Latin_1.Space;
type Day is
range 1 .. 31
with Default_Value => 1;
Note that, unlike default initial values for record
components, these have to be static.
Finally, two new attributes
are introduced to aid in the writing of preconditions. Sometimes it is
necessary to check that two objects do not occupy the same storage in
whole or in part. This can be done with two attributes thus
X'Has_Same_Storage(Y)
X'Overlaps_Storage(Y)
As an example we might
have a procedure Exchange and wish to ensure
that the parameters do not overlap in any way. We can write
procedure Exchange(X, Y: in out T)
with Pre => not X'Overlaps_Storage(Y);
Attributes are used rather than predefined functions
since this enables the semantics to be written in a manner that permits
X and Y to be of
any type and moreover does not imply that X
or Y are read.
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by: