Ada 2012: say what you mean, mean what you say

One of the key capabilities in the new Ada 2012 standard is the contract-based programming model. Here's why.

To ensure the correctness and reliability of a software system, program elements, where appropriate, must define as precisely as possible things such as state, expected inputs, actual outputs, and a convincing argument to enforce the terms of usage. If this is not done, you or someone down the line will have to resort to guesswork and assumptions about how the system should behave.

Since incorrect assumptions are a major contributor to software defects, applications designed to mitigate the need for assumptions go a long way toward improving reliability. If however, the programming language is not expressive enough to enable a developer to precisely define the expectations, obligations, properties, and constraints of each program element, it's not likely that client programmers will make the correct assumptions in all possible cases to produce an overall satisfactory result.

We can compensate for missing features in a programming language by allocating sufficient resources for code reviews, regression tests, manual tests, and validation code in the application itself. However, these overhead activities are very labor-intensive, time-consuming, and represent a significant portion of a project's total cost. It is therefore highly desirable to minimize these costs while at the same time satisfying all functional and quality-assurance requirements.

Enter Ada 2012: a programming language designed to directly addresses the cost issues described above by providing mechanisms to enable programmers to precisely define the behavior of subprograms and the properties and constraints of types and subtypes.

Also, by eliminating the ambiguity factor, we increase the effectiveness of static analysis tools for early detection of potential problems such as program logic, data-flow inconsistencies, and runtime behavior, all of which reduces costs even further.

Ada 2012 contract-based programming model
Pre and post conditions

To illustrate the concept, consider the following subprogram interface:

     procedure  Push (S: in out  Stack; E: in  Element);

With this limited information we can only infer from the specification the input and output requirements. Hence, we must assume that the subprogram will push the read-only Element onto a read-write Stack , that the Stack has been implemented to detect and handle error conditions such as stack full, that the stack pointer is working correctly, and that the Push operation was successful.

Of course, high-integrity software cannot tolerate all those assumptions. Therefore the client programmer is obligated to find and study the implementation of Stack and all units in its closure in order to obtain sufficient assurance of its correctness. If the source code for the implementation of Push is not available then it can't be used–period.

Consider the same subprogram, but this time with the interface signature enhanced with a contract, where the obligations (pre-conditions) and benefits (post-conditions) are clearly stated:

procedure  Push (S: in out  Stack; E: in  Element) with  Pre => Not_Full (S),     Post => (S.Length = S'Old.Length + 1) and              (S.Data (S.Length) = E) and              (for all  J in  1 .. S'Old.Length => 
S.Data (J) = S'Old.Data (J));

With this interface specification, the client programmer does not need to make any assumptions. In addition, we now have sufficient information to make efficient use of tools supporting formal methods that are capable of performing compile and runtime analysis of the interface with respect to the implementation.

In addition, a useful side-effect of the contract mechanism is to limit the size and complexity of a subprogram, since, if a subprogram grows too large and tries to do too much, then formulating the contract becomes too difficult, thereby indicating the need to refactor.

Type invariants
The Ada contract model supports the concept of a class or type invariant , which is an assertion describing an unchangeable property that holds true for all instances. Or to put it another way, a class invariant is a statement of what it means for instances of a class to be valid. Without a class invariant in the contract a corrupt object can go unnoticed for an extended period of time, potentially causing a lot of damage.

A simple example of a type invariant is:

type  Square is  private
 with Type_Invariant => Width_Equals_Height (Square);

where Width_Equals_Height is a function implemented in the body of the package. The invariant is monitored by the Ada runtime from the perspective of the client, and if it fails (in other words, returns the value False ) then an Assertion_Error is raised.

Subtype predicates
This facility extends the notion of a range-constraint to provide an additional means of enforcing restrictions on types. The Ada runtime ensures that variables of these types only contain the specified values. If a violation occurs then a Constraint_Error is raised. Examples of subtype predicates are:

subtype  Even is  Integer  with  Dynamic_Predicate => Even mod  2 = 0;  subtype  Winter is  Month  with  Static_Predicate => Winter in  Dec | Jan | Feb;subtype  Pet is  Animal  with  Static_Predicate =>       (case  Pet is                 when  Cat | Dog | Horse => True,                when  Bear | Wolf => False);

Say it with Ada
By using the Ada 2012 contract model and exploiting the fact that every Ada construct is inherently safe, the language syntax and semantics allow you to “say what you mean” and the compiler and runtime will ensure that you “mean what you say.” In this regard, Ada 2012 may be thought of as a specification language that's capable of capturing, communicating, and executing detailed requirements.

This new capability has attracted an unusual amount of interest, so much so that I suspect the reason stems more from self-preservation than technical convenience. The ability to formulate iron-clad subprogram contracts, which are enforced by the runtime, serve to protect not only the application, but also the programmers who are highly exposed to discipline and litigation should a defect in their “handiwork” result in a catastrophe, such as loss of human life, economic damage, or a serious breach of security.

The Ada-2012 contract model allows developers to apply their knowledge of the domain and their reasoning powers to formulate strong contracts while leaving the tedious and error-prone job of enforcing these contracts to the technology.

To learn more visit www.ada2012.com and also “http://libre.adacore.com” where you can obtain the free open-source Ada 2012 development environment to start experimenting with Ada 2012's contract model.

Daniel Bigelow is an independent IT consultant located in Bern, Switzerland. His main area of interest concerns the implementation of highly-reliable systems where Ada technology plays an important role. He has more than 20 years of experience in all phases of the software development process in domains such as finance, telecommunications, air traffic management, defense, railway control, and instrumentation. He holds a bachelor's degree in electronic engineering and is the author of many video tutorials on Ada on AdaCore's tutorial page and on his own site, www.bigelow.ch/.

References:
1. AdaCore Newsletter, “GNAT Pro insider”, Autumn/Winter 2011-2012
2. John Barnes, “A brief introduction to Ada 2012, Chapter 1–Contracts and Aspects”, Ada User Journal , Volume 32, Number 4, December 2011

8 thoughts on “Ada 2012: say what you mean, mean what you say

  1. I really enjoy this article. In fact, this is subject that I have been studying and improving on. Regarding subtype predicates, you mentioned that Constraint_Error will be raised by the run time if the rules of subtype predicates are violated. However,

    Log in to Reply
  2. Nice article! These are some of the features that I really like from Ada2012 (those and the new iterator functionality). I'm curious about his comment, “This new capability has attracted an unusual amount of interest”. I'd like to know where the interest h

    Log in to Reply
  3. Of all the great features in the new language standard (Iterators included) discussions among my colleagues usually gravitate towards the contract model. Also the IT press seem to “get it” judging from the number of articles appearing on the subject. For e

    Log in to Reply
  4. Are your colleagues already Ada users? It would be nice to know if more non-Ada users became interested because it is a nice language that unfortunately often gets ignored. Every week I see portions of C code that just makes me shake my head in disbelief**

    Log in to Reply
  5. Yes, most of my colleagues are Ada users, but as we all know, the presence of C-family code in most large projects is difficult to avoid. Fortunately Ada and C get along quite well, despite cultural differences.

    I think most developers would rather inter

    Log in to Reply
  6. Contracts are definitely a good way to ensure that simple functions actually do what they are supposed to.

    How are more complex functions handled? I guess the trick is that pre and post conditions handle certain classes of bug really well and others are b

    Log in to Reply
  7. A well-written subprogram contract and the associated implementation that manages to get past the compiler and static analyzer is not necessarily free of defects. As you pointed out, the next line of defense is handled by the unit-tests. These are particul

    Log in to Reply

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.