One of the most powerful features of Ada 2012* is the ability to specify contracts on your code. Contracts describe conditions that must be satisfied upon entry (preconditions) and upon exit (postconditions) of your subprogram. Preconditions describe the context in which the subprogram must be called, and postconditions describe conditions that will be adhered to by the subprogram’s implementation. If you think about it, contracts are a natural evolution of Ada’s core design principle. To encourage developers to be as explicit as possible with their expressions, putting both the compiler/toolchain and other developers in the best position to help them develop better code.

The addition of contracts into a standard Ada application accomplishes several elusive objectives; specifically, they act as a static method of handling potential errors, as documentation that gets updated and checked for consistency by the compiler alongside your code, and provide static analysis tools like SPARK and CodePeer with more application-specific detail they can use to produce higher-quality results. So let’s get started.

Here is a package with a simple subprogram that sets a property of a graph. One thing to notice about the graph from its definition is that its nodes are labelled with IDs from 1 to the number of nodes. In order to make sure that our subprogram doesn’t index into the graph’s list of nodes out of bounds, we might do a number of things. We can change Set_Source to a function that returns a boolean - True if the operation was successful, False if the supplied ID is out of range. Another option is to do nothing and make use of the default compiler-inserted array access check (I'll get into the drawbacks of this later), or we can even insert an explicit defensive check of our own if we want to raise a specific exception with a specific message.

However, all of these approaches come with two fundamental issues: they require additional documentation to be effective, and they rely on checks and/or exception handlers at run-time to prevent errors which can hurt performance. By adding a simple precondition, we can mitigate both of these problems at the same time.

The documentation issue is more obvious, so I’ll address that one first. Anyone using this API, even someone without access to the implementation, now knows that this subprogram expects to be called with the ID parameter in a specific range, yet no additional documentation is needed to express this. If we were using conventional methods, we would need another way to tell API users how to correctly use this subprogram. However, using contracts in this manner integrates the task of writing and updating documentation with the subprogram’s design process. On top of that, if the subprogram were to be redesigned, say if the Graph record type was broadened to accept characters as indices for Node_List, those new requirements would be reflected in the new preconditions, with no additional information needed.

In addition to helping other developers use your subprograms properly, contracts introduce a static methodology for dealing with errors. Conventionally, errors are dealt with via defensive checks and exception handlers at run-time. Particularly in an embedded context, where the final executable size in memory and computational demands need to be optimized, the reduction of run-time code is essential to dealing with hardware constraints. Accordingly, many programs have no choice but to trust that their testing infrastructure was sufficient and ship code with most run-time checks turned off. However, it’s not revolutionary to say that all programs wish their applications ran safely with less overhead. Using contracts provides an elegant way for developers higher in the call chain to take appropriate action to avoid violating known conditions that will cause program failure without adding run-time code at every level, as would happen with either explicit or compiler-inserted defensive checks or propagating exception handlers.

Sometimes though, as in the case of input validation, there’s no way to get around defensive code at run-time. Contracts provide the flexibility to add these checks both broadly and on a granular level. If you pass the ‘-gnata’ switch to the compiler, it will insert additional checks assuring your contracts are not violated alongside the standard Ada run-time checks, like range checks on types. However, if you just want to enable a single defensive check, you can do something like this:

The use of contracts can also increase organizational confidence that testing was in fact sufficient, and accounted for all the potential ways in which the application could fail. If you’re not at the level of statically verifying contracts to be unbreakable within the context of your application with SPARK, other static analysis tools, like CodePeer, can benefit from the extra information contracts provide about the intended use of your code. This is because in this context, contracts are language-level proxies of your application’s requirements, and CodePeer, like many other tools, only works on language-level constructs.

When CodePeer analyzes a subprogram, it generates implicit pre- and postconditions as part of the analysis. If one of those implicit contracts might be violated, you might get a message like this:

However, when you supply CodePeer with your own contracts to compare against,  it can output situations in which user-supplied contracts contradict some of its own, leading to more specific, more actionable findings, and fewer false positives. To learn more about contracts, check out this chapter from learn.adacore.com, or this section of the SPARK documentation.

*Contracts can also be used via pragma Precondition and pragma Postcondition with older versions of GNAT, or approximated with pragma Assert as defined in Ada 05. Learn more about that here.