Home | Libraries | People | FAQ | More |
Copyright © 2008-2019 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
“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:
.precondition(...)
that asserts inc
precondition.
inc
body
(i.e., all the code that follows the boost::contract::check c = ...
declaration).
.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 | |
---|---|
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_; };
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 |