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

January 29, 2013

Daniel Bigelow-January 29, 2013

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

Loading comments...

Parts Search Datasheets.com

KNOWLEDGE CENTER