What you say is what you get: an Ada story

Over the past 30+ years, Ada technology has matured into a unique toolset allowing programmers to achieve software reliability at a very affordable cost. It’s available for small microcontrollers such as ARM Cortex- M, large x86 64 hosted systems, and many things in between. Time to give it a try?

This article is contributed by AdaCore          Download PDF version of this article

At the risk of opening with platitudes, software development has become one of the most central engineering disciplines. Our lives are literally governed by software in quantities that defy imagination. As a matter of fact, our lives actually rely on this software. Drones, cars, medical devices, the list of things whose software can make the difference between life and death is growing by the day. How to avoid making this a list of threats? Truth is, software engineering is not about writing code. It’s about specifying intent, implementing what’s intended, and verifying that what’s implemented corresponds to what’s intended. And to do that, all environments and all languages are not equal.

Ada is a language that was first defined in the 80s, around the same time as C++. Unlike C++ though, which was designed as an evolution of C with extra expressivity capabilities, Ada was aimed at supporting the needs of high-criticality embedded software development. This led to a series of unique technical choices setting the language on a very different path. As a result, Ada tends to force programmers to be much more explicit when they write code, as the compiler will prefer to avoid compiling rather than guessing. Conversely, as opposed to other languages, Ada allows programmers to formally express intent that would be otherwise buried into comments.

This has two interesting consequences. First, many programming errors that would be difficult to avoid can be mitigated or eliminated. Second, it’s actually possible to go much further in making explicit expectations and intent at the software levels and either automatically enforce it or verify correct implementation. Here’s an example of what that may look like at low level:

This says quite a lot about a low-level data structure which is possibly used to map onto a device, or a data connection. It’s a sensor structure composed of Percent, which is a fixed-point value with a precision of 0.1, from 0 to 100 of 4 precision digits, stored in the first half-word of a 32 bits big-endian structure, and a flag that can only take 3 values, stored in the last 2 bits of that same structure. From this description, the compiler will actually verify that this representation can be implemented and if it does, guarantee that this specification will indeed be respected. Developers familiar with development of low-level layers can already see macro and bitwise operations headaches vanishing thanks to these features. In addition to this structural information, the type is associated with a constraint (or dynamic predicate) that states that when the flag Enabled is Off, Power has to be equal to 0. With assertion checking enabled, the compiler will generate consistency checks at appropriate places in the code, allowing the programmer to identify inconsistencies early.

On the opposite side of the spectrum, specification can be used to express functional constraints. The most common one is probably the precondition. The idea is that an assertion can be defined to be true when calling a function (or subprogram). A postcondition will specify the output of a function - its behaviour. Take for example:

The above defines a simple swap procedure on two elements on the array. One may expect that the indexes are within the range of the array. To avoid out of range array access, it’s tempting to write some defensive code within swap to detect the errant case and take appropriate measures - raise an exception or cancel the operation. But it should really be the responsibility of the caller to correctly call swap with two valid indexes. The precondition of this code allows the programmer to specify exactly that, thus removing the need for defensive code. It literally says I1 has to be within the range of A, and so does I2. On top of this, we also specify the outcome of the subprogram, that is the old value of A(I1) now equals to A(I2) and vice versa. So not only is there verification on the way in, to check that the code is properly called, but there’s also verification at the point of return, to check that the operation is doing what is expected. Also, note the parameter mode in out on the array: that specifies that Swap will modify the array, as opposed to I1 and I2 which are in (i.e., only input).

Preconditions, postconditions and other kinds of functional contracts (such as dynamic predicates as shown earlier) can be verified in many different ways. The obvious one is to ask the compiler to generate actual checks. This can be done selectively. All assertions could be kept during testing for example, and only a minimal amount kept after deployment. Even when inactive, these contracts can have merit just from the fact that they’re written and accepted by the compiler – i.e. they refer to actual entities and consistent operations. And they also serve as useful information to the human reader.

There’s however another way to do this verification that doesn’t even involve executing the code: static analysis. Better yet, formal proof. The SPARK language is a subset of the Ada language that is fit for static verification. Within the subset, any potential error will be analyzed and those that may happen will be reported. Every contract will be looked at taking into account all possible values, and those that might not be valid will be reported. In particular, SPARK can guarantee that every single call always respects the preconditions, and that every single subprogram always respects its postcondition.

