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

C++ 的契约式设计框架

starIconstarIconstarIconstarIcon
emptyStarIcon
starIcon

4.83/5 (5投票s)

2002年3月2日

5分钟阅读

viewsIcon

73312

downloadIcon

1179

C++ 中契约式设计的实现。

引言

这些类和支持宏为 C++ 项目提供了合约设计框架。它已在 Visual C++ 6 和 7 中进行了测试,但应能在任何符合标准的 C++ 编译器下进行少量修改后工作。例如,它使用了 Visual C++ 中定义的 _ASSERTE 宏,该宏在 <crtdbg.h> 中定义。其他编译器可能会在别处定义它。

合约设计(Design by Contract)是由 Bertrand Meyer 在 Eiffel 编程语言中推广的一种方法,其中支持直接内嵌于语言结构中。

请参阅 Bertrand Meyer 所著的《面向对象软件构造》(Object-Oriented Software Construction - 2nd Edition,Prentice Hall,1997)第 11 章,以及 http://www.eiffel.com/doc/manuals/technology/contract/

基本思想是,一个类可以被视为与其客户端之间存在一份合约,其中该类保证提供某些结果(其方法的后置条件),前提是客户端同意满足某些要求(类方法的先置条件)。例如,考虑一个例程:

string FindCustomer(int customerID) 

先置条件可能是 customerID 为正数。后置条件可能是我们保证能找到客户,例如,可能在其他方面,返回值是一个非空的 string

先置条件失败表明调用者(客户端)存在 bug。后置条件失败表明例程(供应商)存在 bug。这些条件或规范通过断言语句来实现。在 C/C++ 代码中,assert 宏用于这些目的。这些会在断言失败时生成一个“ abort, ignore, retry”(中止、忽略、重试)的消息框。另一种方法是使用异常处理。我下面描述的框架允许您通过定义或不定义条件编译常量来使用其中一种方法。

在 C++ 中,我们无法像 Eiffel 那样全面,但我们可以走一部分路。下面的框架提供了异常类来表示先置条件、后置条件、类不变量和一般断言。为了简化使用,我提供了一些宏来在合约失败时生成相应的异常。或者,可以通过设置条件编译标志来使用 C assert 宏而不是抛出异常。在调试时,有时您希望能够忽略断言并继续逐步执行代码,特别是当例程仍处于变动状态时。例如,一个断言可能不再有效,但您仍然希望将该断言标记出来,提醒您需要修复代码(移除断言或用另一个替换它)。

该框架力求提供最大的灵活性。

对于每个包含合约设计框架的项目,您可以:

  1. 生成调试断言而不是异常。
  2. 分别启用或禁用先置条件、后置条件、不变量和断言检查。但是,框架在交付时,已基于 Meyer 书中的一个逻辑方案进行了定义。
  3. 按类或按方法禁用先置条件、后置条件、不变量或断言检查。
  4. 为每个断言提供描述,或者不提供。如果不提供,框架将告诉您生成的是哪种类型的错误——先置条件、后置条件等。
  5. 为 Debug 和 Release 版本定义不同的规则。框架在交付时,允许您选择在 Release 版本中启用或禁用仅先置条件,但这可以通过编辑头文件进行修改。

合约与继承

当合约设计与继承一起使用时,有一些规则应该遵守。Eiffel 提供了语言支持来强制执行这些规则,但在 C++ 中,我们必须依赖程序员。这些规则是,在派生类中(Meyer 第 16 章):

  1. 重写的方法可以(仅)放宽先置条件。这意味着重写后的先置条件应与被覆盖的先置条件逻辑上“或”在一起。
  2. 重写的方法可以(仅)加强后置条件。这意味着重写后的后置条件应与被覆盖的后置条件逻辑上“与”在一起。
  3. 派生类的类不变量应与其基类的不变量逻辑上“与”在一起。

示例(使用伪 C++ 语法)

class D : public B
virtual int B::foo(int x)
{
  REQUIRE(1 < x < 3);
  ...
  ENSURE(result < 15);
  return result;
}
virtual int D::foo(int x)
{
  REQUIRE(1 < x < 3 or 0 < x < 5); // weakened precondition
  ...
  ENSURE(result < 15 and result < 3); // strengthened postcondition
  return result;
}

Eiffel 具有支持上述内容的语言结构。在 D::foo() 中,我们会写:

require else 0 < x < 5

这意味着先检查基类的先置条件,如果失败,则检查派生类版本。

ensure then result < 3

这意味着检查基类的后置条件和派生类的后置条件,并确保它们都通过。

对于 C++,我们只需要写:

REQUIRE(0 < x < 5 )
ENSURE(result < 3)

确保先置条件始终等于或弱于基类版本,后置条件始终等于或强于基类版本。

对于不变量,在 B 中,我们可能有:

INVARIANT(B::a > 0 and B::b > 0);

D 中:

INVARIANT(D::c > 0 and D::d > 0);

规则要求我们在 D 中组合这些:

INVARIANT(B::a > 0 and B::b > 0 and D::c > 0 and D::d > 0);

INVARIANT(B::a > 0 and B::b > 0);
INVARIANT(D::c > 0 and D::d > 0);

条件编译常量

全局设置

  • DESIGN_BY_CONTRACT - 启用合约设计检查
  • USE_ASSERTIONS - 使用 ASSERT 宏而不是异常

用于启用和禁用每种类型的合约

这些建议基于 Meyer 的第 393 页。

  • CHECK_ALL - 检查断言 - 包含检查先置条件、后置条件和不变量
  • CHECK_INVARIANT - 检查不变量 - 包含检查先置条件和后置条件
  • CHECK_POSTCONDITION - 检查后置条件 - 包含检查先置条件
  • CHECK_PRECONDITION - 仅检查先置条件,例如,在 Release 版本中

因此,要启用所有检查并使用异常处理,请在头文件中写入:

#define DESIGN_BY_CONTRACT
#define CHECK_ALL

或将它们定义为预处理器设置。

在您的实现文件中,写入:

#include "mydefines.h"
#include "DesignByContract.h"
using namespace DesignByContract;

示例

以下代码将在 Visual C++ 6 或 7 中运行。它已设置为使用断言宏而不是异常,这样通过单击错误对话框中的“忽略”,您可以逐步执行所有断言失败,以查看一些不同的消息显示选项。所有断言都将执行,因为 CHECK_ALL 已定义。

框架类定义在头文件 DesignByContract.h 中,可以在源文件下载中找到。

// DesignByContract.cpp : Defines the entry point for the console application.
//
#include "stdafx.h"
#include "dbcdefs.h"
#include "DesignByContract.h"
#include <iostream>
#include <string>

using namespace std;
// Example debugging flags - can make this as fine-grained as we want
#ifdef _DEBUG
    static const bool NOT_CHECK_FOO = false; // we are debugging: enable 
                                             // DBC check for foo()
#else
    static const bool NOT_CHECK_FOO = true; // we are not debugging: 
                                            //disable DBC check for foo()
#endif
using namespace DesignByContract;
int foo(const char* customerName) // throw(AssertionException)
{
    // Precondition check on function arguments 
    // but only if foo() is being monitored
    REQUIRE(NOT_CHECK_FOO || customerName != NULL, "Must specify a customer");

    int val = 3;

    // General assertion check 
    // Override our monitoring flag for foo() to always check this 
    // (No description supplied)
    CHECK0(val < 3); 

    // Invariant check (contrived)
    // (No description supplied)
    INVARIANT0(customerName != NULL && val > 0);

    // Postcondition check on function return value
    // but only if foo() is being monitored
    ENSURE(NOT_CHECK_FOO || val == 2, "Value must be 2");

    return val;
}

int main(int argc, char* argv[])
{
    try
    {
        const char* customerName = 0;
        int val = foo(customerName);
    }
    catch(const DesignByContractException & e)
    {
        cout << e; // Note: "<<" is overloaded to produce meaningful output
    }

    return 0;
}

头文件 dbcdefs.h 看起来像这样:

#ifndef __DBCDEFS_H__
#define __DBCDEFS_H__

// Note: If this file is included as-is your client code will execute with
// DESIGN_BY_CONTRACT, USE_ASSERTIONS and CHECK_ALL defined.

// If, say, you want to use exception-handling and precondition checking only
// then comment out the #defines USE_ASSERTIONS, CHECK_ALL, CHECK_INVARIANT 
// and CHECK_POSTCONDITION

// If you want postconditions and preconditions,
// then comment out the #defines USE_ASSERTIONS, CHECK_ALL, CHECK_INVARIANT
// and so on.

// In a production environment you might wish to define these in preprocessor 
// settings rather than use this file.

#define DESIGN_BY_CONTRACT // Enable Design by Contract checks
#define USE_ASSERTIONS     // Use ASSERT macros instead of exceptions

#define CHECK_ALL           // Check assertions - implies checking preconditions, 
                            // postconditions and invariants
#define CHECK_INVARIANT     // Check invariants - implies checking preconditions 
                            // and postconditions
#define CHECK_POSTCONDITION // Check postconditions - implies checking 
                            // preconditions 
#define CHECK_PRECONDITION  // Check preconditions only, e.g., in Release build

#endif //__DBCDEFS_H__

运行此示例并单击“忽略”以逐步执行断言,会产生以下输出:

Assertion Failure Image

Assertion Failure Image

Assertion Failure Image

Assertion Failure Image

历史

  • 2002 年 6 月 20 日 - 更新下载

许可证

本文未附加明确的许可证,但可能在文章文本或下载文件本身中包含使用条款。如有疑问,请通过下面的讨论区联系作者。

作者可能使用的许可证列表可以在此处找到。

© . All rights reserved.