Rationale for Ada 2012

John Barnes
Contents   Index   References   Search   Previous   Next 

2.1 Overview of changes: Contracts

The WG9 guidance document [1] identifies very large complex systems as a major application area for Ada. It further identifies four areas for improvements, one of which is
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
Type invariants
Subtype predicates
Aspect specifications
Aliasing predicates
Default initial values for types
Specifiable aspects
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 attributes
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, 229, 243, 267).
Then we discuss the introduction of pre- and postconditions on subprograms including the problems introduced by multiple inheritance (145, 230, 247, 254).
Two other related topics are type invariants and subtype predicates which provide additional means of imposing restrictions on types (146, 153, 250, 287, 289, 297).
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 (191).

Contents   Index   References   Search   Previous   Next 
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by:
The Ada Resource Association:


and   Ada-Europe: