Strong Typing Yields Strong Programming

>> Website Resources
.. >> Library: TechXchange
.. .. >> TechXchange: Embedded Software
.. .. .. >> Topic: Ada and SPARK

The notion of strong typing often is associated with high-integrity and other critical applications. Indeed, in these cases, bugs may have a serious impact and any help coming from the language has great value. However, strong typing is not simply about avoiding bugs. It’s also about following sound software engineering principles and checking consistency at various levels. That is the moral of this story.

The Learning Curve

I joined AdaCore as an intern in 2002 and was tasked with developing the “quick fix” function in our integrated development environment (IDE). Being in the middle of my computer engineering studies and not yet familiar with some of the finer points of software development, I was susceptible to falling into some nasty programming traps.

In particular, I didn’t quite appreciate the difference between an offset to a character in a string and a column in an editor. Of course, most of the time, there is none—that is, until the IDE user presses the tab key and all of a sudden one string character may mean eight columns on the screen. Or seven. Or four. Or one…

Alas. Ten thousand lines of code and three years later, I returned to AdaCore, as an employee this time, tasked among other things with fixing my old intern code. In the meantime, the feature had been integrated within the IDE and did not perform that well in the presence of tabs.

In my code at the time, columns and buffer indexes were implemented as integers. There was no way to distinguish that they were being used for completely different purposes. They were representing objects that had completely different semantics in the system, but were using the same type.

As a result, it was impossible to track which part of the code was manipulating data as a column number, such as in a compiler message, and which part of the code was manipulating data as an index number, such as in a buffer modification. The implicit mix was resulting in various crashes and inconsistencies.

The Solution

That’s where the programming language can help. Ada lets developers define types that are semantically different, but share a compatible representation. Let’s take another example to illustrate this point. Miles and kilometers may be modeled using floating-point values. Adding a miles value and a kilometer value does not make sense, though. You would need to convert one unit into the other first—and deciding which one to convert depends on the locale.

This is exactly what Ada allows you to do. It’s going to forbid operations that implicitly convert from one type to another, even if they are structurally compatible, and force explicit conversions. Although that may feel like a notational burden at first, it relieves the developer from manual and error-prone consistency checks (see the figure). I’m pretty sure the guys from the Mars Climate Orbiter would agree.

Anyway, back to my problem. As I didn’t initially take this design aspect into account, the compiler could not detect any inconsistency. However, I could fix the design after the fact. I introduced two new types at the interfaces of my module, Offset_Type and Column_Type, one for manipulating offsets (in bare strings for example) and the other to manipulate columns (in the editor primitives). That generated a first layer of compiler errors in code where I was either mixing integers with offsets, or integers with columns.

By iteratively correcting the types of fields and variables along the way, I could specify correct typing in deep parts of the code. These chunks would have been completely obscure otherwise. Soon enough, I encountered locations where offsets and columns were mixed in computations. Those were the places where explicit conversions and computations needed to be made. In a matter of a few days, the code was completely repaired.

What I find surprising with this example is that it takes advantage of Ada features in a domain the language had not been specifically designed for—graphical interfaces and IDE design. But in this case, sound engineering principles and tools supporting these principles have proven to be effective in increasing productivity.