实例演示

我们已经介绍了 ACSL 和 WP 的基本思想，下面我们将结合实例演示如何使用 WP 来验证包含 ACSL 注释的 C 项目。

示例代码介绍

我们的示例代码围绕寻找数组中最大值的问题展开。这个项目包含三个文件。项目的入口 main 函数在 max_seq_main.c 文件中。该 main 函数调用一个名为 max_seq 的函数计算给定数组中的最大值。此 max_seq 函数的定义位于头文件 max_seq.h 中。而 max_seq 函数的实现则在 max_seq.c 文件中。我们力图通过这种组织方式模拟一个真实项目的结构，max_seq_main.c 文件代表上层逻辑，max_seq.c 代表底层实现，头文件则是接口。三个文件的内容如下：

/* max_seq_main.c */
#include "max_seq.h"

int main() {
    int array[10] = {3, 1, 4, 1, 5, 9, 2, 6, 5, 3};
    int m = max_seq(array, 10);
    //@ assert \exists int i; m == array[i];
    //@ assert \forall int i; 0 <= i < 10 ==> m >= array[i];
    return 0;
}

/* max_seq.h */
/*@ requires n > 0 && \valid(p + (0..n-1));
    ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];
    ensures \exists int e; 0 <= e <= n−1 && \result == p[e];
*/
int max_seq(int* p, int n);

/* max_seq.c */
#include "max_seq.h"

int max_seq(int* p, int n) {
    int res = *p;
    //@ ghost int e = 0;
    /*@ loop invariant \forall integer j;
            0 <= j < i ==> res >= p[j];
        loop invariant \valid(p + e) && p[e] == res;
        loop invariant about_i: 0 <= i <= n;
        loop invariant 0 <= e < n;
        loop invariant p == \at(p, Pre) && n == \at(n, Pre);
        loop invariant \valid(p + (0..n-1));
    */
    for(int i = 0; i < n; i++) {
        if (res < p[i]) {
            res = p[i];
            //@ ghost e = i;
        }
    }
    return res;
}

在 max_seq_main.c 文件中，main 函数首先创建了一个数组，然后调用 max_seq 函数寻找数组中的最大值并存储在变量 m 中。为了保证我们确实找到了

数组中

的

最大值

，我们做出了两个断言（assert）。第一个断言声明 m 等于数组中的某个元素（m 存在于数组中）；第二个断言声明 m 大于等于数组中所有的元素（m 的值最大）。我们将在演示环节看到 WP 能够帮助我们验证这两条性质。

正如我们所见，max_seq_main.c 文件包含了 max_seq.h 头文件，因为 max_seq 函数的声明（或曰接口）在该头文件内。与 max_seq 函数的声明一起，max_seq.h 头文件还包含了该函数的合约。合约的前置条件部分要求了（requires）数组的长度 n 大于 0；且从数组头 p 开始的 n 个内存位置均可合法访问。合约的后置条件对函数的功能正确性做出了保证（ensures）。其保证的内容和上面讨论的 main 函数中的断言形式类似。不过作为函数的合约，此处的表达是基于函数的形式参数，更具一般性。也是这个原因，当我们验证过 max_seq 函数的合约成立之后，再去验证 main 函数中的断言就会变得非常容易。

相对困难的是验证 max_seq 函数的实现确实符合合约。从 max_seq.c 文件中可见，max_seq 函数的实现并不复杂，它先把变量 res 赋值为 p[0]，然后从头（p[0]）到尾（p[n-1]）检查数组中元素的值，如果发现更大的，就更新 res。但要 WP 验证这个实现符合合约，一些提示是必须的。提示包括幽灵变量（ghost）e 的引入和 6 个循环不变式（loop invariant）。直观上来讲，e 是一个辅助变量，记录了已搜索范围内最大元素的坐标（相对数组头地址的偏移）。第一条循环不变式指出在已搜索的范围内，没有比 res 更大的值。第二条不变式指出这个 res 的值不是凭空出现的，它等于数组中一个合法的元素 p[e]。随后两条不变式给出了搜索范围 i 和最大元素坐标 e 的取值范围。

最后两条不变式看似和合约的前置条件重复，但却是不可或缺的。这是因为 WP 会认为每次更新后的内存状态与之前的状态都是不同的，所以关于某些数据的性质（比如此处数组能够被合法访问的性质）需要重新建立。因为循环操作的复杂性，某些性质不能被 WP（在合理时间内）自动重建。此时一些提示就是必要的了。此例中倒数第二条不变式指出了 p 和 n 不会被循环体修改；进而如最后一条不变式指出，无论循环次数，从数组头 p 开始的 n 个内存位置总是可以合法访问的。

具体来说，按照 ACSL 的规定，WP 会给每个