65.9K
CodeProject 正在变化。 阅读更多。
Home

C++ 中的契约式设计

Jarl Lindrud
starIconstarIconstarIconstarIcon
emptyStarIcon
starIcon

4.45/5 (12投票s)

2004年9月15日

5分钟阅读

viewsIcon

122416

downloadIcon

644

一篇关于如何使用 Lambda 表达式在 C++ 中实现契约式设计的文章。

引言

我偶尔会看到有人尝试将契约式设计（DbC）的概念引入 C++，通常使用某种断言。这样做总有一些局限性，但我认为应该可以做得比我至今所见的更好。

DbC 通常用于描述三种断言

  • 前置条件——在调用函数时必须满足的条件。
  • 后置条件——在函数退出时必须满足的条件。
  • 类不变量——对象类的所有属性在公共成员函数执行期间之外必须始终满足的条件。

DbC 在《面向对象软件构造》[1] 一书中被引入编程界，并且是 Eiffel 编程语言的一个集成部分。然而，很少有（或者没有？）主流语言能开箱即用支持它，C++、C# 和 Java 都不能。在这三者中，C++ 由于其基于作用域的对象销毁和模板的特性，最适合实现 DbC，而 C# 和 Java 都缺乏这些特性。

问题所在

基本上，对于一个给定的函数，我们希望指定一个前置条件，它需要在函数入口处成立，以及一个后置条件，它需要在函数出口处成立，无论是显式返回还是由于未捕获的异常导致栈展开。此外，我们希望能够指定一个类不变量条件，该条件在任何公共成员函数的入口和出口处都会被检查。

能做的事情是有限的。特别是，不可能阻止用户用不满足基函数声明的前置条件或后置条件的实现来覆盖虚函数。而且不变量条件不能自动检查；程序员必须提供某种触发器。尽管如此，C++ 提供了许多设施供我们使用，我们可以利用它们走得相当远。

主要问题是在函数开始时指定一个后置条件，同时将实际检查推迟到函数退出时。局部栈分配对象的析构函数是解决这个问题的关键，再结合 Lambda 表达式。我们还将借鉴 [2] 中的一些想法，为失败的条件提供有用的调试信息。利用预处理器，我们可以在所有底层机制之上添加一个漂亮的封装。下面的例子展示了我们最终得到的效果。

示例

// The Rectangle class represents a rectangular
// viewing area that can be zoomed or translated.
// The rectangle is specified by two corners,
// of which the first must have smaller
// coordinates than the second.

#include "PrePostCondition.h"

namespace Demo {

    class Rectangle
    {
    public:
        Rectangle(double x1, double y1, double x2, double y2) :
            x1(x1), 
            y1(y1), 
            x2(x2), 
            y2(y2)
        {
            PRECONDITION(1);
            POSTCONDITION(1);
        }

        double width()
        {
            return x2-x1;
        }

        double height()
        {
            return y2-y1;
        }

        void zoom(double factor)
        {
            PRECONDITION( factor > 0 )(factor);
            POSTCONDITION( POST(width) == 
                width()*factor )(width())(factor)(POST(width));
            POSTCONDITION( POST(height) == 
                height()*factor )(height())(factor)(POST(height));

            // Implementation
            // ...
        }

        void translate(double dx, double dy)
        {
            PRECONDITION(1);
            POSTCONDITION( POST(x1) == x1+dx )(x1)(POST(x1))(dx);
            POSTCONDITION( POST(y1) == y1+dy )(y1)(POST(y1))(dy);
            POSTCONDITION( POST(x2) == x2+dx )(x2)(POST(x2))(dx);
            POSTCONDITION( POST(y2) == y2+dy )(y2)(POST(y2))(dy);

            // Implementation
            // ...

        }

    private:
        double x1;
        double y1;
        double x2;
        double y2;

        BEGIN_INVARIANT(Rectangle)
            DEFINE_INVARIANT( x2 > x1 && y2 > y1 )(x1)(x2)(y1)(y2)
        END_INVARIANT()
    };

} // namespace Demo

int main()
{
    Demo::Rectangle badRectangle(0,0,-1,-1);
    Demo::Rectangle rectangle(0,0,1,1);
    rectangle.zoom(-1);
    rectangle.translate(1,1);
    rectangle.zoom(2);
    rectangle.translate(-5,-5);
    rectangle.zoom(.5);
    return 0;
}

POST() 宏指示其参数不应在条件本身被求值之前被求值；如果没有 POST()，参数将被立即求值。参数可以是变量、自由函数或成员函数。

PRECONDITION 和 POSTCONDITION 宏都会检查类不变量，前者在入口处检查，后者在出口处检查。当前置条件、后置条件或不变量失败时，相关信息将被打印到调试输出。要查看这一点，请编译并运行示例代码。由于我们未能为 zoom 和 translate 函数提供实现，而且我们还冒昧地创建了一个具有糟糕角的 Rectangle，我们将遇到大量的前置条件、后置条件和不变量失败。我想在这里放一张 Visual Studio 输出窗口的截图，显示所有失败，但本文仅限于 600 像素宽的图像，您将看不到什么。无论如何，输出窗口中一行文本的完整内容是

e:\development\codeproject\designbycontract\demo.cpp(34): FAILURE: 
Postcondition: POST(height) == height()*factor in Demo::Rectangle::zoom: 
Thread-id=2572 : Timestamp(ms)= 35866: height()=1, factor= -1, POST(height)=1,

这是另一行

e:\development\codeproject\designbycontract\demo.cpp(16): FAILURE: Class 
invariant (on exit): x2 > x1 && y2 > y1 in 
Demo::Rectangle::Rectangle: Thread-id=2572 : 
      Timestamp(ms)=37800: x1=0, x2=-1, y1=0, y2=-1,

双击这些行会直接将您带到失败条件的代码行。注意，可以轻松地写出额外的变量和值来帮助诊断情况。

在条件失败后要采取的操作很容易定制。默认操作是不做任何事情，即继续正常执行。一个更明显的做法是，在调试版本中触发断言，在发布版本中抛出异常。要启用此失败操作，请重新定义 PRECONDITION 和 POSTCONDITION 宏

#include "PrePostCondition.h" 

#undef PRECONDITION
#undef POSTCONDITION

#ifdef NDEBUG 
#define PRECONDITION(condition) 
        UTIL_PRECONDITION( util::PrePostCondition::Print_ODS, 
        util::PrePostCondition::Fail_Throw, condition ) 
#define POSTCONDITION(condition) 
        UTIL_POSTCONDITION( util::PrePostCondition::Print_ODS, 
        util::PrePostCondition::Fail_Throw, condition ) 
#else 
#define PRECONDITION(condition) 
        UTIL_PRECONDITION( util::PrePostCondition::Print_ODS, 
        util::PrePostCondition::Fail_Assert, condition ) 
#define POSTCONDITION(condition) 
        UTIL_POSTCONDITION( util::PrePostCondition::Print_ODS, 
        util::PrePostCondition::Fail_Assert, condition ) 
#endif

如果在未捕获异常的栈展开过程中检测到条件失败，则不执行任何操作；在这种情况下抛出另一个异常将无情地终止整个程序。

实现细节

我们使用局部变量的析构函数来延迟检查后置条件和不变量。为了存储构成条件的表达式，我们利用了 Boost Lambda 库 [3]，它允许我们构建可以在稍后某个时间点存储和求值的复杂表达式。为了允许用户在条件失败时输出额外信息，我们应用了 [2] 中的一些预处理器技巧，实际上创建了一个可变参数宏。

由于大量使用 Lambda 表达式，使用这些宏会显著增加编译时间。我还没有尝试优化框架以提高编译时间；目前存在大量的 functor 和编译时 Lambda 表达式，消除其中一些肯定有助于缩短编译时间。使用预编译头文件并在那里实例化通用模板也有帮助。

运行时开销也很显著，尤其是在调试版本中，因为不执行内联。不过，这通常不是大问题。在测试程序时，我们可以容忍性能损失以帮助定位 DbC 违规，一旦程序被确定为正确运行，就可以禁用检查。

包含的示例程序已在 Visual C++ 7.1 中编译和测试。由于编译器特有的行为（也称为 bug），它几乎肯定无法在早期版本的 Visual C++ 中工作。需要 Boost Function 和 Lambda 库，可以作为 Boost 库 [4] 的一部分下载。我已经针对 Boost 的 1.30 和 1.31 版本进行了测试。

摘要

我提出了一个 C++ 框架来实现 DbC，该框架允许预先声明类不变量、前置条件和后置条件，并在正确的时间强制执行它们，并在遇到失败时提供详尽的诊断信息。

非常欢迎评论。如果您发现任何 bug，请告诉我！

参考文献

[1] - Bertrand Meyer: Object-Oriented Software Construction, Second Edition, Prentice Hall, 1997.

[2] - Andrei Alexandrescu, John Torjo: Enhancing Assertions, C++ Users Journal, August 2003.

[3] - Jaakko Järvi, Gary Powell: Boost Lambda Library.

[4] - www.boost.org

© . All rights reserved.