And there’s more with Ada. Class hierarchies with verification that the behaviour defined at the root level is consistent with the behaviour of subclasses. Concurrency models with guarantees of absence of deadlocks. Specification of global variables - and more generally global states. Physical dimension consistency checking. Integer overflow elimination. The list goes on.

So who is using Ada today? While the language has a long-standing history in aerospace and defense, it’s now frequently being adopted outside its original area by a growing number of companies in other embedded domains. Some are in the very enviable situation of having projects to start from scratch. Adopting Ada or SPARK is very easy then, it’s merely a question of training and there’s nothing fundamentally difficult for a typical embedded developer. Most of those companies, however, have a significant investment in C or C++ code bases - or rely on components developed in those languages. So how do they migrate to Ada? Surely, bearing the costs of rewriting the whole code base offsets any benefits they may get.

Luckily, this is never a requirement. Ada is extremely amenable to language interfacing. As a matter of fact, often C and Ada compilers share most of their code (at least the part responsible for optimizing and generating assembly) making mixing those two an easy task. As an example, the swap function described already could actually come from a C library:

All we need to do is to tell Ada that this implementation is actually in C, specifying that it’s imported, of a C convention, and linked to a symbol swap:

Hey, isn’t that adding contracts to a C function? Note that although this interfacing code can be manually written, there are also binding generators available that would automatically take care of most of the burden (with the exception of addition of contracts). At the end of the day, only specific software components will be re-written in Ada, most legacy code can be kept. New modules developed in Ada can then be integrated with this legacy code. What you say is what you get. Software engineering is not about writing code, it’s about specifying intent, implementing it and ensuring that what has been implemented corresponds to what has been specified, with as little effort as possible.


The Benefits of C and C++ Compiler Qualification

In embedded application development, the correct operation of the compilation toolset is critical to the functional safety of the application. Two options are available to build trust in the corre...

An introduction to the SuperTest MISRA suites

The SuperTest MISRA suites are created to verify the conformance of MISRA checking software. The aim of a, so-called, MISRA checker is to check application software for its compliance with the MIS...

Coding safe and secure applications

The world is becoming far more connected, and systems are vulnerable to malicious attacks via these connections. Safety and security are different, but there are some common ways to achieve them i...

Data Distribution Service in autonomous car design

Builders of autonomous vehicles face a daunting challenge. To get a competitive edge, intelligent vehicle manufacturers must deliver superior driving experience while meeting demanding requirement...

Nine Steps to Choosing The Right Coding Standard

Selecting the right coding standard is an essential building block for safe and secure coding. While superficially many coding standards and automatic analysis tools may look similar, they can be quit...

Basics and tools for multi-core debugging

In the past, debugging meant seeking for variables written with wrong values. These days, it’s completely different: for the multi-core systems used nowadays in automotive control units, deb...


ZES Zimmer on testing advanced power electronics

In this video Bernd Neuner from ZES Zimmer talks to Alix Paultre for Electronic News TV at the 2017 Power Electronics Conference in Nuremberg. The discussion deals with the issues involving test and m...

Weidmüller discusses the need for a better signal and power interface

In this video Rene Arntzen from Weidmüller talks to Alix Paultre of Electronic News TV about the importance of a good signal and power interface for industrial equipment. There is currently no good ...

Mouser talks about the state of engineering development today

In this video Mark Burr-Lonnon and Graham Maggs of Mouser Electronics, a major international electronics distributor, talk to Alix Paultre about the state of engineering development today. With massiv...

Infineon launches a new family of configurable industrial drive boards

In this video Infineon explains their new family of configurable industrial drive boards at SPS-IPC Drives 2017. Intended to enable easy setup and deployment, the XMC-based automation boards can handl...

STMicro explains their STSPIN family of single-chip motor drivers

In this video STMicroelectronics explains their STSPIN single-chip motor drivers at SPS-IPC Drives 2017. The STSPIN family embeds can drive motors efficiently and with high accuracy, with an advanced ...