Good contracts make good programs

May 01, 2007

JackGanssle-May 01, 2007

Is Design by Contract just a fancy name for the tried and tested assert( ) macro? No!

This is the third of three installments about Design by Contract (DBC, a trademark of Eiffel Software), in my opinion one vastly ignored yet tremendously powerful way to stamp out bugs. To very briefly reiterate: DBC is like assertions on steroids. With DBC one defines contracts, which are assertion-like statements about functions' input and output parameters (pre- and postconditions), as well as things that never change throughout the execution of the function (invariants). On their wedding day, the betrothed say "I do;" they enter into a contractual arrangement that is an invariant underlying all of their future relationship.

Although contracts do look at lot like assertions, there is an important philosophical difference. An assertion makes a statement about what the programmer thinks is true at one particular time or place in the code. A contract, however, is a strong statement about the relationship of the function to its caller. For instance, something is profoundly wrong if a routine calls a square-root function with a negative argument. Or is there? If sqrt() understands complex math, a different set of assumptions, and thus contracts, defines the relationship between caller and callee.

The right contracts prove that the programmer hasn't made incorrect assumptions about code's behavior, a particular bane of reuse. As Bertrand Meyer said, "Reuse without a contract is sheer folly."1

Set contracts on "impossible" conditions, things that just can't happen, like pulling data from an empty queue or getting a null pointer to a string. A contract stops execution immediately, long before these errors can precipitate a potentially worse failure, producing debugging hints that help us fix things fast.

Place contracts on conditions for which there is no recovery. That excludes incorrect user input, as the code should complain and prompt for better data. If it's possible to retry in some manner, write the appropriate recovery code and don't use a contract.

Thus, there is no recovery from a broken contract. Fail fast; fail safe. Place the system in a safe mode and then halt. Log the error so developers can see what went wrong when, printing or displaying the error if possible, or stuffing the error into flash for later analysis.

In general, contracts shouldn't break in the field. Good design and aggressive testing should wring out such problems before shipping. It's best to deal with hardware failures using normal code. If the 5 V analog-to-digital converter returns 6 V, give the user a clear error message so there's no doubt what needs to be fixed.

DBC for C
In part two of this series I described Charlie Mills' DBC for C package, which preprocesses C modules to turn contracts embedded in comments into compileable C code. It works well and offers a lot of value, but is written in Ruby, which may not be available on all systems. And, to me at least, the structure of the code is completely inscrutable, making it hard to impossible to extend and maintain. Other options exist.

Falling back to Eiffel's DBC syntax, one can write require() (precondition) and ensure() (postcondition) macros. I have no idea how to create an invariant without using some sort of preprocessor, but you could embed the invariant's tests in the two new macros. Use:


void assert(int);
#define require(a) 
    ((void)(a), assert(a))
#define ensure(a)  
    ((void)(a), assert(a))
Why the double arguments? Contracts should have no side effects. The assignment operator "=" and function calls aren't allowed. Couple the above definition with the use of Lint to flag a contract that uses assignments or function calls. (You do use Lint, don't you? It's an essential part of any development environment.) Using Gimpel's Lint (www.gimpel.com), add this command to the code:

//lint -emacro(730,require)
so Lint won't complain about passing Booleans to functions. Now, Lint will be happy with a contract like:

require(n >=0);
But will give warning 666 ("expression with side effects") for contracts like:

require(m=n);
or

require(g(m));

Contracts are also a form of documentation since they clearly describe the limits of a function's behavior. There's some merit in substituting constructs familiar only to C programmers with more English-like words, so I like to define AND and R corresponding to && and ||, using the former in writing contracts.

The gnu Nana project offers another alternative.2 It's a collection of DBC-like constructs that do ultimately resolve to error handlers. These error handlers are little different from assert() macros, but they're well thought out with an eye to the limited resources typical of embedded systems. One option enables contracts using gdb resources, greatly reducing the overhead required by assert()'s traditional __line__ and __file__ parameters. Support of a limited amount of predicate calculus lets one define quite involved contracts.

Nana's use of I() for invariants and other too-short, cryptic nomenclature is a mistake. Worse is that it supports assignment and function calls in contracts. But it's worth reading the (alas, all too limited) documents and code at the web site.2

At least one commercial DBC product supports C and C++. The 249-euro C2 from Aechmea ties tightly to Microsoft's Visual Studio and preprocesses C files to convert contracts embedded in comments to code.3

The keywords are @pre, @post, and @invariant.

A free Linux version is available, but the license limits its use to noncommercial work.

Aechmea's product works well; I'd be enthusiastic about it, except for it's limiting Linux license and Windows operation solely with Visual Studio.

I started this series mentioning Eiffel, a language that includes a complete DBC mechanism. Yet Eiffel has only a microscopic presence in the embedded space. SPARK, a subset of Ada, is an intriguing alternative that includes precompile-time contract checking.4 That's not a misprint; it has an extremely expressive contract language that transcends the simple invariants, pre- and post-conditions discussed here. SPARK's analysis tools examine the code before compilation, flagging any state the code can enter that will break a contract. That's a fundamentally different approach to the run-time checking of contracts, and to debugging in general. If you carefully define the contracts and fix any flaws detected by the tools, the SPARK tools can guarantee your program free from large classes of common defects, including all undefined and implementation-dependent behaviors, data-flow errors and so-called "run-time errors" like buffer overflow, arithmetic overflow, and division by zero.

Finally, this magazine's own Dan Saks wrote a very interesting article about building compile-time assertions—again, constructs that catch some classes of errors while you compile, without the use of external tools.5 The approach is not nearly as comprehensive as DBC, but it's a fascinating way to use the preprocessor to stomp out bugs early.

Stop the madness
February's snowstorms generated a flurry of flight cancellations. Figure 1 shows that, though cancelled, my flight to Chicago was still expected to arrive on time. Clearly, we programmers continue to labor under the illusion that, once a little testing is done, the code is perfect.

Is Design by Contract just a fancy name for the tried and tested assert() macro? I, and many others, argue no even though some C implementations merely expand DBC's keywords into assert() or a construct very much like it. DBC represents a different philosophy about writing programs. Programmers sprinkle assertions about wherever the spirit moves them (which usually means not at all). In DBC we define a function's behavior, to a certain extent, by the contracts. Functions routinely start and end with contracts. Contracts help document the code, yet can never suffer from documentation drift as the slightest misalignment with the code will instantly flag an error.

Contracts are truly about the way we design the code. Assertions check for errors in implementation.

Extreme Programming, Test-Driven Development, and other agile methods stress the importance of writing test code early. DBC complements that idea, adding built-in tests to ensure we don't violate design assumptions.

Write a function's comment header block first. Then write the contracts. Fill in the rest of the comments, and only then produce the code.

Thanks to Jim Gimpel and Rod Chapman for their thoughts and comments on this article.

Jack Ganssle (jack@ganssle.com) is a lecturer and consultant specializing in embedded systems' development issues. 

Endnotes:
1. Meyer, Bertrand. "Advanced Topics in Object Technology," Lecture 3, 29 April 2002: Design by Contract, ETH, Summer 2002. (original link is out of date: http://se.inf.ethz.ch/people/arnout/lectures/arnout_dbc_2002_slides.pdf. Try: http://se.ethz.ch/~meyer/courses/object/.
Back

2. DBC using Nana: http://savannah.gnu.org/projects/nana
Back

3. Aechmea's C2 product: www.automatedtestinginstitute.com
Back

4. SPARK home page: http://www.altran.co.uk/uksolutions/ecs/technology/spark.html Back

5. Saks, Dan. "Catching errors early with compile-time assertions," Embedded Systems Programming, July 2005, p.7.
Back

Reader Response


SPARK sounds a lot like the static code analysis that Polyspace offers in their products (www.polyspace.com), though the Polyspace product is not limited to contract checking.

The department I'm working in at Sandia has been using Design By Contract for at least 4+ years now (it was in place before I started working here). As you have mentioned, there is a clean alternative implementation using macros (which means DBC can work for all C/C++ compilers, requires no extra pre-compilation steps, and results in no messy code). We have a default DBC failure-condition function that prints out the file, line number, and actual assertion (using the macro preprocessor's standard "convert to string" # operator). On a project I recently worked on, once all resources were initialized by the code, I registered a DBC failure callback that did the following upon contractual failure:

If in testing mode, the DBC failure function logged/printed out an error message to the developer, and flashed an LED in a loop. When connected to the processor via JTAG, the developer could halt the processor and step back through the stack to determine what might have caused the failure.

In deployment mode, the DBC failure function does the following:

1) A watchdog timer (reserved for use by DBC only) is queried to see if it has been enabled prior to entry of this DBC failure function
a) if the WD timer is enabled, the WD timer is set such that the processor is immediately reset;
b) if the WD timer is not enabled, the WD timer is enabled and set for a reasonable amount of time to allow the next step to be carried out.

2) An attempt to report the DBC error to another processor via more DB-contracted code is made. If another DBC failure fires while trying to report the error, step 2 will reset the processor to avoid an endless loop of DBC failures.

3) After returning from the report function, the watchdog timer is set to reboot the processor immediately.

This DBC failure function worked very well in practice.

I should also mention that we devised a method of shutting off DBC through conditional compilation of the macro (the macro would simply be defined to do nothing if a certain constant was defined). Originally using this option meant one or more of the macros were always defined as on or off for the whole application, but eventually I figured out a way to define the macros on/off at a per C-file basis. While the practice of turning off DBC is useful for reclaiming a slight bit of performance & code/data space once the code is flawless, we have never turned off DBC in deployed applications. Turning off DBC could allow a developer on a team to come in and inadvertantly add a bug to the code that DBC would have caught if turned on. We also find that regardless of how stable our code is, we're never confident we've got all the bugs out and achieved "flawless code". Using DBC is cheap insurance.

Last of all, I used Doxygen to produce code-level documentation. In doing so, I found a way to re-define the DBC require(), invariant(), and ensure() macros inside of Doxygen, assigning pre/post/inv tags with the contract assertion strings supplied to the macros in the code. This ended up producing wonderful documentation of the code while at the same time kept the code very clean.

I highly recommend DBC to fellow programmers. If you'd like to see/post the details behind our DBC implementation & Doxygen use, let me know. I can't promise anything up front except for the Doxygen macro re-definitions, but if asked, I'll see what I can do to provide code. Sometimes getting public-domain-like IP for release outside of Sandia can be a battle.

Regards,
-Jason Jarosz
Firmware Engineer
Sandia National Laboratories
Albuquerque, NM


Loading comments...

Parts Search Datasheets.com

KNOWLEDGE CENTER