Boost C++ Libraries Home Libraries People FAQ More

Next

Chapter 1. Boost.Contract 1.0.0

Lorenzo Caminiti

Distributed under the Boost Software License, Version 1.0 (see accompanying file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt)

Table of Contents

Introduction
Full Table of Contents
Getting Started
Contract Programming Overview
Tutorial
Advanced
Extras
Examples
Reference
Release Notes
Bibliography
Acknowledgments

Our field needs more formality, but the profession has not realized it yet.

-- Bertrand Meyer (see [Meyer97] page 400)

This library implements contract programming (a.k.a., Design by Contract or DbC) [1] for the C++ programming language. All contract programming features are supported by this library: Subcontracting, class invariants (also for static and volatile member functions), postconditions (with old and return values), preconditions, customizable actions on assertion failure (e.g., terminate the program or throw exceptions), optional compilation of assertions, disable assertions while already checking other assertions (to avoid infinite recursion), and more (see Feature Summary).

Contract programming allows to specify preconditions, postconditions, and class invariants that are automatically checked when functions are executed at run-time. These conditions assert program specifications within the source code itself allowing to find bugs more quickly during testing, making the code self-documenting, and increasing overall software quality (see Contract Programming Overview).

For example, consider the following function inc that increments its argument x by 1 and let's write its contract using code comments (see introduction_comments.cpp):

void inc(int& x)
    // Precondition:    x < std::numeric_limit<int>::max()
    // Postcondition:   x == oldof(x) + 1
{
    ++x; // Function body.
}

The precondition states that at function entry the argument x must be strictly smaller than the maximum allowable value of its type (so it can be incremented by 1 without overflowing). The postcondition states that at function exit the argument x must be incremented by 1 with respect to the old value that x had before executing the function (indicated here by oldof(x)). Note that postconditions shall be checked only when the execution of the function body does not throw an exception.

Now let's program this function and its contract using this library (see introduction.cpp and Non-Member Functions):

#include <boost/contract.hpp>

void inc(int& x) {
    boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); // Old value.
    boost::contract::check c = boost::contract::function()
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); // Line 17.
        })
        .postcondition([&] {
            BOOST_CONTRACT_ASSERT(x == *old_x + 1); // Line 20.
        })
    ;

    ++x; // Function body.
}

When the above function inc is called, this library will:

  • First, execute the functor passed to .precondition(...) that asserts inc precondition.
  • Then, execute inc body (i.e., all the code that follows the boost::contract::check c = ... declaration).
  • Last, execute the functor passed to .postcondition(...) that asserts inc postcondition (unless inc body threw an exception).

For example, if there is a bug in the code calling inc so that the function is called with x equal to std::numeric_limits<int>::max() then the program will terminate with an error message similar to the following (and it will be evident that the bug is in the calling code):

precondition assertion "x < std::numeric_limits<int>::max()" failed: file "introduction.cpp", line 17

Instead, if there is a bug in the implementation of inc so that x is not incremented by 1 after the execution of the function body then the program will terminate with an error message similar to the following (and it will be evident that the bug is in inc body): [2]

postcondition assertion "x == *old_x + 1" failed: file "introduction.cpp", line 20

By default, when an assertion fails this library prints an error message such the ones above to the standard error std::cerr and terminates the program calling std::terminate (this behaviour can be customized to take any user-specified action including throwing exceptions, see Throw on Failures). Note that the error messages printed by this library contain all the information necessary to easily and uniquely identify the point in the code at which contract assertions fail. [3]

[Note] Note

C++11 lambda functions are necessary to use this library without manually writing a significant amount of boiler-plate code to program functors that assert the contracts (see No Lambda Functions). That said, this library implementation does not use C++11 features and should work on most modern C++ compilers (see Getting Started).

In addition to contracts for non-member functions as shown the in the example above, this library allows to program contracts for constructors, destructors, and member functions. These can check class invariants and can also subcontract inheriting and extending contracts from base classes (see introduction_public.cpp and Public Function Overrides): [4]

template<typename T>
class vector
    #define BASES public pushable<T>
    : BASES
{
public:
    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // For subcontracting.
    #undef BASES

    void invariant() const { // Checked in AND with base class invariants.
        BOOST_CONTRACT_ASSERT(size() <= capacity());
    }

    virtual void push_back(T const& value,
            boost::contract::virtual_* v = 0) /* override */ { // For virtuals.
        boost::contract::old_ptr<unsigned> old_size =
                BOOST_CONTRACT_OLDOF(v, size()); // Old values for virtuals.
        boost::contract::check c = boost::contract::public_function< // For overrides.
                override_push_back>(v, &vector::push_back, this, value)
            .precondition([&] { // Checked in OR with base preconditions.
                BOOST_CONTRACT_ASSERT(size() < max_size());
            })
            .postcondition([&] { // Checked in AND with base postconditions.
                BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
            })
        ;

        vect_.push_back(value);
    }
    BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back` above.

    // Could program contracts for those as well.
    unsigned size() const { return vect_.size(); }
    unsigned max_size() const { return vect_.max_size(); }
    unsigned capacity() const { return vect_.capacity(); }

private:
    std::vector<T> vect_;
};

Language Support

The authors of this library advocate for contracts to be added to the core language. Adding contract programming to the C++ standard has a number of advantages over any library implementation (shorter and more concise syntax to program contracts, specify contracts in declarations instead of definitions, enforce contract constant-correctness, expected faster compile- and run-time, vendors could develop static analysis tools to recognize and check contracts statically when possible, compiler optimizations could be improved based on contract conditions, etc.).

The [P0380] proposal supports basic contract programming, it was accepted and it will be included in C++20. This is undoubtedly a step in the right direction, but unfortunately [P0380] only supports pre- and postconditions while missing important features such as class invariants and old values in postconditions, not to mention the lack of more advanced features like subcontracting (more complete proposals like [N1962] were rejected by the C++ standard committee). All contracting programming features are instead supported by this library (see Feature Summary for a detailed comparison between the features supported by this library and the ones listed in different contract programming proposals, see Bibliography for a list of references considered during the design and implementation of this library, including the vast majority of contract programming proposals submitted to the C++ standard committee).



[1] Design by Contract (DbC) is a registered trademark of the Eiffel Software company and it was first introduced by the Eiffel programming language (see [Meyer97]).

[2] In this example the function body is composed of a single trivial instruction ++x so it easy to check by visual inspection that it does not contain any bug and it will always increment x by 1 thus the function postcondition will never fail. In real production code, function bodies are rarely this simple and can hide bugs which make checking postconditions useful.

[3] Rationale: The assertion failure message printed by this library follows a format similar to the message printed by Clang when the C-style assert macro fails.

[4] The pushable base class is used in this example just to show subcontracting, it is somewhat arbitrary and it will likely not appear in real production code.

Last revised: April 22, 2020 at 13:40:40 GMT


Next