Boost C++ Libraries

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:

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]

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).