CppCoreGuidelines I.7 声明后置条件

19 March 2022

I.7: State postconditions

理由

检测到针对输出结果可能的误解，可能可以发现代码实现错误。

例子

int area(int height, int width) { return height * width; }  // bad

此处，我们故意不做前置条件判断，因此长宽不一定是正数。我们也没有检查后置条件，长宽的乘积可能超过最大整数，从而产生溢出。

可以这么写：

#include <gsl/gsl_assert>
int area(int height, int width)
{
    auto res = height * width;
    Ensures(res > 0);
    return res;
}
int main()
{
    cout << area(-10, 10) << endl;
    return 0;
}

terminate called without an active exception

例子

考虑这个著名的安全 bug：

#include <string.h>
const int MAX = 10;
void f()    // problematic
{
    char buffer[MAX];
    // ...
    memset(buffer, 0, sizeof(buffer));
}
int main()
{
    f();
    return 0;
}

为没有后置条件说 buffer 必须清零，所以显然多余的memset()调用可能会被编译优化掉（实际执行看不出来）。

#include <gsl/gsl_assert>
#include <string.h>
const int MAX = 10;
void f()    // problematic
{
    char buffer[MAX];
    // ...
    memset(buffer, 0, sizeof(buffer));
    Ensures(buffer[0] == 0);
}
int main()
{
    f();
    return 0;
}

注意

后置条件经常在注释中非正式的介绍函数的目的；Ensures()可以更系统化、更明显、更容易检查。

注意

除了直接返回结果的情况，后置条件也可用于其他如数据结构状态的检查。

例子

一个操作 Record 的函数，使用互斥锁避免竞争条件：

mutex m;

void manipulate(Record& r)    // don't
{
    m.lock();
    // ... no m.unlock() ...
}

此处，我们忘记了说明是否要释放互斥锁，因此我们不知道这是有意为之，还是 bug。标明后置条件可以澄清：

void manipulate(Record& r)    // postcondition: m is unlocked upon exit
{
    m.lock();
    // ... no m.unlock() ...
}

这时候，我们就知道，这是个 bug 。但是需要读注释。

更好地办法是，通过过 RAII （Resource Acquisition Is Initialization，资源获取就是初始化）确保满足“函数结束时释放互斥锁”这个后置条件：

#include <mutex>
#include <thread>
struct Record {
    int x;
} r;
mutex m;
void manipulate(Record& r, int n)    // best
{
    lock_guard<mutex> _ {m};
    r.x = n;
    cout << r.x << endl;
}
int main()
{
    thread t([]{ manipulate(r, 1);});
    manipulate(r, 2);
    t.join();
    return 0;
}

2
1

注意

理想情况下，最好可以在接口声明中标明后置条件，用户可以方便看到。
只有与用户相关的后置条件展示在接口定义中。
内部状态相关的后置条件放在实现和定义中。

强化

比较难。工具可以支持锁的状态检查。

programming 164

CppCoreGuidelines 475