Friday, September 13, 2013

Design by contract

Design by contract is a software design approach (the term is actually a trademark), first introduced by Bertrand Meyer in his programming language Eiffel (a free GNU implementation of the language is called SmartEiffel). The concept is built around the idea of a contract between software components, which must fulfilled. Each module defines a set of valid input conditions and guarantees a certain output when the conditions are met. Simply put, design by contract requires you to define a set of preconditions (input constraints) and postconditions (output constraints) for each function or method. Eiffel also supports invariants, which are constraints put on the object fields.

If you think about it for a while, it turns out that you don't need a dedicated programming language to implement most of the design by contract principles in your software. In fact, many programmers use at least some kind of preconditions in their code to ensure input data correctness, but without specifing it formally. Consider this simple C++ method to calculate the greatest common divisor of two integers:
int gcd(int a, int b)
{
    if (b == 0) {
        return a;
    } else {
        return gcd(b, a % b);
    }
}
According to its definition "the greatest common divisor (gcd) of two or more integers (at least one of which is not zero), is the largest positive integer that divides the numbers without a remainder". To be sure that the method parameters meet the criteria stated in the definition, you will need to validate both variabes:
int gcd(int a, int b)
{
    // at least one of the integers is not zero
    if (a != 0 || b != 0) {
        if (b == 0) {
            return a;
        } else {
            return gcd(b, a % b);
        }
    }
    // report error
}
As you can see, the code gets unnecessarily complicated, because it mixes computations with validation logic. And it's still only a half of the contract. To ensure that the return value is also correct, you need to implement additional conditions:
int gcd(int a, int b)
{
    int result;

    // at least one of the integers is not zero
    if (a != 0 || b != 0) {
        if (b == 0) {
            result = a;
        } else {
            result = gcd(b, a % b);
        }
        // resulting number divides the input numbers without a remainder
        if ((a % result == 0) && (b % result == 0)) {
            return result;
        }
    }
    // report error
}
These conditions complicate the code even more. To solve this problem, design by contract approach introduces two dedicated clauses: requires for preconditions and ensures for postconditions. There are libraries and compilers for many various programming languages which support these directives. For example, if you write code in Java, you can use cofoja, which supports contracts through annotations. In C and C++ you can use standard assert macro to achieve the similar effect:
#define REQUIRES(condition) assert(condition)
#define ENSURES(condition) assert(condition)

int gcd(int a, int b)
{
    // at least one of the integers is not zero
    REQUIRES(a != 0 || b != 0)

    int result;

    if (b == 0) {
        result = a;
    } else {
        result = gcd(b, a % b);
    }

    // resulting number divides the input numbers without a remainder
    ENSURES((a % result == 0) && (b % result == 0))

    return result;
}
Now the code looks much cleaner and it is easy to distinguish the computation logic from the preconditions and postcoditions. Also, you can now quickly spot the method's input requirements and the conditions met by the result.

Of course you can replace assert with your own macros, in order to not stop the program execution when the contract rules are broken (which assert does by default). If you are interested, I prepared a set of macros which throw a dedicated exception instead. You can find them, together with usage examples, at the project page on Github.

Design by contract is a very useful technique if you want to ensure a high level of software correctness, and it should be considered as complementary, not competitive, to unit testing. Unit tests are usually run only once before software deployment and may not be able to find all errors, because in most cases it is impossible to test code against all possible inputs. The contract rules, however, are verified every time code is executed. On the other hand, using preconditions and postconditions may in some cases considerably slow the program down. Although this should rarely be the problem, since CPU usage very seldom is a bottleneck, many systems allow you to turn off constraint checking in release mode, in order to improve performance.

No comments: