Ada is a programming lan-guage well known in military and communication circles, though it has lost ground in recent times to C and C++. While there are some legitimate reasons to move in this direction, there are also quite a few arguments in favor of moving from C/C++ to Ada—especially Ada 2012.
Ada 2012 is the latest incarnation of the Ada language standard, incorporating a number of changes from previous versions. One of the most useful of these is contract support. Contracts are assertions for functions and procedures or types that specify pre- and post-conditions (Fig. 1). Even programmers unfamiliar with Ada can see clearly what is specified by the new contract support. These contracts can reference function and procedure arguments, thus indicating the type of operations that will be performed or checking the validity of parameters.
The idea behind contracts is not new. Ideally, they should improve programming practices and minimize bugs. They help encapsulate the purpose and operation of types and procedures. This type of information is often found in formal system definitions, but it is often up to the programmer to encode properly.
The initial Ada language version included strong typing (where assignments are checked statically to make sure both sides have compatible types), in addition to dynamic checking (to make sure assigned values are within the assigned range for a type). Ada 2005 added an Assert pragma that works like a C macro. A false condition raises the associated error message.
SPARK, a subset of Ada supporting formal proofs of program properties, initially implemented the pre- and post-condition checks in Ada 2012. These definitions are now part of the Ada language definition and implemented by the compiler, so that the way contracts work is standardized. While C and C++ programmers often use an assert macro to provide such checks, there is no standard associated with this approach. Also, macro placement is arbitrary and difficult for checking exit values. That is not the case with Ada 2012 post-conditions.
Ada’s post-condition can also utilize initial values. This would be difficult to implement using macros or other techniques. The S’Old.Entries value in Fig. 1 is an example of this. Type contracts utilize Ada 2012 subtype static and dynamic predicates (Fig. 2). A static predicate can be a compile time check for subtypes. For example, a programmer may require a type for even numbers. That is easy to define, but it would be hard to add checks for valid assignments. A dynamic predicate allows this check to be implemented by the compiler. The static version allows compile time checking to occur, such as determining whether a case statement enumerates all options.
The contract support in Ada 2012 is impressive. It allows the use of quantifiers, making it possible to specify that an array remain unchanged, or else changed in a specific fashion. Likewise, conditional and case expressions can be used in contract definitions.
Safe, reliable and secure programs are the goal of most programmers, and Ada’s contracts fit into this realm. They provide a level of control unattainable with other languages. Their portability is key for embedded applications that may need to target different hardware in the future. Perhaps it’s time to take out a contract with Ada 2012.
Assessing Ada 2012’s Additions
Ada is a high-level, object-oriented programming language initiated in the late 1970s under contract to and direction of the United States Department of Defense (DoD). The DoD was in search of a truly universal and secure code for its computers and electronic systems. This code was expanded from earlier programming languages, including Pascal, with the intent of creating an international standard language. Ada 2012 builds upon the foundation of the Ada 2005 standard, itself with many additions from a 1995 version of the code. In this latest version, modifications were made to improve reliability and readability of code.
As part of Ada 2012’s new “Programming by Contract” features, programmers are encouraged to be more precise in writing code by using more powerful predicates and—in general, more preconditions, postconditions, type invariants, and subtype predicates—to avoid ambiguities in language. Many of the latest enhancements to the Ada standards are designed for improved readability, using conditional expressions, case expressions, quantified expressions, and expression functions, mainly to simplify the writing of complex expressions. Some of the modifications in Ada 2012 were made for enhanced visibility of code, such as the use of incomplete types to simplify the construction of nested containers.
Copies of the new Ada reference manual are available at http://www.ada-auth.org/arm.html. The link leads to a webpage with additional links for the Ada 2012 Language Reference Manual (LRM), the Annotated Ada 2012 Language Reference Manual (AARM), the Ada Reference Manual Source Files, and the Ada Reference Manual Formatting Tool.