The most recent version of the Ada standard, known as Ada 2012, brings contract-based programming to a mainstream language. Preconditions, postconditions, type invariants, and subtype predicates allow software developers to specify their programs' intent more clearly, in effect embedding requirements into the source code. This feature makes it easier to review and understand the program, and it facilitates verification by the compiler, static analysis tools, and/or runtime checks.
"New, Improved" or "No, Unproved"?
In the software world, we are used to getting new versions of things all the time. Nearly every software product undergoes frequent revision, and companies dutifully trot out press releases to trumpet the wonderful new features in each version. In practice, these updates are often not that significant or newsworthy.
Programming languages follow a similar revision pattern. For example, a new version of C, referred to as C11, was released last year. New versions of languages typically have many new features, and to those in the language design business, these always seem like major advances. However, the wonderful improvements often don't make that much difference in practice. Indeed the style of a lot of C coding has not much changed since the Kernighan and Ritchie days 35 years ago. Most C programmers don't use the new features in C99, let alone the ones that recently appeared in C11.
Ada is no exception to the rule of periodic updates and is subject to the same caveat that often these revisions have "nothing earth-shaking" to offer. For example, Ada 2005, the previous version of the standard, introduced many new features that those of us working on the language felt were very important advances, but most Ada programmers stayed with Ada 95. The Ada 95 version of the language, by the way, upgraded the original Ada 83 standard with significant functionality including full support for OOP. When an undertaking of comparable magnitude was carried out for C, a language with a new name was born.
A Seismic Shift
All of this leads us to Ada 2012, the latest version of the Ada language standard, formally approved by the ISO in December 2012. Is this really an important development or simply a "new version yawn"? I could certainly supply a catalog of new features, and you can find articles that do just that. But Ada 2012 does bring an "earth-shaking" advance the introduction of contract-based programming, or what Eiffel programmers call "design by contract."
In the context of software, a "contract" is an assertion of some property of a program component reflecting a requirement that the component must meet. This is a fairly general definition; some specific examples, to be covered later, are preconditions and postconditions (which apply to subprograms, that is, functions and procedures), and invariants and predicates (which apply to types).
The concept isn't new. What is new with the inclusion of this facility in Ada is its spread into the broader domains of high-reliability, safety-critical, and security-critical programming. These are areas where Ada has a significant presence. (For example, the newly deployed iFacts Air Traffic Control program in England is programmed in SPARK, a high-integrity Ada subset augmented with annotations. Ada is widely used on new aircraft, both military and civilian.)
The notion of a contract is fundamental to improving a program's reliability (that is, giving increased confidence that it correctly meets its requirements). From a broader perspective, the software development process involves defining a set of high-level requirements, deriving low-level requirements, formulating a software architecture/design that meets these requirements, and writing code that implements the design. This process is not necessarily sequential (feedback/iteration is common) and may be more or less formalized.
Contracts help bridge the gap between low-level requirements and the code. They also create formal documentation of how the code relates to these requirements. Two of the most important kinds of contract are a subprogram's preconditions (which must be true on entry) and postconditions (which must be true on exit). Again, these are not unique to Ada. Their usage was well established, particularly in the area of formal proof of correctness. However, major programming languages have been slow to adopt these concepts.
Capturing Preconditions and Postconditions
Preconditions and postconditions are most easily understood in the context of an example. Assume a program has to process arrays of integers, and one required operation is to remove duplicate elements from a given array. In Ada, this entails defining an array type, then a subprogram to perform the removal:
type Int_Array is array (Natural range <>) of Integer; procedure Dedupe (Arr: in out Int_Array; Last : out Natural);
Int_Array declaration allows different objects of the type to be created with different bounds; the lower bound can be any non-negative integer (
Arr is an object of type
Int_Array, then its bounds can be queried by the constructs
Arr'First (lower bound) and
Arr'Last (upper bound).
Dedupe needs to meet the following requirements:
- On entry, the parameter
Arrcontains at least one duplicated element.
- On exit, all duplicates (and only the duplicates) have been removed, nothing new has been added, and the parameter
Lastshows the new upper bound.
English comments could be added to the source code to express these requirements, but Ada 2012 supports much more precision through preconditions and postconditions:
procedure Dedupe (Arr: in out Int_Array; Last : out Natural) with Pre => Has_Duplicates(Arr), Post => not Has_Duplicates( Arr(Arr'First .. Last) ) and then (for all Item of Arr'Old => (for some J in Arr'First .. Last => Item = Arr(J))) -- Only duplicates removed and then (for all J in Arr'First .. Last => (for some Item of Arr'Old => Item = Arr(J))); -- Nothing new added
where the helper function
Has_Duplicates can be defined as follows:
function Has_Duplicates(Arr : Int_Array) return Boolean is begin return (for some I in Arr'First .. Arr'Last-1 => (for some J in I+1 .. Arr'Last => Arr(I)=Arr(J))); end Has_Duplicates;
The pre- and postconditions make use of quantification syntax introduced in Ada 2012. They precisely specify what the
Dedupe procedure does without constraining how it is implemented. The example also illustrates that the value of a parameter on entry to the subprogram (
Arr'Old) can be referenced in a postcondition.
If youare just writing comments in English, achieving completeness and precision is a formidable challenge; but that's a critical part of making sure that the code meets low-level requirements. Expressing the requirements as contracts forces precision, and the analysis required may help tease out pre- or postconditions that otherwise might be overlooked (for example, the terms in the postcondition corresponding to "only duplicates removed" and "nothing new added"). Such "forgotten" conditions correspond to very typical bugs.
Using Preconditions and Postconditions
Once you get into the habit of including contracts with subprograms, how do you make use of them? There are three principal styles of usage.
First, they can act simply as a substitute for English language comments to guide a human reader in understanding the code. In this context, they perform the same function as comments, but with the great advantage of unambiguity and much higher precision. At first glance, this may seem equivalent to simply reading the source code of the subprogram to see what it does. However, contracts are different in two crucial respects: The contracts are at a much higher level of abstraction; and most importantly, the contracts specify everything that is needed and nothing more. Several implementations of
Dedupe are possible; some would leave the order unchanged and some might leave it sorted. If you relied only on the code, you might infer that one of these two possibilities was part of the requirements, but that would be wrong.
The second use of contracts is to enable the compiler to turn them into runtime checks optionally. Testing then does not simply check the final results of the program, but also verifies on entry and exit from each subprogram that the code is doing what it is supposed to do. A runtime exception (a well-defined concept in Ada) is raised if a precondition or postcondition fails. Typically, such an exception occurrence will precisely identify the test that fails, thereby easing the debugging process. Like all runtime checks, these checks can optionally be removed for the final production build. This is often done in safety-critical applications such as aircraft software, where the verification process provides sufficient confidence that the checks will not fail. (And in any event, it would not be much help to the pilot to get a message on the screen saying that some precondition has failed!) In this context, the runtime checks are a means to the end of making sure they are not needed. But in other contexts, if the extra inefficiency is not a problem, it may well make sense to leave the checks enabled. Better to have an ATM machine shut down than to get an undetected error and hand out the wrong amount of money.
Finally, contracts can be used as a basis for formal verification. The
Dedupe procedure in our example includes a set of preconditions and postconditions expressed in quantificational logic; you (or your automated tools) can have a formal understanding of these conditions and of the code that implements the procedure. The process of proving that the code does in fact guarantee that the postconditions hold on exit if the preconditions hold on entry is explicitly defined. Very often in proofs of correctness, the critical issue is knowing what to prove. The systematic use of contracts allows this question to be answered precisely, and also allows the proof to be carried out in a modular fashion. The
Dedupe procedure can be proved correct in isolation, and then callers must ensure that the preconditions are met. It is also possible to combine testing and proving in the same program, conveniently using the contracts as a boundary between the two. For example, you might prove the
Dedupe procedure correct, but rely on testing to verify that the preconditions are met on each call. Such a synthesis between formal methods and testing shows great promise.