Rationale for Ada 2012
2.1 Overview of changes: Contracts
The WG9 guidance document 
identifies very large complex systems as a major application area for
Ada. It further identifies four areas for improvements, one of which
Improving the ability to write and enforce
contracts for Ada entities (for instance, via preconditions).
The idea of contracts has been a cornerstone of programming
for many years. The very idea of specifying parameters for subroutines
is a simple form of contract going back to languages such as Fortran
over half a century ago.
More recently the idea of contracts has been brought
to the fore by languages such as SPARK and Eiffel.
SPARK is, as many readers will be aware, a subset
of Ada with annotations providing assertions regarding state embedded
as Ada comments. The subset excludes features such as access types and
dynamic dispatching but it does include Ravenscar tasking and generics.
The subset was chosen to enable the contracts to be proved prior to execution.
Thus SPARK is a very appropriate vehicle for real programs that just
have to be correct because of concerns of safety and security.
Eiffel, on the other hand, is a language with a range
of dynamic facilities much as in Ada and has found favour as a vehicle
for education. Eiffel includes mechanisms describing contracts which
are monitored on a dynamic basis at program execution.
The goal of this amendment to Ada is to incorporate
matters such as pre- and postconditions but with the recognition that
they are, like those in Eiffel, essentially for checking at runtime.
Adding pre- and postconditions and similar features
has had quite a wide ranging impact on Ada and has required much more
flexibility in many areas such as the form of expressions which will
be addressed in later chapters.
The following Ada issues
cover the key changes and are described in detail in this chapter:
Pre- and postconditions
Default initial values for types
Inheritance of null procedures with precondition
Clarification of categorization
Preconditions, postconditions, multiple inheritance and dispatching calls
Thoughts on type invariants
Do we really have contracts right?
Improvements for aspect specifications
Some questions on subtype predicates
Invariants and in mode parameters
First_Valid and Last_Valid
These changes can be grouped as follows.
First we lay the syntactic foundations necessary
to introduce features such as preconditions by discussing aspect specifications
which essentially replace or provide an alternative to pragmas for specifying
many features (183
Then we discuss the introduction of pre- and postconditions
on subprograms including the problems introduced by multiple inheritance
Two other related topics are type invariants and
subtype predicates which provide additional means of imposing restrictions
on types (146
Finally, two auxiliary features are the ability to
provide default values for scalar types and array types (228
and means of checking that aliasing does not occur between two objects
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by: