Putting out contracts on bugs - Embedded.com

Putting out contracts on bugs

Start debugging before a bug slaps you in the forehead like a cold fish jumping out of water.

Last month I introduced Design by Contract (a trademark of Eiffel software and abbreviated DBC). DBC is an approach to programming that recognizes that there are responsibilities between functions and their callers. Developers explicitly describe these responsibilities, or contracts, in the code, using three tags. Preconditions are things that must be true about the system's state when the function starts—for instance, the legal range of a variable passed to the routine. Postconditions express the nature of the system when the routine exits. Invariants stay true throughout the execution of the function.

People familiar with DBC will be aghast that I'm torturing the concept into a procedural, rather than object-oriented, description. Yet today most embedded systems developers use C. It would be tragic to leave 70% of us unable to use these ideas.

Although DBC is hardly new, it as yet has almost no penetration into the embedded space, due to a lack of knowledge about the concept and the fact that mainstream languages provide no intrinsic support.

Regular readers know I'm a zealot about seeding software with debugging traps. The time to start debugging is when you're writing the code, not when a bug rears up and slaps you in the forehead like a cold fish jumping out of the water. Since code typically has a 5% to 10% error rate after passing the compiler's syntax check, it's clear that a lot of what we produce will be wrong. DBC is perhaps the most powerful technique we have to toss a penalty flag when someone tries to use a function incorrectly.

In my last column, I evangelized DBC, only to finally disappoint you, gentle reader, when I admitted that it's not a part of C or C++.1 But there are some options. None are perfect, none achieve the clean and seamless DBC possibilities embodied in the Eiffel language. But a 90% solution counts as an A grade in most things. A first approximation to perfection is often good enough. For more background on DBC and writing good contracts, see last month's column and the two books I recommend in the endnotes.1, 2, 3

Charlie Mills wrote a free preprocessor for C programs that extracts contracts embedded in comments, turning them into normal C code. His 2004 article about the package generated some interest that quickly died out.4 I've found only a single user—though he's enthusiastic about both the preprocessor and DBC in general.

Let's look at some examples using the syntax that Charlie adopted. Since C doesn't accept any sort of DBC keywords, his preprocessor extracts mnemonics embedded in comments as follows:

/**  pre:  (precondition)  post: (postcondition)  inv:  (invariant)*/  

That is, a set of contracts exists in its own comment block which starts with double asterisks. Last month I showed a function that computes the positive root of a quadratic equation. Listing 1 shows the same function instrumented with three contracts.

View the full-size image

The triptych of contracts traps the three ways that this, essentially one line of code, can fail. Isn't that astonishing? A single line possibly teeming with mistakes. Yet the code is correct. Problems stem from using it incorrectly, the very issue DBC prevents. So rather than “failure,” think of the contracts as provisions that define and enforce the relationship between the function and the caller. In this case, the caller may not supply zero for a, to avoid a divide by zero. If (b*b-4*a*c) is negative, sqrt() will fail. And a very small a could overflow the capacity of a floating point number.

Run Listing 1 through Charlie's preprocessor and the result, edited for clarity, is shown in Listing 2.

View the full-size image

Break a contract, and dbc_error() —which you supply—runs. printf if you can, log the error, and halt if you must. But any attempt to use solve_pos() illegally will immediately flag a problem, long before an incorrect error would propagate through hundreds of other calls.

Computing the discriminant twice sounds computationally expensive! The gcc compiler, though, using the “Os (optimize for size) switch on an x86, does the math once and stores the result for use later. gcc also optimizes out the unneeded gotos . Other compilers and processor architectures may give different results. Contracts don't necessarily add much of a memory or performance penalty.

In DBC, contracts never cause side effects. Thus the preprocessor does not support the “= ” operator.

The preprocessor has numerous options beyond what I've mentioned. See Charlie's article for the full syntax.4 I think some of the more complex features (which create loops) are not needed and are too computationally expensive.

Downsides? the preprocessor's output is ugly. The indentation strategy (edited out in Listing 2) just couldn't be worse. I've found one bug: some constants with decimal points stop the preprocessor. The strings (for example, “quad.c:5 postcondition failed “) are long and burn valuable memory. And wouldn't it be nice for the program to optimize out unnecessary jumps? None of these are showstoppers, though.

I did try to make some improvements, but gave up, totally baffled by the language used (Ruby) and the code's structure. No one provides support, and Charlie doesn't return my e-mails. Perhaps one of you can become the Yoda of DBC and fold some improvements into this very useful utility.

Building & using DBC for C
I installed Charlie's package on both Linux and Windows machines. The Linux build is pretty simple, but under Windows figure on a lot of annoying hunting around for files and copying them to the proper directories. I can't give better advice as it's quite directory-specific. Arm yourself with an adult drink to soothe frayed nerves.

DBC for C is written in Ruby, which few of us firmware folk use. Charlie used a parser-generator to simplify the work. Unfortunately, these choices yield a completely opaque structure that's impossible to tune if you're not versed in Ruby and parser languages.

First get Ruby from www.ruby-lang.org and install it using the supplied instructions. For Windows use the “one-click install” package. The Linux package has a very easy-to-use script that builds Ruby from the sources.

You'll also need Ruby's header files.The apt-get command, supported in Ubuntu and Debian, will get the header files. Issue apt-get install ruby1.8-dev . Those were included in the Windows one-click package. With a fresh installation of Linux I needed C header files, obtained via apt-get install libc-dev .

Next get racc, Ruby's version of yacc, from http://i.loveruby.net/en/prog/racc.html. I found it convenient to extract it to a bin directory in my home path. Follow the build instructions; then test racc per the README. In Linux you may need root privileges, though sudo access suffices.

Under Windows I had no end of trouble getting the right files in the right places, but whenever the build failed I just found the missing file and copied it as needed. Eventually I found www.dets-home.de/it-writings/Install_rd2_winnt.html, which describes the installation process for a Windows version. If troubled by a finicky installation see the references at the end of this article for more information.5, 6, 7

Get and extract DBC for C from http://rubyforge.org/frs/?group_id=354. The build instructions are simple and clear, though sudo access may be required under Linux. In Windows I had to fiddle with the file pre-config.rb because of the Unix file conventions. Comment out lines 25 to 33 and 51 to 59, which move files between directories. Copy them yourself using Windows Explorer.

Once installed, dbcparse.rb converts a C source file full of DBC constructs to a source file with the DBC constructs converted to C code. Ruby dbcparse.rb –help will display the options, though I've been unable to ascertain the meaning of some. To use the program issue:

ruby dbcparse.db "no-line 	infile.c > outfile.c   

Feed outfile.c into your C compiler. If, for some reason, you must compile without contracts, skip dbcparse and compile infile.c . With the contracts embedded in comments, no source changes are needed to enable or disable contract generation. Yet the contracts remain a permanent form of documentation.

Add the -d option to generate doxygen tags in the output file.

Other approaches
Charlie's is just one approach to doing DBC in C. We'll look at others next month and also consider appropriate responses to a broken contract.Thanks to Bill Gatliff for help with some Linux issues and Marc Verweft for insight into his experiences using DBC for C.

Jack Ganssle () is a lecturer and consultant specializing in embedded systems' development issues. For more information about Jack .

1. Ganssle, Jack.
“Contracts put the 'I do' in code, Embedded Systems Design March 2007, p.59.

2. Mitchell, Richard and Jim McKim. Design By Contract, By Example . Boston, MA: Addison Wesley, 2002 . A frustrating and badly organized book that offers good advice on designing good contracts.

3. Samek, Miro. Practical Statecharts in C/C++ . Lawrence, KS: CMP Books, 2002. Though not about DBC, Miro does have some useful discussion of the subject.

4. Mills, Charlie. “Using Design by Contract in C,” OnLamp.com, O'Reilly, 10/28/2004. Available at: www.onlamp.com/pub/a/onlamp/2004/10/28/design_by_contract_in_c.html

5. Detering, Dirk.”HOWTO install RDtool on Windows NT,” Version: 0.2 Copyright 2003. Available at: www.dets-home.de/it-writings/Install_rd2_winnt.html

6. “Why are parser tools rarely used in ruby?” E-mail discussion from comp.lang.ruby on Google Groups, September 2002. Available at: http://groups.google.com/group/comp.lang.ruby/

7. “Ruby.doc?” E-mail discussion from comp.lang.ruby on Google Groups, January 2002. Available at: http://groups.google.com/group/comp.lang.ruby/

We've been using REQUIRE and ENSURE macros in C for years for this purpose. They nominally expand to ASSERT, which we either define as a special-purpose log/recover routine or in some cases just use the standard assert (and thence to abort).

For invariants, we provide a boolean function invariants() and then REQUIRE and ENSURE(invariants). (Initialization functions don't require it but do ensure it).

It will be interesting to read the other DBC methods for C in your upcoming articles.

– Paul Hepworth

Two obeservaions.

1. The generated test “if (!(a > 0) …” doesn't semantically match the precondition “a != 0”. In fact, you could always require that “a” be normalized to a positive value, but then the precondition should be changed.

2. The function isn't clearly defined. It claims to return “the positive root”. What does it do for quadratics with two positive roots, such as “x**2 -3*x + 2”? It chooses an arbitrary member of the solution set. This behavior isn't easily expressed in a postcondition.

Granted, this is just an example. But it illustrates that the hard work is in describing the conditions and invariants, not necessarily in automating the checks.

– Gary Bjerke

One last “obeservaion” … er, observation.

You should probably define the function as returning the maximum real root of a quadratic, it it exists. This includes the case where both roots are negative.

– Gary Bjerke

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.