Boost C++ 库

...世界上最受推崇和设计最精良的 C++ 库项目之一。 Herb SutterAndrei Alexandrescu,《C++ 编程规范

Next

第 1 章。Boost.Contract 1.0.0

Lorenzo Caminiti

根据 Boost 软件许可协议 1.0 版发布(请参阅随附文件 LICENSE_1_0.txt 或 https://boost.ac.cn/LICENSE_1_0.txt 的副本)

目录

简介
完整目录
入门指南
契约式编程概述
教程
高级
扩展
示例
参考
发布说明
参考文献
致谢

我们的领域需要更多的形式化,但专业领域尚未意识到这一点。

-- Bertrand Meyer(参见 [Meyer97] 第 400 页)

此库为 C++ 编程语言实现了 契约式编程(也称为 Design by Contract 或 DbC)[1]。此库支持所有契约式编程功能:子契约、类不变式(也适用于静态和 volatile 成员函数)、后置条件(带有旧值和返回值)、前置条件、断言失败时的可自定义操作(例如,终止程序或抛出异常)、断言的可选编译、在已检查其他断言时禁用断言(以避免无限递归)以及更多功能(请参阅功能概要)。

契约式编程允许指定前置条件、后置条件和类不变式,这些条件在函数运行时自动检查。这些条件在源代码本身中声明程序规范,从而可以在测试期间更快地发现错误,使代码具有自文档性,并提高整体软件质量(请参阅 契约式编程概述)。

例如,考虑以下函数 inc,它将其参数 x 递增 1,让我们使用代码注释编写其契约(请参阅 introduction_comments.cpp

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

前置条件声明在函数入口处,参数 x 必须严格小于其类型的最大允许值(以便它可以递增 1 而不会溢出)。后置条件声明在函数退出时,参数 x 必须相对于函数执行之前的 旧值 递增 1(此处用 oldof(x) 表示)。请注意,只有当函数体执行未抛出异常时才应检查后置条件。

现在,让我们使用此库编写此函数及其契约(请参阅 introduction.cpp非成员函数

#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.
}

当调用上述函数 inc 时,此库将

  • 首先,执行传递给 .precondition(...) 的 functor,该 functor 断言 inc 前置条件。
  • 然后,执行 inc 主体(即,boost::contract::check c = ... 声明之后的所有代码)。
  • 最后,执行传递给 .postcondition(...) 的 functor,该 functor 断言 inc 后置条件(除非 inc 主体抛出异常)。

例如,如果调用 inc 的代码中存在错误,导致使用等于 std::numeric_limits<int>::max()x 调用该函数,则程序将终止并显示类似于以下的错误消息(并且很明显错误在调用代码中)

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

相反,如果 inc 的实现中存在错误,导致在函数体执行后 x 未递增 1,则程序将终止并显示类似于以下的错误消息(并且很明显错误在 inc 主体中):[2]

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

默认情况下,当断言失败时,此库会将如上所示的错误消息打印到标准错误 std::cerr 并终止程序,调用 std::terminate(此行为可以自定义为执行任何用户指定的操作,包括抛出异常,请参阅 失败时抛出异常)。请注意,此库打印的错误消息包含轻松且唯一地识别代码中契约断言失败点所需的所有信息。[3]

[Note] 注意

C++11 lambda 函数是使用此库所必需的,无需手动编写大量样板代码来编程 functor 以断言契约(请参阅 无 Lambda 函数(无 C++11))。也就是说,此库实现不使用 C++11 功能,并且应该在大多数现代 C++ 编译器上工作(请参阅 入门指南)。

除了如上例所示的非成员函数的契约外,此库还允许为构造函数、析构函数和成员函数编程契约。这些可以检查类不变式,并且还可以从基类 子契约 继承和扩展契约(请参阅 introduction_public.cpp公共函数重写(子契约)):[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_;
};

语言支持

此库的作者提倡将契约添加到核心语言中。将契约式编程添加到 C++ 标准比任何库实现都具有许多优势(更短更简洁的语法来编程契约,在声明而不是定义中指定契约,强制执行契约常量正确性,预期的更快编译和运行时,供应商可以开发静态分析工具以在可能的情况下静态识别和检查契约,编译器优化可以基于契约条件进行改进等)。

[P0380] 提案支持基本的契约式编程,它已被接受,并将包含在 C++20 中。这无疑是朝着正确方向迈出的一步,但不幸的是,[P0380] 仅支持前置条件和后置条件,而缺少重要的功能,例如类不变式和后置条件中的旧值,更不用说缺少更高级的功能,如子契约(更完整的提案,如 [N1962] 被 C++ 标准委员会拒绝)。此库反而支持所有契约式编程功能(有关此库支持的功能与不同契约式编程提案中列出的功能之间的详细比较,请参阅 功能概要,有关设计和实现此库期间考虑的参考文献列表,包括提交给 C++ 标准委员会的大多数契约式编程提案,请参阅 参考文献)。



[1] 契约式设计 (DbC) 是 Eiffel Software 公司的注册商标,它最初由 Eiffel 编程语言引入(请参阅 [Meyer97])。

[2] 在此示例中,函数体由单个简单的指令 ++x 组成,因此通过目视检查很容易检查它是否不包含任何错误,并且它将始终将 x 递增 1,因此函数后置条件永远不会失败。在实际生产代码中,函数体很少如此简单,并且可能隐藏使检查后置条件有用的错误。

[3] 理由: 此库打印的断言失败消息遵循类似于 Clang 在 C 风格 assert 宏失败时打印的消息的格式。

[4] 此示例中使用 pushable 基类只是为了展示子契约,它有些随意,可能不会出现在实际生产代码中。


Next