Ada 2012: The Joy of Contracts

This article is part of the Embedded Software Series: Enforced Coding Using Ada Contracts

The relationship of a software developer to his or her programming language sometimes seems to follow an arc that is common in a romance/marriage: wild infatuation, a brief honeymoon, unrealistic expectations, realities and incompatibilities, and then separation or perhaps passionless cohabitation. The key question is, what next? A bitter divorce and a search for a new mate, or reconciliation and a renewed enthusiasm?

In the case of Ada, smart money is on the latter outcome, thanks to the new Ada 2012 standard recently approved by ISO (the International Organization for Standardization). For a while, the common perception of Ada was that of a niche language that was being replaced by sexier competition such as C++ and Java. This perception was rather distorted. Ada was still being used heavily (although perhaps without as much fanfare as in earlier times) in industries where reliability was critical. And importantly, the language was not standing still; it was undergoing some significant enhancements, responding to real user needs and taking into account the technological trends in both the software and hardware realms. Newly refreshed and rejuvenated, Ada is well poised to capture the hearts and minds of today's software developers.

The most exciting addition to Ada 2012 is the facility known as contract-based programming. The concept is straightforward: program elements such as subprograms are designed to satisfy specific software requirements ("contracts"), so the syntax of these program elements should support specifying such requirements. As a concrete example, the contract for a subprogram includes its preconditions (properties that the subprogram assumes on entry) and its postconditions (properties that the subprogram assures on exit). Figure 1 shows an example of the contracts associated with an insertion procedure for adding an element to a simple queue. Contracts may be checked statically by the compiler or a supplemental analysis tool, or enforced dynamically with run-time checks.

Queue : array (1..N) of Float;
Last : Integer := 0; -- Index of last element

procedure Insert(X : Float)
   with Pre => Last in 0 .. N-1,
       Post => Last in 1 .. N and Queue(Last) = X;

Contract-based programming is an increasingly important style of software development, especially in high-integrity systems where reliability, safety, and/or security are essential. It is amenable to static analysis and helps meet certification objectives such as the Formal Methods supplement to the DO-178C avionics software safety standard [1]. A tool can attempt to prove that a subprogram's postconditions are derivable from its preconditions, or find counterexamples otherwise. Contracts can also be used to show that a program will not have run-time errors. The idea of contracts is not new, but Ada is now the most widely used language that includes explicit support as part of the standard syntax and semantics (versus as stylized comments, for example). This means that the contracts are always in synch with the program and can be processed by any compiler that complies with the language standard.

Integrating contract-based programming with the language's existing facility for Object-Oriented Programming presented a challenge, in particular how to manage the interaction of inheritance with pre- and postconditions. Ada 2012 addresses this issue by supplying semantics consistent with a design approach known as the Liskov Substitution Principle [2], which in effect ensures that a subclass serves as a specialization of its superclass.

Beyond contract-based programming, Ada 2012 has added major enhancements in real-time scheduling, multiprocessor and multicore support, and the predefined library. The language revision also includes a variety of small improvements, along the lines of tidying up some loose ends.

The Ada design has always focused on reliability, readability, and early detection of errors. Ada 2012 is significant because these goals are becoming increasingly critical in today's software-intensive and interconnected world. Bugs that would have simply been inconveniences in standalone systems twenty years ago can now have far-reaching effects with major financial cost and perhaps even loss of life. In a sense, the software industry has caught up with Ada. Further, Ada 2012 features like contract-based programming are fun to use. The language revision recognized that notational expressiveness and convenience are important, so Ada 2012 supplies a natural and succinct (but readable) syntax including quantification and conditional expressions.

In short, if software developers take a fresh and thorough look at Ada 2012, a new spark may be kindled.

Read more from the Embedded Software Series: Enforced Coding Using Ada Contracts

References

1. RTCA /EUROCAE DO-178C/ED-12C. Software Considerations in Airborne Systems and Equipment Certification, December 2011.
2. B. Liskov and J. Wing. "A behavioral notion of subtyping", ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, Issue 6 (November 1994), pp 1811-1841.