Channels ▼
RSS

Design

Ada 2012: Ada With Contracts


Preconditions, Postconditions, and Type Inheritance

Object-oriented programming raises an interesting issue in connection with pre- and postconditions. In a hierarchy of derived types (type derivation is Ada's mechanism for extending a type through inheritance), a parent type's subprogram may be overridden at each level, with each declaration providing its own set of pre- and postconditions. If such a subprogram is invoked on a polymorphic variable (class-wide, in Ada terms) of the root type, what can be assumed about the pre- and post-conditions that apply to the call?

It is certainly possible to regard a subprogram's preconditions for a derived type to be independent of those for the parent type (and, likewise, for the postconditions), so that the set that applies at runtime is determined by the actual subprogram being called. However, this approach can be problematic for formal verification, or even for informal analysis of the code, since you don't know at compile time which set of conditions will need to be met. The only preconditions and postconditions visible are the ones defined for the root type, and that should be the extent of the caller's obligation. If a derived type strengthens the root type's precondition or weakens the root type's postcondition, then the call (on an object of such a type) may fail.

One solution, embodied in Eiffel, is to consider that preconditions on derived types weaken the combined precondition to be applied (this basically corresponds to insisting that on any call, only the root type's preconditions need to be met). And the postconditions are correspondingly strengthened (which corresponds to considering that on return, at least the root type's postconditions must hold).

Ada 2012 has taken a similar approach through two additional constructs, Pre'Class and Post'Class, which automatically weaken the preconditions and strengthen the postconditions. This is done by automatically or'ing the ancestor types' preconditions for the given subprogram, and analogously and'ing the postconditions.

Other Contracts in Ada 2012

Besides preconditions and postconditions for subprograms, Ada 2012 supports several other kinds of contracts. One category involves predicates on types: conditions that must always be met by values of the type. One of the most important such predicates, ranges on scalar types, has been part of the language since Ada 83:

     Test_Score : Integer range 0 through 100;
     Distance : Float range -100.0 .. 100.0;

This capability (sadly missing from C, C++, Java, and many other languages) is extremely important for program understandability and reliability. It is hardly new (it's been part of Pascal for more than 40 years), but for some reason, it did not catch on in many other languages. And the consequences are significant. Many buffer overruns in C could be avoided if the language supported range constraints. An important project at Microsoft is to add such range declarations to the Windows code base. Hundreds of thousands of such statements have been added, and have detected a large number of potential buffer overruns.

Range constraints are important but limited in that they can capture only contiguous subranges of a scalar type's value space. Ada 2012 has generalized this concept: It enables the programmer to specify arbitrary subsets of a type's values through subtype predicates.

Ada 2012's subtype predicates come in two forms, Static_Predicate and Dynamic_Predicate, employed depending on the nature of the expression that defines the predicate. For example:

  type Month is 
    (Jan, Feb, Mar, Apr, May, Jun, Jul, Aug, Sep, Oct, Nov, Dec);
  
  subtype Long_Month is Month with
  Static_Predicate => Long_Month in Jan | Mar | May | Jul | Aug | Oct | Dec;
  
  subtype Short_Month is Month with
  Static_Predicate => Short_Month in Apr | Jun | Sep | Nov;  >>
  
  subtype Even is Integer with
  Dynamic_Predicate => Even rem 2 = 0;

The predicate is checked on assignment, analogous to range constraints:

  L : Long_Month := Apr;       -- Raises Constraint_Error
  E : Even := Some_Func(X, Y); -- Check that result is even

The static forms allow more compile-time checking. For example, in this case statement:

  case Month_Val is
     when Long_Month => …
     when Short_Month => …
  end case;

the compiler will detect that Feb is absent. Dynamic predicates cannot be checked at compile time, but violations can still be detected at runtime. In general, predicates require runtime checks; when you assign a Month value to a Short_Month variable, a runtime check verifies that it has an appropriate value.

Type Invariants

Another form of contract introduced by Ada 2012 is the type invariant. An invariant applies to a "private" type (somewhat analogous to "protected" in C++ and Java), which can be viewed from two perspectives. One is that of a client, or user, of the type, which can only access the type through subprograms supplied by the type and does not have access to its implementation details. The other viewpoint is that of the module (package) in which the private type is defined. This code has full access to the type's implementation details. A type invariant (for example, a table that is always sorted) ensures that values that are visible to clients are always appropriate, and that subprograms taking the type as parameter can rely on appropriate values being passed. Since the client cannot access the internals of a private type, there is no possibility for the client to corrupt this value. However, inside the implementation of the package defining the type, no such checks apply. This is important in practice because a complex object needs to be consistent after it has been constructed, but not at the intermediate stages as it is being built. Ada's private type interface provides exactly the partitioning that is needed to meet the two seemingly conflicting requirements: Sometimes, the values must be guaranteed to be consistent; and at other times, no such guarantees apply. As with preconditions and postconditions, predicates and invariants serve three possible purposes. They are formalized comments concerning the allowed values of variables. They can activate optional runtime checks that the required values are in fact present. Finally, they can act as a proof of correctness, which must show formally that appropriate values are being assigned.

Conclusion

As with all new versions of languages, Ada 2012 has many new features, but its most notable advance is the introduction of contracts, which will change the way that Ada can be used for constructing large-scale, highly reliable software. For programmers accustomed to pre- and postconditions in other languages, Ada 2012 will seem immediately familiar, although with some interesting new twists made possible by Ada's design. For others, it may require some education and practice. But for all users, the techniques of contract-based programming represent a significant advance.

Note: Students and developers of Free Software can gain access to a Free Software implementation of Ada 2012. This implementation is available for several targets, including Windows and Mac, as well as the Lego Mindstorm system, where contract-based programming can be put to effective use in robotics projects.


Robert Dewar is an emeritus professor of computer science at New York University and the president of AdaCore.


Related Reading


More Insights






Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

 
Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.
 

Video